Theory Group_ZF
section ‹Groups - introduction›
theory Group_ZF imports Monoid_ZF
begin
text‹This theory file covers basics of group theory.›
subsection‹Definition and basic properties of groups›
text‹In this section we define the notion of a group and set up the
notation for discussing groups. We prove some basic theorems about
groups.›
text‹To define a group we take a monoid and add a requirement
that the right inverse needs to exist for every element of the group.›
definition
"IsAgroup(G,f) ≡
(IsAmonoid(G,f) ∧ (∀g∈G. ∃b∈G. f`⟨g,b⟩ = TheNeutralElement(G,f)))"
text‹We define the group inverse as the set
$\{\langle x,y \rangle \in G\times G: x\cdot y = e \}$, where $e$ is the
neutral element of the group. This set (which can be written as
$(\cdot)^{-1}\{ e\}$) is a certain relation on the group (carrier).
Since, as we show later, for every $x\in G$ there is exactly one $y\in G$
such that $x \cdot y = e$ this relation is in fact a function from $G$ to $G$.›
definition
"GroupInv(G,f) ≡ {⟨x,y⟩ ∈ G×G. f`⟨x,y⟩ = TheNeutralElement(G,f)}"
text‹We will use the miltiplicative notation for groups. The neutral
element is denoted $1$.›
locale group0 =
fixes G
fixes P
assumes groupAssum: "IsAgroup(G,P)"
fixes neut ("𝟭")
defines neut_def[simp]: "𝟭 ≡ TheNeutralElement(G,P)"
fixes groper (infixl "⋅" 70)
defines groper_def[simp]: "a ⋅ b ≡ P`⟨a,b⟩"
fixes inv ("_¯ " [90] 91)
defines inv_def[simp]: "x¯ ≡ GroupInv(G,P)`(x)"
text‹First we show a lemma that says that we can use theorems proven in
the ‹monoid0› context (locale).›
lemma (in group0) group0_2_L1: shows "monoid0(G,P)"
using groupAssum IsAgroup_def monoid0_def by simp
text‹The theorems proven in the ‹monoid› context are valid in the ‹group0› context.›
sublocale group0 < monoid: monoid0 G P groper
unfolding groper_def using group0_2_L1 by auto
text‹In some strange cases Isabelle has difficulties with applying
the definition of a group. The next lemma defines a rule to be applied
in such cases.›
lemma definition_of_group: assumes "IsAmonoid(G,f)"
and "∀g∈G. ∃b∈G. f`⟨g,b⟩ = TheNeutralElement(G,f)"
shows "IsAgroup(G,f)"
using assms IsAgroup_def by simp
text‹A technical lemma that allows to use $1$ as the neutral element of
the group without referencing a list of lemmas and definitions.›
lemma (in group0) group0_2_L2:
shows "𝟭∈G ∧ (∀g∈G.(𝟭⋅g = g ∧ g⋅𝟭 = g))"
using group0_2_L1 monoid.unit_is_neutral by simp
text‹The group is closed under the group operation. Used all the time,
useful to have handy.›
lemma (in group0) group_op_closed: assumes "a∈G" "b∈G"
shows "a⋅b ∈ G" using assms monoid.group0_1_L1
by simp
text‹The group operation is associative. This is another technical lemma
that allows to shorten the list of referenced lemmas in some proofs.›
lemma (in group0) group_oper_assoc:
assumes "a∈G" "b∈G" "c∈G" shows "a⋅(b⋅c) = a⋅b⋅c"
using groupAssum assms IsAgroup_def IsAmonoid_def
IsAssociative_def group_op_closed by simp
text‹The group operation maps $G\times G$ into $G$. It is conveniet to have
this fact easily accessible in the ‹group0› context.›
lemma (in group0) group_oper_fun: shows "P : G×G→G"
using groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def
by simp
text‹The definition of a group requires the existence of the right inverse.
We show that this is also the left inverse.›
theorem (in group0) group0_2_T1:
assumes A1: "g∈G" and A2: "b∈G" and A3: "g⋅b = 𝟭"
shows "b⋅g = 𝟭"
proof -
from A2 groupAssum obtain c where I: "c ∈ G ∧ b⋅c = 𝟭"
using IsAgroup_def by auto
then have "c∈G" by simp
have "𝟭∈G" using group0_2_L2 by simp
with A1 A2 I have "b⋅g = b⋅(g⋅(b⋅c))"
using group_op_closed group0_2_L2 group_oper_assoc
by simp
also from A1 A2 ‹c∈G› have "b⋅(g⋅(b⋅c)) = b⋅(g⋅b⋅c)"
using group_oper_assoc by simp
also from A3 A2 I have "b⋅(g⋅b⋅c)= 𝟭" using group0_2_L2 by simp
finally show "b⋅g = 𝟭" by simp
qed
text‹For every element of a group there is only one inverse.›
lemma (in group0) group0_2_L4:
assumes A1: "x∈G" shows "∃!y. y∈G ∧ x⋅y = 𝟭"
proof
from A1 groupAssum show "∃y. y∈G ∧ x⋅y = 𝟭"
using IsAgroup_def by auto
fix y n
assume A2: "y∈G ∧ x⋅y = 𝟭" and A3:"n∈G ∧ x⋅n = 𝟭" show "y=n"
proof -
from A1 A2 have T1: "y⋅x = 𝟭"
using group0_2_T1 by simp
from A2 A3 have "y = y⋅(x⋅n)"
using group0_2_L2 by simp
also from A1 A2 A3 have "… = (y⋅x)⋅n"
using group_oper_assoc by blast
also from T1 A3 have "… = n"
using group0_2_L2 by simp
finally show "y=n" by simp
qed
qed
text‹The group inverse is a function that maps G into G.›
theorem group0_2_T2:
assumes A1: "IsAgroup(G,f)" shows "GroupInv(G,f) : G→G"
proof -
have "GroupInv(G,f) ⊆ G×G" using GroupInv_def by auto
moreover from A1 have
"∀x∈G. ∃!y. y∈G ∧ ⟨x,y⟩ ∈ GroupInv(G,f)"
using group0_def group0.group0_2_L4 GroupInv_def by simp
ultimately show ?thesis using func1_1_L11 by simp
qed
text‹We can think about the group inverse (the function)
as the inverse image of the neutral element. Recall that
in Isabelle ‹f-``(A)› denotes the inverse image of
the set $A$.›
theorem (in group0) group0_2_T3: shows "P-``{𝟭} = GroupInv(G,P)"
proof -
from groupAssum have "P : G×G → G"
using IsAgroup_def IsAmonoid_def IsAssociative_def
by simp
then show "P-``{𝟭} = GroupInv(G,P)"
using func1_1_L14 GroupInv_def by auto
qed
text‹The inverse is in the group.›
lemma (in group0) inverse_in_group: assumes A1: "x∈G" shows "x¯∈G"
proof -
from groupAssum have "GroupInv(G,P) : G→G" using group0_2_T2 by simp
with A1 show ?thesis using apply_type by simp
qed
text‹The notation for the inverse means what it is supposed to mean.›
lemma (in group0) group0_2_L6:
assumes A1: "x∈G" shows "x⋅x¯ = 𝟭 ∧ x¯⋅x = 𝟭"
proof
from groupAssum have "GroupInv(G,P) : G→G"
using group0_2_T2 by simp
with A1 have "⟨x,x¯⟩ ∈ GroupInv(G,P)"
using apply_Pair by simp
then show "x⋅x¯ = 𝟭" using GroupInv_def by simp
with A1 show "x¯⋅x = 𝟭" using inverse_in_group group0_2_T1
by blast
qed
text‹The next two lemmas state that unless we multiply by
the neutral element, the result is always
different than any of the operands.›
lemma (in group0) group0_2_L7:
assumes A1: "a∈G" and A2: "b∈G" and A3: "a⋅b = a"
shows "b=𝟭"
proof -
from A3 have "a¯ ⋅ (a⋅b) = a¯⋅a" by simp
with A1 A2 show ?thesis using
inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
by simp
qed
text‹See the comment to ‹group0_2_L7›.›
lemma (in group0) group0_2_L8:
assumes A1: "a∈G" and A2: "b∈G" and A3: "a⋅b = b"
shows "a=𝟭"
proof -
from A3 have "(a⋅b)⋅b¯ = b⋅b¯" by simp
with A1 A2 have "a⋅(b⋅b¯) = b⋅b¯" using
inverse_in_group group_oper_assoc by simp
with A1 A2 show ?thesis
using group0_2_L6 group0_2_L2 by simp
qed
text‹The inverse of the neutral element is the neutral element.›
lemma (in group0) group_inv_of_one: shows "𝟭¯ = 𝟭"
using group0_2_L2 inverse_in_group group0_2_L6 group0_2_L7 by blast
text‹if $a^{-1} = 1$, then $a=1$.›
lemma (in group0) group0_2_L8A:
assumes A1: "a∈G" and A2: "a¯ = 𝟭"
shows "a = 𝟭"
proof -
from A1 have "a⋅a¯ = 𝟭" using group0_2_L6 by simp
with A1 A2 show "a = 𝟭" using group0_2_L2 by simp
qed
text‹If $a$ is not a unit, then its inverse is not a unit either.›
lemma (in group0) group0_2_L8B:
assumes "a∈G" and "a ≠ 𝟭"
shows "a¯ ≠ 𝟭" using assms group0_2_L8A by auto
text‹If $a^{-1}$ is not a unit, then a is not a unit either.›
lemma (in group0) group0_2_L8C:
assumes "a∈G" and "a¯ ≠ 𝟭"
shows "a≠𝟭"
using assms group0_2_L8A group_inv_of_one by auto
text‹If a product of two elements of a group is equal to the neutral
element then they are inverses of each other.›
lemma (in group0) group0_2_L9:
assumes A1: "a∈G" and A2: "b∈G" and A3: "a⋅b = 𝟭"
shows "a = b¯" and "b = a¯"
proof -
from A3 have "a⋅b⋅b¯ = 𝟭⋅b¯" by simp
with A1 A2 have "a⋅(b⋅b¯) = 𝟭⋅b¯" using
inverse_in_group group_oper_assoc by simp
with A1 A2 show "a = b¯" using
group0_2_L6 inverse_in_group group0_2_L2 by simp
from A3 have "a¯⋅(a⋅b) = a¯⋅𝟭" by simp
with A1 A2 show "b = a¯" using
inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
by simp
qed
text‹It happens quite often that we know what is (have a meta-function for)
the right inverse in a group. The next lemma shows that the value
of the group inverse (function) is equal to the right inverse
(meta-function).›
lemma (in group0) group0_2_L9A:
assumes A1: "∀g∈G. b(g) ∈ G ∧ g⋅b(g) = 𝟭"
shows "∀g∈G. b(g) = g¯"
proof
fix g assume "g∈G"
moreover from A1 ‹g∈G› have "b(g) ∈ G" by simp
moreover from A1 ‹g∈G› have "g⋅b(g) = 𝟭" by simp
ultimately show "b(g) = g¯" by (rule group0_2_L9)
qed
text‹What is the inverse of a product?›
lemma (in group0) group_inv_of_two:
assumes A1: "a∈G" and A2: "b∈G"
shows " b¯⋅a¯ = (a⋅b)¯"
proof -
from A1 A2 have
"b¯∈G" "a¯∈G" "a⋅b∈G" "b¯⋅a¯ ∈ G"
using inverse_in_group group_op_closed
by auto
from A1 A2 ‹b¯⋅a¯ ∈ G› have "a⋅b⋅(b¯⋅a¯) = a⋅(b⋅(b¯⋅a¯))"
using group_oper_assoc by simp
moreover from A2 ‹b¯∈G› ‹a¯∈G› have "b⋅(b¯⋅a¯) = b⋅b¯⋅a¯"
using group_oper_assoc by simp
moreover from A2 ‹a¯∈G› have "b⋅b¯⋅a¯ = a¯"
using group0_2_L6 group0_2_L2 by simp
ultimately have "a⋅b⋅(b¯⋅a¯) = a⋅a¯"
by simp
with A1 have "a⋅b⋅(b¯⋅a¯) = 𝟭"
using group0_2_L6 by simp
with ‹a⋅b ∈ G› ‹b¯⋅a¯ ∈ G› show "b¯⋅a¯ = (a⋅b)¯"
using group0_2_L9 by simp
qed
text‹What is the inverse of a product of three elements?›
lemma (in group0) group_inv_of_three:
assumes A1: "a∈G" "b∈G" "c∈G"
shows
"(a⋅b⋅c)¯ = c¯⋅(a⋅b)¯"
"(a⋅b⋅c)¯ = c¯⋅(b¯⋅a¯)"
"(a⋅b⋅c)¯ = c¯⋅b¯⋅a¯"
proof -
from A1 have T:
"a⋅b ∈ G" "a¯ ∈ G" "b¯ ∈ G" "c¯ ∈ G"
using group_op_closed inverse_in_group by auto
with A1 show
"(a⋅b⋅c)¯ = c¯⋅(a⋅b)¯" and "(a⋅b⋅c)¯ = c¯⋅(b¯⋅a¯)"
using group_inv_of_two by auto
with T show "(a⋅b⋅c)¯ = c¯⋅b¯⋅a¯" using group_oper_assoc
by simp
qed
text‹The inverse of the inverse is the element.›
lemma (in group0) group_inv_of_inv:
assumes "a∈G" shows "a = (a¯)¯"
using assms inverse_in_group group0_2_L6 group0_2_L9
by simp
text‹Group inverse is nilpotent, therefore a bijection and involution.›
lemma (in group0) group_inv_bij:
shows "GroupInv(G,P) O GroupInv(G,P) = id(G)" and "GroupInv(G,P) ∈ bij(G,G)" and
"GroupInv(G,P) = converse(GroupInv(G,P))"
proof -
have I: "GroupInv(G,P): G→G" using groupAssum group0_2_T2 by simp
then have "GroupInv(G,P) O GroupInv(G,P): G→G" and "id(G):G→G"
using comp_fun id_type by auto
moreover
{ fix g assume "g∈G"
with I have "(GroupInv(G,P) O GroupInv(G,P))`(g) = id(G)`(g)"
using comp_fun_apply group_inv_of_inv id_conv by simp
} hence "∀g∈G. (GroupInv(G,P) O GroupInv(G,P))`(g) = id(G)`(g)" by simp
ultimately show "GroupInv(G,P) O GroupInv(G,P) = id(G)"
by (rule func_eq)
with I show "GroupInv(G,P) ∈ bij(G,G)" using nilpotent_imp_bijective
by simp
with ‹GroupInv(G,P) O GroupInv(G,P) = id(G)› show
"GroupInv(G,P) = converse(GroupInv(G,P))" using comp_id_conv by simp
qed
text‹A set comprehension form of the image of a set under the group inverse. ›
lemma (in group0) ginv_image: assumes "V⊆G"
shows "GroupInv(G,P)``(V) ⊆ G" and "GroupInv(G,P)``(V) = {g¯. g ∈ V}"
proof -
from assms have I: "GroupInv(G,P)``(V) = {GroupInv(G,P)`(g). g∈V}"
using groupAssum group0_2_T2 func_imagedef by blast
thus "GroupInv(G,P)``(V) = {g¯. g ∈ V}" by simp
show "GroupInv(G,P)``(V) ⊆ G" using groupAssum group0_2_T2 func1_1_L6(2) by blast
qed
text‹Inverse of an element that belongs to the inverse of the set belongs to the set. ›
lemma (in group0) ginv_image_el: assumes "V⊆G" "g ∈ GroupInv(G,P)``(V)"
shows "g¯ ∈ V"
using assms ginv_image group_inv_of_inv by auto
text‹For the group inverse the image is the same as inverse image.›
lemma (in group0) inv_image_vimage: shows "GroupInv(G,P)``(V) = GroupInv(G,P)-``(V)"
using group_inv_bij vimage_converse by simp
text‹If the unit is in a set then it is in the inverse of that set.›
lemma (in group0) neut_inv_neut: assumes "A⊆G" and "𝟭∈A"
shows "𝟭 ∈ GroupInv(G,P)``(A)"
proof -
have "GroupInv(G,P):G→G" using groupAssum group0_2_T2 by simp
with assms have "𝟭¯ ∈ GroupInv(G,P)``(A)" using func_imagedef by auto
then show ?thesis using group_inv_of_one by simp
qed
text‹The group inverse is onto.›
lemma (in group0) group_inv_surj: shows "GroupInv(G,P)``(G) = G"
using group_inv_bij bij_def surj_range_image_domain by auto
text‹If $a^{-1}\cdot b=1$, then $a=b$.›
lemma (in group0) group0_2_L11:
assumes A1: "a∈G" "b∈G" and A2: "a¯⋅b = 𝟭"
shows "a=b"
proof -
from A1 A2 have "a¯ ∈ G" "b∈G" "a¯⋅b = 𝟭"
using inverse_in_group by auto
then have "b = (a¯)¯" by (rule group0_2_L9)
with A1 show "a=b" using group_inv_of_inv by simp
qed
text‹If $a\cdot b^{-1}=1$, then $a=b$.›
lemma (in group0) group0_2_L11A:
assumes A1: "a∈G" "b∈G" and A2: "a⋅b¯ = 𝟭"
shows "a=b"
proof -
from A1 A2 have "a ∈ G" "b¯∈G" "a⋅b¯ = 𝟭"
using inverse_in_group by auto
then have "a = (b¯)¯" by (rule group0_2_L9)
with A1 show "a=b" using group_inv_of_inv by simp
qed
text‹If if the inverse of $b$ is different than $a$, then the
inverse of $a$ is different than $b$.›
lemma (in group0) group0_2_L11B:
assumes A1: "a∈G" and A2: "b¯ ≠ a"
shows "a¯ ≠ b"
proof -
{ assume "a¯ = b"
then have "(a¯)¯ = b¯" by simp
with A1 A2 have False using group_inv_of_inv
by simp
} then show "a¯ ≠ b" by auto
qed
text‹What is the inverse of $ab^{-1}$ ?›
lemma (in group0) group0_2_L12:
assumes A1: "a∈G" "b∈G"
shows
"(a⋅b¯)¯ = b⋅a¯"
"(a¯⋅b)¯ = b¯⋅a"
proof -
from A1 have
"(a⋅b¯)¯ = (b¯)¯⋅ a¯" and "(a¯⋅b)¯ = b¯⋅(a¯)¯"
using inverse_in_group group_inv_of_two by auto
with A1 show "(a⋅b¯)¯ = b⋅a¯" "(a¯⋅b)¯ = b¯⋅a"
using group_inv_of_inv by auto
qed
text‹A couple useful rearrangements with three elements:
we can insert a $b\cdot b^{-1}$
between two group elements (another version) and one about a product of
an element and inverse of a product, and two others.›
lemma (in group0) group0_2_L14A:
assumes A1: "a∈G" "b∈G" "c∈G"
shows
"a⋅c¯= (a⋅b¯)⋅(b⋅c¯)"
"a¯⋅c = (a¯⋅b)⋅(b¯⋅c)"
"a⋅(b⋅c)¯ = a⋅c¯⋅b¯"
"a⋅(b⋅c¯) = a⋅b⋅c¯"
"(a⋅b¯⋅c¯)¯ = c⋅b⋅a¯"
"a⋅b⋅c¯⋅(c⋅b¯) = a"
"a⋅(b⋅c)⋅c¯ = a⋅b"
proof -
from A1 have T:
"a¯ ∈ G" "b¯∈G" "c¯∈G"
"a¯⋅b ∈ G" "a⋅b¯ ∈ G" "a⋅b ∈ G"
"c⋅b¯ ∈ G" "b⋅c ∈ G"
using inverse_in_group group_op_closed
by auto
from A1 T have
"a⋅c¯ = a⋅(b¯⋅b)⋅c¯"
"a¯⋅c = a¯⋅(b⋅b¯)⋅c"
using group0_2_L2 group0_2_L6 by auto
with A1 T show
"a⋅c¯= (a⋅b¯)⋅(b⋅c¯)"
"a¯⋅c = (a¯⋅b)⋅(b¯⋅c)"
using group_oper_assoc by auto
from A1 have "a⋅(b⋅c)¯ = a⋅(c¯⋅b¯)"
using group_inv_of_two by simp
with A1 T show "a⋅(b⋅c)¯ =a⋅c¯⋅b¯"
using group_oper_assoc by simp
from A1 T show "a⋅(b⋅c¯) = a⋅b⋅c¯"
using group_oper_assoc by simp
from A1 T show "(a⋅b¯⋅c¯)¯ = c⋅b⋅a¯"
using group_inv_of_three group_inv_of_inv
by simp
from T have "a⋅b⋅c¯⋅(c⋅b¯) = a⋅b⋅(c¯⋅(c⋅b¯))"
using group_oper_assoc by simp
also from A1 T have "… = a⋅b⋅b¯"
using group_oper_assoc group0_2_L6 group0_2_L2
by simp
also from A1 T have "… = a⋅(b⋅b¯)"
using group_oper_assoc by simp
also from A1 have "… = a"
using group0_2_L6 group0_2_L2 by simp
finally show "a⋅b⋅c¯⋅(c⋅b¯) = a" by simp
from A1 T have "a⋅(b⋅c)⋅c¯ = a⋅(b⋅(c⋅c¯))"
using group_oper_assoc by simp
also from A1 T have "… = a⋅b"
using group0_2_L6 group0_2_L2 by simp
finally show "a⋅(b⋅c)⋅c¯ = a⋅b"
by simp
qed
text‹ A simple equation to solve ›
lemma (in group0) simple_equation0:
assumes "a∈G" "b∈G" "c∈G" "a⋅b¯ = c¯"
shows "c = b⋅a¯"
proof -
from assms(4) have "(a⋅b¯)¯ = (c¯)¯" by simp
with assms(1,2,3) show "c = b⋅a¯" using group0_2_L12(1) group_inv_of_inv by simp
qed
text‹ Another simple equation ›
lemma (in group0) simple_equation1:
assumes "a∈G" "b∈G" "c∈G" "a¯⋅b = c¯"
shows "c = b¯⋅a"
proof -
from assms(4) have "(a¯⋅b)¯ = (c¯)¯" by simp
with assms(1,2,3) show "c = b¯⋅a" using group0_2_L12(2) group_inv_of_inv by simp
qed
text‹Another lemma about rearranging a product of four group
elements.›
lemma (in group0) group0_2_L15:
assumes A1: "a∈G" "b∈G" "c∈G" "d∈G"
shows "(a⋅b)⋅(c⋅d)¯ = a⋅(b⋅d¯)⋅a¯⋅(a⋅c¯)"
proof -
from A1 have T1:
"d¯∈G" "c¯∈G" "a⋅b∈G" "a⋅(b⋅d¯)∈G"
using inverse_in_group group_op_closed
by auto
with A1 have "(a⋅b)⋅(c⋅d)¯ = (a⋅b)⋅(d¯⋅c¯)"
using group_inv_of_two by simp
also from A1 T1 have "… = a⋅(b⋅d¯)⋅c¯"
using group_oper_assoc by simp
also from A1 T1 have "… = a⋅(b⋅d¯)⋅a¯⋅(a⋅c¯)"
using group0_2_L14A by blast
finally show ?thesis by simp
qed
text‹We can cancel an element with its inverse that is written next to it.›
lemma (in group0) inv_cancel_two:
assumes A1: "a∈G" "b∈G"
shows
"a⋅b¯⋅b = a"
"a⋅b⋅b¯ = a"
"a¯⋅(a⋅b) = b"
"a⋅(a¯⋅b) = b"
proof -
from A1 have
"a⋅b¯⋅b = a⋅(b¯⋅b)" "a⋅b⋅b¯ = a⋅(b⋅b¯)"
"a¯⋅(a⋅b) = a¯⋅a⋅b" "a⋅(a¯⋅b) = a⋅a¯⋅b"
using inverse_in_group group_oper_assoc by auto
with A1 show
"a⋅b¯⋅b = a"
"a⋅b⋅b¯ = a"
"a¯⋅(a⋅b) = b"
"a⋅(a¯⋅b) = b"
using group0_2_L6 group0_2_L2 by auto
qed
text‹Another lemma about cancelling with two group elements.›
lemma (in group0) group0_2_L16A:
assumes A1: "a∈G" "b∈G"
shows "a⋅(b⋅a)¯ = b¯"
proof -
from A1 have "(b⋅a)¯ = a¯⋅b¯" "b¯ ∈ G"
using group_inv_of_two inverse_in_group by auto
with A1 show "a⋅(b⋅a)¯ = b¯" using inv_cancel_two
by simp
qed
text‹ Some other identities with three element and cancelling. ›
lemma (in group0) cancel_middle:
assumes "a∈G" "b∈G" "c∈G"
shows
"(a⋅b)¯⋅(a⋅c) = b¯⋅c"
"(a⋅b)⋅(c⋅b)¯ = a⋅c¯"
"a¯⋅(a⋅b⋅c)⋅c¯ = b"
"a⋅(b⋅c¯)⋅c = a⋅b"
"a⋅b¯⋅(b⋅c¯) = a⋅c¯"
proof -
from assms have "(a⋅b)¯⋅(a⋅c) = b¯⋅(a¯⋅(a⋅c))"
using group_inv_of_two inverse_in_group group_oper_assoc group_op_closed by auto
with assms(1,3) show "(a⋅b)¯⋅(a⋅c) = b¯⋅c" using inv_cancel_two(3) by simp
from assms have "(a⋅b)⋅(c⋅b)¯ = a⋅(b⋅(b¯⋅c¯))"
using group_inv_of_two inverse_in_group group_oper_assoc group_op_closed by auto
with assms show "(a⋅b)⋅(c⋅b)¯ =a⋅c¯" using inverse_in_group inv_cancel_two(4) by simp
from assms have "a¯⋅(a⋅b⋅c)⋅c¯ = (a¯⋅a)⋅b⋅(c⋅c¯)"
using inverse_in_group group_oper_assoc group_op_closed by auto
with assms show "a¯⋅(a⋅b⋅c)⋅c¯ = b" using group0_2_L6 group0_2_L2 by simp
from assms have "a⋅(b⋅c¯)⋅c = a⋅b⋅(c¯⋅c)" using inverse_in_group group_oper_assoc group_op_closed
by simp
with assms show "a⋅(b⋅c¯)⋅c = a⋅b" using group_op_closed group0_2_L6 group0_2_L2 by simp
from assms have "a⋅b¯⋅(b⋅c¯) = a⋅(b¯⋅b)⋅c¯" using inverse_in_group group_oper_assoc group_op_closed
by simp
with assms show "a⋅b¯⋅(b⋅c¯) = a⋅c¯" using group0_2_L6 group0_2_L2 by simp
qed
text‹Adding a neutral element to a set that is
closed under the group operation results in a set that is closed under the
group operation.›
lemma (in group0) group0_2_L17:
assumes "H⊆G"
and "H {is closed under} P"
shows "(H ∪ {𝟭}) {is closed under} P"
using assms IsOpClosed_def group0_2_L2 by auto
text‹We can put an element on the other side of an equation.›
lemma (in group0) group0_2_L18:
assumes A1: "a∈G" "b∈G"
and A2: "c = a⋅b"
shows "c⋅b¯ = a" "a¯⋅c = b"
proof-
from A2 A1 have "c⋅b¯ = a⋅(b⋅b¯)" "a¯⋅c = (a¯⋅a)⋅b"
using inverse_in_group group_oper_assoc by auto
moreover from A1 have "a⋅(b⋅b¯) = a" "(a¯⋅a)⋅b = b"
using group0_2_L6 group0_2_L2 by auto
ultimately show "c⋅b¯ = a" "a¯⋅c = b"
by auto
qed
text‹ We can cancel an element on the right from both sides of an equation. ›
lemma (in group0) cancel_right: assumes "a∈G" "b∈G" "c∈G" "a⋅b = c⋅b"
shows "a = c"
proof -
from assms(4) have "a⋅b⋅b¯ = c⋅b⋅b¯" by simp
with assms(1,2,3) show ?thesis using inv_cancel_two(2) by simp
qed
text‹ We can cancel an element on the left from both sides of an equation. ›
lemma (in group0) cancel_left: assumes "a∈G" "b∈G" "c∈G" "a⋅b = a⋅c"
shows "b=c"
proof -
from assms(4) have "a¯⋅(a⋅b) = a¯⋅(a⋅c)" by simp
with assms(1,2,3) show ?thesis using inv_cancel_two(3) by simp
qed
text‹Multiplying different group elements by the same factor results
in different group elements.›
lemma (in group0) group0_2_L19:
assumes A1: "a∈G" "b∈G" "c∈G" and A2: "a≠b"
shows "a⋅c ≠ b⋅c" and "c⋅a ≠ c⋅b"
proof -
{ assume "a⋅c = b⋅c ∨ c⋅a =c⋅b"
then have "a⋅c⋅c¯ = b⋅c⋅c¯ ∨ c¯⋅(c⋅a) = c¯⋅(c⋅b)"
by auto
with A1 A2 have False using inv_cancel_two by simp
} then show "a⋅c ≠ b⋅c" and "c⋅a ≠ c⋅b" by auto
qed
subsection‹Subgroups›
text‹There are two common ways to define subgroups. One requires that the
group operation is closed in the subgroup. The second one defines subgroup
as a subset of a group which is itself a group under the group operations.
We use the second approach because it results in shorter definition.
The rest of this section is devoted to proving the equivalence of these two
definitions of the notion of a subgroup.
›
text‹A pair $(H,P)$ is a subgroup if $H$ forms a group with the
operation $P$ restricted to $H\times H$. It may be surprising that
we don't require $H$ to be a subset of $G$. This however can be inferred
from the definition if the pair $(G,P)$ is a group,
see lemma ‹group0_3_L2›.›
definition
"IsAsubgroup(H,P) ≡ IsAgroup(H, restrict(P,H×H))"
text‹The group is its own subgroup.›
lemma (in group0) group_self_subgroup: shows "IsAsubgroup(G,P)"
using groupAssum group_oper_fun restrict_domain
unfolding IsAsubgroup_def by simp
text‹Formally the group operation in a subgroup is different than in the
group as they have different domains. Of course we want to use the original
operation with the associated notation in the subgroup. The next couple of
lemmas will allow for that.
The next lemma states that the neutral element of
a subgroup is in the subgroup and it is
both right and left neutral there. The notation is very ugly because
we don't want to introduce a separate notation for the subgroup operation.
›
lemma group0_3_L1:
assumes A1: "IsAsubgroup(H,f)"
and A2: "n = TheNeutralElement(H,restrict(f,H×H))"
shows "n ∈ H"
"∀h∈H. restrict(f,H×H)`⟨n,h ⟩ = h"
"∀h∈H. restrict(f,H×H)`⟨h,n⟩ = h"
proof -
let ?b = "restrict(f,H×H)"
let ?e = "TheNeutralElement(H,restrict(f,H×H))"
from A1 have "group0(H,?b)"
using IsAsubgroup_def group0_def by simp
then have I:
"?e ∈ H ∧ (∀h∈H. (?b`⟨?e,h ⟩ = h ∧ ?b`⟨h,?e⟩ = h))"
by (rule group0.group0_2_L2)
with A2 show "n ∈ H" by simp
from A2 I show "∀h∈H. ?b`⟨n,h⟩ = h" and "∀h∈H. ?b`⟨h,n⟩ = h"
by auto
qed
text‹A subgroup is contained in the group.›
lemma (in group0) group0_3_L2:
assumes A1: "IsAsubgroup(H,P)"
shows "H ⊆ G"
proof
fix h assume "h∈H"
let ?b = "restrict(P,H×H)"
let ?n = "TheNeutralElement(H,restrict(P,H×H))"
from A1 have "?b ∈ H×H→H"
using IsAsubgroup_def IsAgroup_def
IsAmonoid_def IsAssociative_def by simp
moreover from A1 ‹h∈H› have "⟨ ?n,h⟩ ∈ H×H"
using group0_3_L1 by simp
moreover from A1 ‹h∈H› have "h = ?b`⟨?n,h ⟩"
using group0_3_L1 by simp
ultimately have "⟨⟨?n,h⟩,h⟩ ∈ ?b"
using func1_1_L5A by blast
then have "⟨⟨?n,h⟩,h⟩ ∈ P" using restrict_subset by auto
moreover from groupAssum have "P:G×G→G"
using IsAgroup_def IsAmonoid_def IsAssociative_def
by simp
ultimately show "h∈G" using func1_1_L5
by blast
qed
text‹The group's neutral element (denoted $1$ in the group0 context)
is a neutral element for the subgroup with respect to the group action.›
lemma (in group0) group0_3_L3:
assumes "IsAsubgroup(H,P)"
shows "∀h∈H. 𝟭⋅h = h ∧ h⋅𝟭 = h"
using assms groupAssum group0_3_L2 group0_2_L2
by auto
text‹The neutral element of a subgroup is the same as that of the group.›
lemma (in group0) group0_3_L4: assumes A1: "IsAsubgroup(H,P)"
shows "TheNeutralElement(H,restrict(P,H×H)) = 𝟭"
proof -
let ?n = "TheNeutralElement(H,restrict(P,H×H))"
from A1 have "?n ∈ H" using group0_3_L1 by simp
with groupAssum A1 have "?n∈G" using group0_3_L2 by auto
with A1 ‹?n ∈ H› show ?thesis using
group0_3_L1 restrict_if group0_2_L7 by simp
qed
text‹The neutral element of the group (denoted $1$ in the group0 context)
belongs to every subgroup.›
lemma (in group0) group0_3_L5: assumes A1: "IsAsubgroup(H,P)"
shows "𝟭 ∈ H"
proof -
from A1 show "𝟭∈H" using group0_3_L1 group0_3_L4
by fast
qed
text‹Subgroups are closed with respect to the group operation.›
lemma (in group0) group0_3_L6: assumes A1: "IsAsubgroup(H,P)"
and A2: "a∈H" "b∈H"
shows "a⋅b ∈ H"
proof -
let ?f = "restrict(P,H×H)"
from A1 have "monoid0(H,?f)" using
IsAsubgroup_def IsAgroup_def monoid0_def by simp
with A2 have "?f` (⟨a,b⟩) ∈ H" using monoid0.group0_1_L1
by blast
with A2 show "a⋅b ∈ H" using restrict_if by simp
qed
text‹A preliminary lemma that we need to show that taking the inverse
in the subgroup is the same as taking the inverse
in the group.›
lemma group0_3_L7A:
assumes A1: "IsAgroup(G,f)"
and A2: "IsAsubgroup(H,f)" and A3: "g = restrict(f,H×H)"
shows "GroupInv(G,f) ∩ H×H = GroupInv(H,g)"
proof -
let ?e = "TheNeutralElement(G,f)"
let ?e⇩1 = "TheNeutralElement(H,g)"
from A1 have "group0(G,f)" using group0_def by simp
from A2 A3 have "group0(H,g)"
using IsAsubgroup_def group0_def by simp
from ‹group0(G,f)› A2 A3 have "GroupInv(G,f) = f-``{?e⇩1}"
using group0.group0_3_L4 group0.group0_2_T3
by simp
moreover have "g-``{?e⇩1} = f-``{?e⇩1} ∩ H×H"
proof -
from A1 have "f ∈ G×G→G"
using IsAgroup_def IsAmonoid_def IsAssociative_def
by simp
moreover from A2 ‹group0(G,f)› have "H×H ⊆ G×G"
using group0.group0_3_L2 by auto
ultimately show "g-``{?e⇩1} = f-``{?e⇩1} ∩ H×H"
using A3 func1_2_L1 by simp
qed
moreover from A3 ‹group0(H,g)› have "GroupInv(H,g) = g-``{?e⇩1}"
using group0.group0_2_T3 by simp
ultimately show ?thesis by simp
qed
text‹Using the lemma above we can show the actual statement:
taking the inverse in the subgroup is the same as taking the inverse
in the group.›
theorem (in group0) group0_3_T1:
assumes A1: "IsAsubgroup(H,P)"
and A2: "g = restrict(P,H×H)"
shows "GroupInv(H,g) = restrict(GroupInv(G,P),H)"
proof -
from groupAssum have "GroupInv(G,P) : G→G"
using group0_2_T2 by simp
moreover from A1 A2 have "GroupInv(H,g) : H→H"
using IsAsubgroup_def group0_2_T2 by simp
moreover from A1 have "H ⊆ G"
using group0_3_L2 by simp
moreover from groupAssum A1 A2 have
"GroupInv(G,P) ∩ H×H = GroupInv(H,g)"
using group0_3_L7A by simp
ultimately show ?thesis
using func1_2_L3 by simp
qed
text‹A sligtly weaker, but more convenient in applications,
reformulation of the above theorem.›
theorem (in group0) group0_3_T2:
assumes "IsAsubgroup(H,P)"
and "g = restrict(P,H×H)"
shows "∀h∈H. GroupInv(H,g)`(h) = h¯"
using assms group0_3_T1 restrict_if by simp
text‹Subgroups are closed with respect to taking the group inverse.›
theorem (in group0) group0_3_T3A:
assumes A1: "IsAsubgroup(H,P)" and A2: "h∈H"
shows "h¯∈ H"
proof -
let ?g = "restrict(P,H×H)"
from A1 have "GroupInv(H,?g) ∈ H→H"
using IsAsubgroup_def group0_2_T2 by simp
with A2 have "GroupInv(H,?g)`(h) ∈ H"
using apply_type by simp
with A1 A2 show "h¯∈ H" using group0_3_T2 by simp
qed
text‹The next theorem states that a nonempty subset of
a group $G$ that is closed under the group operation and
taking the inverse is a subgroup of the group.›
theorem (in group0) group0_3_T3:
assumes A1: "H≠0"
and A2: "H⊆G"
and A3: "H {is closed under} P"
and A4: "∀x∈H. x¯ ∈ H"
shows "IsAsubgroup(H,P)"
proof -
let ?g = "restrict(P,H×H)"
let ?n = "TheNeutralElement(H,?g)"
from A3 have I: "∀x∈H.∀y∈H. x⋅y ∈ H"
using IsOpClosed_def by simp
from A1 obtain x where "x∈H" by auto
with A4 I A2 have "𝟭∈H"
using group0_2_L6 by blast
with A3 A2 have T2: "IsAmonoid(H,?g)"
using monoid.group0_1_T1
by simp
moreover have "∀h∈H.∃b∈H. ?g`⟨h,b⟩ = ?n"
proof
fix h assume "h∈H"
with A4 A2 have "h⋅h¯ = 𝟭"
using group0_2_L6 by auto
moreover from groupAssum A2 A3 ‹𝟭∈H› have "𝟭 = ?n"
using IsAgroup_def group0_1_L6 by auto
moreover from A4 ‹h∈H› have "?g`⟨h,h¯⟩ = h⋅h¯"
using restrict_if by simp
ultimately have "?g`⟨h,h¯⟩ = ?n" by simp
with A4 ‹h∈H› show "∃b∈H. ?g`⟨h,b⟩ = ?n" by auto
qed
ultimately show "IsAsubgroup(H,P)" using
IsAsubgroup_def IsAgroup_def by simp
qed
text‹The singleton with the neutral element is a subgroup.›
corollary (in group0) unit_singl_subgr:
shows "IsAsubgroup({𝟭},P)"
using group0_2_L2 group_inv_of_one group0_3_T3
unfolding IsOpClosed_def
by auto
text‹Intersection of subgroups is a subgroup. This lemma is obsolete and should be replaced by
‹subgroup_inter›. ›
lemma group0_3_L7:
assumes A1: "IsAgroup(G,f)"
and A2: "IsAsubgroup(H⇩1,f)"
and A3: "IsAsubgroup(H⇩2,f)"
shows "IsAsubgroup(H⇩1∩H⇩2,restrict(f,H⇩1×H⇩1))"
proof -
let ?e = "TheNeutralElement(G,f)"
let ?g = "restrict(f,H⇩1×H⇩1)"
from A1 have I: "group0(G,f)"
using group0_def by simp
from A2 have "group0(H⇩1,?g)"
using IsAsubgroup_def group0_def by simp
moreover have "H⇩1∩H⇩2 ≠ 0"
proof -
from A1 A2 A3 have "?e ∈ H⇩1∩H⇩2"
using group0_def group0.group0_3_L5 by simp
thus ?thesis by auto
qed
moreover have "H⇩1∩H⇩2 ⊆ H⇩1" by auto
moreover from A2 A3 I ‹H⇩1∩H⇩2 ⊆ H⇩1› have
"H⇩1∩H⇩2 {is closed under} ?g"
using group0.group0_3_L6 IsOpClosed_def
func_ZF_4_L7 func_ZF_4_L5 by simp
moreover from A2 A3 I have
"∀x ∈ H⇩1∩H⇩2. GroupInv(H⇩1,?g)`(x) ∈ H⇩1∩H⇩2"
using group0.group0_3_T2 group0.group0_3_T3A
by simp
ultimately show ?thesis
using group0.group0_3_T3 by simp
qed
text‹Intersection of subgroups is a subgroup.›
lemma (in group0) subgroup_inter: assumes "ℋ≠0"
and "∀H∈ℋ. IsAsubgroup(H,P)"
shows "IsAsubgroup(⋂ℋ,P)"
proof -
{
fix H assume "H:ℋ"
with assms(2) have "𝟭:H" using group0_3_L5 by auto
}
then have "⋂ℋ ≠ 0" using assms(1) by auto moreover
{
fix t assume "t:⋂ℋ"
then have "∀H∈ℋ. t:H" by auto
with assms have "t:G" using group0_3_L2 by blast
}
then have "⋂ℋ ⊆ G" by auto moreover
{
fix x y assume xy:"x:⋂ℋ" "y:⋂ℋ"
{
fix J assume J:"J:ℋ"
with xy have "x:J" "y:J" by auto
with J have "P`⟨x,y⟩:J" using assms(2) group0_3_L6 by auto
}
then have "P`⟨x,y⟩:⋂ℋ" using assms(1) by auto
}
then have "⋂ℋ {is closed under} P" unfolding IsOpClosed_def by simp
moreover
{
fix x assume x:"x:⋂ℋ"
{
fix J assume J:"J:ℋ"
with x have "x:J" by auto
with J assms(2) have "x¯ ∈ J" using group0_3_T3A by auto
}
then have "x¯ ∈ ⋂ℋ" using assms(1) by auto
}
then have "∀x ∈ ⋂ℋ. x¯ ∈ ⋂ℋ" by simp
ultimately show ?thesis using group0_3_T3 by auto
qed
text‹The range of the subgroup operation is the whole subgroup.›
lemma image_subgr_op: assumes A1: "IsAsubgroup(H,P)"
shows "restrict(P,H×H)``(H×H) = H"
proof -
from A1 have "monoid0(H,restrict(P,H×H))"
using IsAsubgroup_def IsAgroup_def monoid0_def
by simp
then show ?thesis by (rule monoid0.range_carr)
qed
text‹If we restrict the inverse to a subgroup, then the restricted
inverse is onto the subgroup.›
lemma (in group0) restr_inv_onto: assumes A1: "IsAsubgroup(H,P)"
shows "restrict(GroupInv(G,P),H)``(H) = H"
proof -
from A1 have "GroupInv(H,restrict(P,H×H))``(H) = H"
using IsAsubgroup_def group0_def group0.group_inv_surj
by simp
with A1 show ?thesis using group0_3_T1 by simp
qed
text‹A union of two subgroups is a subgroup iff
one of the subgroups is a subset of the other subgroup.›
lemma (in group0) union_subgroups:
assumes "IsAsubgroup(H⇩1,P)" and "IsAsubgroup(H⇩2,P)"
shows "IsAsubgroup(H⇩1∪H⇩2,P) ⟷ (H⇩1⊆H⇩2 ∨ H⇩2⊆H⇩1)"
proof
assume "H⇩1⊆H⇩2 ∨ H⇩2⊆H⇩1" show "IsAsubgroup(H⇩1∪H⇩2,P)"
proof -
from ‹H⇩1⊆H⇩2 ∨ H⇩2⊆H⇩1› have "H⇩2 = H⇩1∪H⇩2 ∨ H⇩1 = H⇩1∪H⇩2" by auto
with assms show "IsAsubgroup(H⇩1∪H⇩2,P)" by auto
qed
next
assume "IsAsubgroup(H⇩1∪H⇩2, P)" show "H⇩1⊆H⇩2 ∨ H⇩2⊆H⇩1"
proof -
{ assume "¬ H⇩1⊆H⇩2"
then obtain x where "x∈H⇩1" and "x∉H⇩2" by auto
with assms(1) have "x¯ ∈ H⇩1" using group0_3_T3A by simp
{ fix y assume "y∈H⇩2"
let ?z = "x⋅y"
from ‹x∈H⇩1› ‹y∈H⇩2› have "x ∈ H⇩1∪H⇩2" and "y ∈ H⇩1∪H⇩2" by auto
with ‹IsAsubgroup(H⇩1∪H⇩2,P)› have "?z ∈ H⇩1∪H⇩2" using group0_3_L6 by blast
from assms ‹x ∈ H⇩1∪H⇩2› ‹y∈H⇩2› have "x∈G" "y∈G" and "y¯∈H⇩2"
using group0_3_T3A group0_3_L2 by auto
then have "?z⋅y¯ = x" and "x¯⋅?z = y" using inv_cancel_two(2,3) by auto
{ assume "?z ∈ H⇩2"
with ‹IsAsubgroup(H⇩2,P)› ‹y¯∈H⇩2› have "?z⋅y¯ ∈ H⇩2" using group0_3_L6 by simp
with ‹?z⋅y¯ = x› ‹x∉H⇩2› have False by auto
} hence "?z ∉ H⇩2" by auto
with assms(1) ‹x¯ ∈ H⇩1› ‹?z ∈ H⇩1∪H⇩2› have "x¯⋅?z ∈ H⇩1" using group0_3_L6 by simp
with ‹x¯⋅?z = y› have "y∈H⇩1" by simp
} hence "H⇩2⊆H⇩1" by blast
} thus ?thesis by blast
qed
qed
text‹Transitivity for "is a subgroup of" relation. The proof (probably) uses the lemma
‹restrict_restrict› from standard Isabelle/ZF library which states that
‹restrict(restrict(f,A),B) = restrict(f,A∩B)›. That lemma is added to the simplifier, so it does
not have to be referenced explicitly in the proof below. ›
lemma subgroup_transitive:
assumes "IsAgroup(G⇩3,P)" "IsAsubgroup(G⇩2,P)" "IsAsubgroup(G⇩1,restrict(P,G⇩2×G⇩2))"
shows "IsAsubgroup(G⇩1,P)"
proof -
from assms(2) have "group0(G⇩2,restrict(P,G⇩2×G⇩2))" unfolding IsAsubgroup_def group0_def by simp
with assms(3) have "G⇩1⊆G⇩2" using group0.group0_3_L2 by simp
hence "G⇩2×G⇩2 ∩ G⇩1×G⇩1 = G⇩1×G⇩1" by auto
with assms(3) show "IsAsubgroup(G⇩1,P)" unfolding IsAsubgroup_def by simp
qed
subsection‹Groups vs. loops›
text‹We defined groups as monoids with the inverse operation. An alternative way of defining a group
is as a loop whose operation is associative. ›
text‹ Groups have left and right division. ›
lemma (in group0) gr_has_lr_div: shows "HasLeftDiv(G,P)" and "HasRightDiv(G,P)"
proof -
{ fix x y assume "x∈G" "y∈G"
then have "x¯⋅y ∈ G ∧ x⋅(x¯⋅y) = y" using group_op_closed inverse_in_group inv_cancel_two(4)
by simp
hence "∃z. z∈G ∧ x⋅z =y" by auto
moreover
{ fix z⇩1 z⇩2 assume "z⇩1∈G ∧ x⋅z⇩1 =y" and "z⇩2∈G ∧ x⋅z⇩2 =y"
with ‹x∈G› have "z⇩1 = z⇩2" using cancel_left by blast
}
ultimately have "∃!z. z∈G ∧ x⋅z =y" by auto
} then show "HasLeftDiv(G,P)" unfolding HasLeftDiv_def by simp
{ fix x y assume "x∈G" "y∈G"
then have "y⋅x¯ ∈ G ∧ (y⋅x¯)⋅x = y" using group_op_closed inverse_in_group inv_cancel_two(1)
by simp
hence "∃z. z∈G ∧ z⋅x =y" by auto
moreover
{ fix z⇩1 z⇩2 assume "z⇩1∈G ∧ z⇩1⋅x =y" and "z⇩2∈G ∧ z⇩2⋅x =y"
with ‹x∈G› have "z⇩1 = z⇩2" using cancel_right by blast
}
ultimately have "∃!z. z∈G ∧ z⋅x =y" by auto
} then show "HasRightDiv(G,P)" unfolding HasRightDiv_def by simp
qed
text‹A group is a quasigroup and a loop.›
lemma (in group0) group_is_loop: shows "IsAquasigroup(G,P)" and "IsAloop(G,P)"
proof -
show "IsAquasigroup(G,P)" unfolding IsAquasigroup_def HasLatinSquareProp_def
using gr_has_lr_div group_oper_fun by simp
then show "IsAloop(G,P)" unfolding IsAloop_def using group0_2_L2 by auto
qed
text‹ An associative loop is a group.›
theorem assoc_loop_is_gr: assumes "IsAloop(G,P)" and "P {is associative on} G"
shows "IsAgroup(G,P)"
proof -
from assms(1) have "∃e∈G. ∀x∈G. P`⟨e,x⟩ = x ∧ P`⟨x,e⟩ = x"
unfolding IsAloop_def by simp
with assms(2) have "IsAmonoid(G,P)" unfolding IsAmonoid_def by simp
{ fix x assume "x∈G"
let ?y = "RightInv(G,P)`(x)"
from assms(1) ‹x∈G› have "?y ∈ G" and "P`⟨x,?y⟩ = TheNeutralElement(G,P)"
using loop_loop0_valid loop0.lr_inv_props(3,4) by auto
hence "∃y∈G. P`⟨x,y⟩ = TheNeutralElement(G,P)" by auto
}
with ‹IsAmonoid(G,P)› show "IsAgroup(G,P)" unfolding IsAgroup_def by simp
qed
text‹For groups the left and right inverse are the same as the group inverse. ›
lemma (in group0) lr_inv_gr_inv:
shows "LeftInv(G,P) = GroupInv(G,P)" and "RightInv(G,P) = GroupInv(G,P)"
proof -
have "LeftInv(G,P):G→G" using group_is_loop loop_loop0_valid loop0.lr_inv_fun(1)
by simp
moreover from groupAssum have "GroupInv(G,P):G→G" using group0_2_T2 by simp
moreover
{ fix x assume "x∈G"
let ?y = "LeftInv(G,P)`(x)"
from ‹x∈G› have "?y ∈ G" and "?y⋅x = 𝟭"
using group_is_loop(2) loop_loop0_valid loop0.lr_inv_props(1,2) by auto
with ‹x∈G› have "LeftInv(G,P)`(x) = GroupInv(G,P)`(x)" using group0_2_L9(1) by simp
}
ultimately show "LeftInv(G,P) = GroupInv(G,P)" using func_eq by blast
have "RightInv(G,P):G→G" using group_is_loop loop_loop0_valid loop0.lr_inv_fun(2)
by simp
moreover from groupAssum have "GroupInv(G,P):G→G" using group0_2_T2 by simp
moreover
{ fix x assume "x∈G"
let ?y = "RightInv(G,P)`(x)"
from ‹x∈G› have "?y ∈ G" and "x⋅?y = 𝟭"
using group_is_loop(2) loop_loop0_valid loop0.lr_inv_props(3,4) by auto
with ‹x∈G› have "RightInv(G,P)`(x) = GroupInv(G,P)`(x)" using group0_2_L9(2) by simp
}
ultimately show "RightInv(G,P) = GroupInv(G,P)" using func_eq by blast
qed
end