IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Group_ZF imports Monoid_ZF
begin

This theory file covers basics of group theory.

Definition and basic properties of groups

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.

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

\( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)

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

\( \text{GroupInv}(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = \text{ TheNeutralElement}(G,f)\} \)

We will use the miltiplicative notation for groups. The neutral element is denoted \(1\).

locale group0

assumes groupAssum: \( \text{IsAgroup}(G,P) \)

defines \( 1 \equiv \text{ TheNeutralElement}(G,P) \)

defines \( a \cdot b \equiv P\langle a,b\rangle \)

defines \( x^{-1} \equiv \text{GroupInv}(G,P)(x) \)

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

The theorems proven in the monoid context are valid in the group0 context.

sublocale group0 < monoid: monoid0

unfolding groper_def using group0_2_L1

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 \( \text{IsAmonoid}(G,f) \) and \( \forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f) \)

shows \( \text{IsAgroup}(G,f) \) using assms, IsAgroup_def

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 \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \) using group0_2_L1, unit_is_neutral

The group is closed under the group operation. Used all the time, useful to have handy.

lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \) using assms, group0_1_L1

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\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \) using groupAssum, assms, IsAgroup_def, IsAmonoid_def, IsAssociative_def, group_op_closed

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\times G\rightarrow G \) using groupAssum, IsAgroup_def, IsAmonoid_def, IsAssociative_def

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\in G \) and A2: \( b\in G \) and A3: \( g\cdot b = 1 \)

shows \( b\cdot g = 1 \)proof
from A2, groupAssum obtain \( c \) where I: \( c \in G \wedge b\cdot c = 1 \) using IsAgroup_def
then have \( c\in G \)
have \( 1 \in G \) using group0_2_L2
with A1, A2, I have \( b\cdot g = b\cdot (g\cdot (b\cdot c)) \) using group_op_closed, group0_2_L2, group_oper_assoc
also
from A1, A2, \( c\in G \) have \( b\cdot (g\cdot (b\cdot c)) = b\cdot (g\cdot b\cdot c) \) using group_oper_assoc
also
from A3, A2, I have \( b\cdot (g\cdot b\cdot c)= 1 \) using group0_2_L2
finally show \( b\cdot g = 1 \)
qed

For every element of a group there is only one inverse.

lemma (in group0) group0_2_L4:

assumes A1: \( x\in G \)

shows \( \exists !y.\ y\in G \wedge x\cdot y = 1 \)proof
from A1, groupAssum show \( \exists y.\ y\in G \wedge x\cdot y = 1 \) using IsAgroup_def
fix \( y \) \( n \)
assume A2: \( y\in G \wedge x\cdot y = 1 \) and A3: \( n\in G \wedge x\cdot n = 1 \)
show \( y=n \)proof
from A1, A2 have T1: \( y\cdot x = 1 \) using group0_2_T1
from A2, A3 have \( y = y\cdot (x\cdot n) \) using group0_2_L2
also
from A1, A2, A3 have \( \ldots = (y\cdot x)\cdot n \) using group_oper_assoc
also
from T1, A3 have \( \ldots = n \) using group0_2_L2
finally show \( y=n \)
qed
qed

The group inverse is a function that maps G into G.

theorem group0_2_T2:

assumes A1: \( \text{IsAgroup}(G,f) \)

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)proof
have \( \text{GroupInv}(G,f) \subseteq G\times G \) using GroupInv_def
moreover
from A1 have \( \forall x\in G.\ \exists !y.\ y\in G \wedge \langle x,y\rangle \in \text{GroupInv}(G,f) \) using group0_def, group0_2_L4, GroupInv_def
ultimately show \( thesis \) using func1_1_L11
qed

We can think about the group inverse (the function) as the inverse image of the neutral element. Recall that in Isabelle \( f^{-1}(A) \) denotes the inverse image of the set \(A\).

theorem (in group0) group0_2_T3:

shows \( P^{-1}\{1 \} = \text{GroupInv}(G,P) \)proof
from groupAssum have \( P : G\times G \rightarrow G \) using IsAgroup_def, IsAmonoid_def, IsAssociative_def
then show \( P^{-1}\{1 \} = \text{GroupInv}(G,P) \) using func1_1_L14, GroupInv_def
qed

The inverse is in the group.

lemma (in group0) inverse_in_group:

assumes A1: \( x\in G \)

shows \( x^{-1}\in G \)proof
from groupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using group0_2_T2
with A1 show \( thesis \) using apply_type
qed

The notation for the inverse means what it is supposed to mean.

lemma (in group0) group0_2_L6:

assumes A1: \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)proof
from groupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using group0_2_T2
with A1 have \( \langle x,x^{-1}\rangle \in \text{GroupInv}(G,P) \) using apply_Pair
then show \( x\cdot x^{-1} = 1 \) using GroupInv_def
with A1 show \( x^{-1}\cdot x = 1 \) using inverse_in_group, group0_2_T1
qed

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\in G \) and A2: \( b\in G \) and A3: \( a\cdot b = a \)

shows \( b=1 \)proof
from A3 have \( a^{-1} \cdot (a\cdot b) = a^{-1}\cdot a \)
with A1, A2 show \( thesis \) using inverse_in_group, group_oper_assoc, group0_2_L6, group0_2_L2
qed

See the comment to group0_2_L7.

lemma (in group0) group0_2_L8:

assumes A1: \( a\in G \) and A2: \( b\in G \) and A3: \( a\cdot b = b \)

shows \( a=1 \)proof
from A3 have \( (a\cdot b)\cdot b^{-1} = b\cdot b^{-1} \)
with A1, A2 have \( a\cdot (b\cdot b^{-1}) = b\cdot b^{-1} \) using inverse_in_group, group_oper_assoc
with A1, A2 show \( thesis \) using group0_2_L6, group0_2_L2
qed

The inverse of the neutral element is the neutral element.

lemma (in group0) group_inv_of_one:

shows \( 1 ^{-1} = 1 \) using group0_2_L2, inverse_in_group, group0_2_L6, group0_2_L7

if \(a^{-1} = 1\), then \(a=1\).

lemma (in group0) group0_2_L8A:

assumes A1: \( a\in G \) and A2: \( a^{-1} = 1 \)

shows \( a = 1 \)proof
from A1 have \( a\cdot a^{-1} = 1 \) using group0_2_L6
with A1, A2 show \( a = 1 \) using group0_2_L2
qed

If \(a\) is not a unit, then its inverse is not a unit either.

lemma (in group0) group0_2_L8B:

assumes \( a\in G \) and \( a \neq 1 \)

shows \( a^{-1} \neq 1 \) using assms, group0_2_L8A

If \(a^{-1}\) is not a unit, then a is not a unit either.

lemma (in group0) group0_2_L8C:

assumes \( a\in G \) and \( a^{-1} \neq 1 \)

shows \( a\neq 1 \) using assms, group0_2_L8A, group_inv_of_one

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\in G \) and A2: \( b\in G \) and A3: \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)proof
from A3 have \( a\cdot b\cdot b^{-1} = 1 \cdot b^{-1} \)
with A1, A2 have \( a\cdot (b\cdot b^{-1}) = 1 \cdot b^{-1} \) using inverse_in_group, group_oper_assoc
with A1, A2 show \( a = b^{-1} \) using group0_2_L6, inverse_in_group, group0_2_L2
from A3 have \( a^{-1}\cdot (a\cdot b) = a^{-1}\cdot 1 \)
with A1, A2 show \( b = a^{-1} \) using inverse_in_group, group_oper_assoc, group0_2_L6, group0_2_L2
qed

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: \( \forall g\in G.\ b(g) \in G \wedge g\cdot b(g) = 1 \)

shows \( \forall g\in G.\ b(g) = g^{-1} \)proof
fix \( g \)
assume \( g\in G \)
moreover
from A1, \( g\in G \) have \( b(g) \in G \)
moreover
from A1, \( g\in G \) have \( g\cdot b(g) = 1 \)
ultimately show \( b(g) = g^{-1} \) by (rule group0_2_L9 )
qed

What is the inverse of a product?

lemma (in group0) group_inv_of_two:

assumes A1: \( a\in G \) and A2: \( b\in G \)

shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \)proof
from A1, A2 have \( b^{-1}\in G \), \( a^{-1}\in G \), \( a\cdot b\in G \), \( b^{-1}\cdot a^{-1} \in G \) using inverse_in_group, group_op_closed
from A1, A2, \( b^{-1}\cdot a^{-1} \in G \) have \( a\cdot b\cdot (b^{-1}\cdot a^{-1}) = a\cdot (b\cdot (b^{-1}\cdot a^{-1})) \) using group_oper_assoc
moreover
from A2, \( b^{-1}\in G \), \( a^{-1}\in G \) have \( b\cdot (b^{-1}\cdot a^{-1}) = b\cdot b^{-1}\cdot a^{-1} \) using group_oper_assoc
moreover
from A2, \( a^{-1}\in G \) have \( b\cdot b^{-1}\cdot a^{-1} = a^{-1} \) using group0_2_L6, group0_2_L2
ultimately have \( a\cdot b\cdot (b^{-1}\cdot a^{-1}) = a\cdot a^{-1} \)
with A1 have \( a\cdot b\cdot (b^{-1}\cdot a^{-1}) = 1 \) using group0_2_L6
with \( a\cdot b \in G \), \( b^{-1}\cdot a^{-1} \in G \) show \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \) using group0_2_L9
qed

What is the inverse of a product of three elements?

lemma (in group0) group_inv_of_three:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1} \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1}) \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1} \)proof
from A1 have T: \( a\cdot b \in G \), \( a^{-1} \in G \), \( b^{-1} \in G \), \( c^{-1} \in G \) using group_op_closed, inverse_in_group
with A1 show \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1} \) and \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1}) \) using group_inv_of_two
with T show \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1} \) using group_oper_assoc
qed

The inverse of the inverse is the element.

lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \) using assms, inverse_in_group, group0_2_L6, group0_2_L9

Group inverse is nilpotent, therefore a bijection and involution.

lemma (in group0) group_inv_bij:

shows \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P) = id(G) \) and \( \text{GroupInv}(G,P) \in \text{bij}(G,G) \) and \( \text{GroupInv}(G,P) = converse( \text{GroupInv}(G,P)) \)proof
have I: \( \text{GroupInv}(G,P): G\rightarrow G \) using groupAssum, group0_2_T2
then have \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P): G\rightarrow G \) and \( id(G):G\rightarrow G \) using comp_fun, id_type
moreover {
fix \( g \)
assume \( g\in G \)
with I have \( ( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P))(g) = id(G)(g) \) using comp_fun_apply, group_inv_of_inv, id_conv
}
hence \( \forall g\in G.\ ( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P))(g) = id(G)(g) \)
ultimately show \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P) = id(G) \) by (rule func_eq )
with I show \( \text{GroupInv}(G,P) \in \text{bij}(G,G) \) using nilpotent_imp_bijective
with \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P) = id(G) \) show \( \text{GroupInv}(G,P) = converse( \text{GroupInv}(G,P)) \) using comp_id_conv
qed

A set comprehension form of the image of a set under the group inverse.

lemma (in group0) ginv_image:

assumes \( V\subseteq G \)

shows \( \text{GroupInv}(G,P)(V) \subseteq G \) and \( \text{GroupInv}(G,P)(V) = \{g^{-1}.\ g \in V\} \)proof
from assms have I: \( \text{GroupInv}(G,P)(V) = \{ \text{GroupInv}(G,P)(g).\ g\in V\} \) using groupAssum, group0_2_T2, func_imagedef
thus \( \text{GroupInv}(G,P)(V) = \{g^{-1}.\ g \in V\} \)
show \( \text{GroupInv}(G,P)(V) \subseteq G \) using groupAssum, group0_2_T2, func1_1_L6(2)
qed

Inverse of an element that belongs to the inverse of the set belongs to the set.

lemma (in group0) ginv_image_el:

assumes \( V\subseteq G \), \( g \in \text{GroupInv}(G,P)(V) \)

shows \( g^{-1} \in V \) using assms, ginv_image, group_inv_of_inv

For the group inverse the image is the same as inverse image.

lemma (in group0) inv_image_vimage:

shows \( \text{GroupInv}(G,P)(V) = \text{GroupInv}(G,P)^{-1}(V) \) using group_inv_bij, vimage_converse

If the unit is in a set then it is in the inverse of that set.

lemma (in group0) neut_inv_neut:

assumes \( A\subseteq G \) and \( 1 \in A \)

shows \( 1 \in \text{GroupInv}(G,P)(A) \)proof
have \( \text{GroupInv}(G,P):G\rightarrow G \) using groupAssum, group0_2_T2
with assms have \( 1 ^{-1} \in \text{GroupInv}(G,P)(A) \) using func_imagedef
then show \( thesis \) using group_inv_of_one
qed

The group inverse is onto.

lemma (in group0) group_inv_surj:

shows \( \text{GroupInv}(G,P)(G) = G \) using group_inv_bij, bij_def, surj_range_image_domain

If \(a^{-1}\cdot b=1\), then \(a=b\).

lemma (in group0) group0_2_L11:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a^{-1}\cdot b = 1 \)

shows \( a=b \)proof
from A1, A2 have \( a^{-1} \in G \), \( b\in G \), \( a^{-1}\cdot b = 1 \) using inverse_in_group
then have \( b = (a^{-1})^{-1} \) by (rule group0_2_L9 )
with A1 show \( a=b \) using group_inv_of_inv
qed

If \(a\cdot b^{-1}=1\), then \(a=b\).

lemma (in group0) group0_2_L11A:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} = 1 \)

shows \( a=b \)proof
from A1, A2 have \( a \in G \), \( b^{-1}\in G \), \( a\cdot b^{-1} = 1 \) using inverse_in_group
then have \( a = (b^{-1})^{-1} \) by (rule group0_2_L9 )
with A1 show \( a=b \) using group_inv_of_inv
qed

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\in G \) and A2: \( b^{-1} \neq a \)

shows \( a^{-1} \neq b \)proof
{
assume \( a^{-1} = b \)
then have \( (a^{-1})^{-1} = b^{-1} \)
with A1, A2 have \( False \) using group_inv_of_inv
}
then show \( a^{-1} \neq b \)
qed

What is the inverse of \(ab^{-1}\) ?

lemma (in group0) group0_2_L12:

assumes A1: \( a\in G \), \( b\in G \)

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)proof
from A1 have \( (a\cdot b^{-1})^{-1} = (b^{-1})^{-1}\cdot a^{-1} \) and \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot (a^{-1})^{-1} \) using inverse_in_group, group_inv_of_two
with A1 show \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \) using group_inv_of_inv
qed

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\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)proof
from A1 have T: \( a^{-1} \in G \), \( b^{-1}\in G \), \( c^{-1}\in G \), \( a^{-1}\cdot b \in G \), \( a\cdot b^{-1} \in G \), \( a\cdot b \in G \), \( c\cdot b^{-1} \in G \), \( b\cdot c \in G \) using inverse_in_group, group_op_closed
from A1, T have \( a\cdot c^{-1} = a\cdot (b^{-1}\cdot b)\cdot c^{-1} \), \( a^{-1}\cdot c = a^{-1}\cdot (b\cdot b^{-1})\cdot c \) using group0_2_L2, group0_2_L6
with A1, T show \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \) using group_oper_assoc
from A1 have \( a\cdot (b\cdot c)^{-1} = a\cdot (c^{-1}\cdot b^{-1}) \) using group_inv_of_two
with A1, T show \( a\cdot (b\cdot c)^{-1} =a\cdot c^{-1}\cdot b^{-1} \) using group_oper_assoc
from A1, T show \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \) using group_oper_assoc
from A1, T show \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \) using group_inv_of_three, group_inv_of_inv
from T have \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a\cdot b\cdot (c^{-1}\cdot (c\cdot b^{-1})) \) using group_oper_assoc
also
from A1, T have \( \ldots = a\cdot b\cdot b^{-1} \) using group_oper_assoc, group0_2_L6, group0_2_L2
also
from A1, T have \( \ldots = a\cdot (b\cdot b^{-1}) \) using group_oper_assoc
also
from A1 have \( \ldots = a \) using group0_2_L6, group0_2_L2
finally show \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \)
from A1, T have \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot (b\cdot (c\cdot c^{-1})) \) using group_oper_assoc
also
from A1, T have \( \ldots = a\cdot b \) using group0_2_L6, group0_2_L2
finally show \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)
qed

A simple equation to solve

lemma (in group0) simple_equation0:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b^{-1} = c^{-1} \)

shows \( c = b\cdot a^{-1} \)proof
from assms(4) have \( (a\cdot b^{-1})^{-1} = (c^{-1})^{-1} \)
with assms(1,2,3) show \( c = b\cdot a^{-1} \) using group0_2_L12(1), group_inv_of_inv
qed

Another simple equation

lemma (in group0) simple_equation1:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a^{-1}\cdot b = c^{-1} \)

shows \( c = b^{-1}\cdot a \)proof
from assms(4) have \( (a^{-1}\cdot b)^{-1} = (c^{-1})^{-1} \)
with assms(1,2,3) show \( c = b^{-1}\cdot a \) using group0_2_L12(2), group_inv_of_inv
qed

Another lemma about rearranging a product of four group elements.

lemma (in group0) group0_2_L15:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( (a\cdot b)\cdot (c\cdot d)^{-1} = a\cdot (b\cdot d^{-1})\cdot a^{-1}\cdot (a\cdot c^{-1}) \)proof
from A1 have T1: \( d^{-1}\in G \), \( c^{-1}\in G \), \( a\cdot b\in G \), \( a\cdot (b\cdot d^{-1})\in G \) using inverse_in_group, group_op_closed
with A1 have \( (a\cdot b)\cdot (c\cdot d)^{-1} = (a\cdot b)\cdot (d^{-1}\cdot c^{-1}) \) using group_inv_of_two
also
from A1, T1 have \( \ldots = a\cdot (b\cdot d^{-1})\cdot c^{-1} \) using group_oper_assoc
also
from A1, T1 have \( \ldots = a\cdot (b\cdot d^{-1})\cdot a^{-1}\cdot (a\cdot c^{-1}) \) using group0_2_L14A
finally show \( thesis \)
qed

We can cancel an element with its inverse that is written next to it.

lemma (in group0) inv_cancel_two:

assumes A1: \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)proof
from A1 have \( a\cdot b^{-1}\cdot b = a\cdot (b^{-1}\cdot b) \), \( a\cdot b\cdot b^{-1} = a\cdot (b\cdot b^{-1}) \), \( a^{-1}\cdot (a\cdot b) = a^{-1}\cdot a\cdot b \), \( a\cdot (a^{-1}\cdot b) = a\cdot a^{-1}\cdot b \) using inverse_in_group, group_oper_assoc
with A1 show \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \) using group0_2_L6, group0_2_L2
qed

Another lemma about cancelling with two group elements.

lemma (in group0) group0_2_L16A:

assumes A1: \( a\in G \), \( b\in G \)

shows \( a\cdot (b\cdot a)^{-1} = b^{-1} \)proof
from A1 have \( (b\cdot a)^{-1} = a^{-1}\cdot b^{-1} \), \( b^{-1} \in G \) using group_inv_of_two, inverse_in_group
with A1 show \( a\cdot (b\cdot a)^{-1} = b^{-1} \) using inv_cancel_two
qed

Some other identities with three element and cancelling.

lemma (in group0) cancel_middle:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot c \), \( (a\cdot b)\cdot (c\cdot b)^{-1} = a\cdot c^{-1} \), \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = b \), \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b \), \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \)proof
from assms have \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot (a^{-1}\cdot (a\cdot c)) \) using group_inv_of_two, inverse_in_group, group_oper_assoc, group_op_closed
with assms(1,3) show \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot c \) using inv_cancel_two(3)
from assms have \( (a\cdot b)\cdot (c\cdot b)^{-1} = a\cdot (b\cdot (b^{-1}\cdot c^{-1})) \) using group_inv_of_two, inverse_in_group, group_oper_assoc, group_op_closed
with assms show \( (a\cdot b)\cdot (c\cdot b)^{-1} =a\cdot c^{-1} \) using inverse_in_group, inv_cancel_two(4)
from assms have \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = (a^{-1}\cdot a)\cdot b\cdot (c\cdot c^{-1}) \) using inverse_in_group, group_oper_assoc, group_op_closed
with assms show \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = b \) using group0_2_L6, group0_2_L2
from assms have \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b\cdot (c^{-1}\cdot c) \) using inverse_in_group, group_oper_assoc, group_op_closed
with assms show \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b \) using group_op_closed, group0_2_L6, group0_2_L2
from assms have \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot (b^{-1}\cdot b)\cdot c^{-1} \) using inverse_in_group, group_oper_assoc, group_op_closed
with assms show \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \) using group0_2_L6, group0_2_L2
qed

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\subseteq G \) and \( H \text{ is closed under } P \)

shows \( (H \cup \{1 \}) \text{ is closed under } P \) using assms, IsOpClosed_def, group0_2_L2

We can put an element on the other side of an equation.

lemma (in group0) group0_2_L18:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( c = a\cdot b \)

shows \( c\cdot b^{-1} = a \), \( a^{-1}\cdot c = b \)proof
from A2, A1 have \( c\cdot b^{-1} = a\cdot (b\cdot b^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot a)\cdot b \) using inverse_in_group, group_oper_assoc
moreover
from A1 have \( a\cdot (b\cdot b^{-1}) = a \), \( (a^{-1}\cdot a)\cdot b = b \) using group0_2_L6, group0_2_L2
ultimately show \( c\cdot b^{-1} = a \), \( a^{-1}\cdot c = b \)
qed

We can cancel an element on the right from both sides of an equation.

lemma (in group0) cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b = c\cdot b \)

shows \( a = c \)proof
from assms(4) have \( a\cdot b\cdot b^{-1} = c\cdot b\cdot b^{-1} \)
with assms(1,2,3) show \( thesis \) using inv_cancel_two(2)
qed

We can cancel an element on the left from both sides of an equation.

lemma (in group0) cancel_left:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b = a\cdot c \)

shows \( b=c \)proof
from assms(4) have \( a^{-1}\cdot (a\cdot b) = a^{-1}\cdot (a\cdot c) \)
with assms(1,2,3) show \( thesis \) using inv_cancel_two(3)
qed

Multiplying different group elements by the same factor results in different group elements.

lemma (in group0) group0_2_L19:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \) and A2: \( a\neq b \)

shows \( a\cdot c \neq b\cdot c \) and \( c\cdot a \neq c\cdot b \)proof
{
assume \( a\cdot c = b\cdot c \vee c\cdot a =c\cdot b \)
then have \( a\cdot c\cdot c^{-1} = b\cdot c\cdot c^{-1} \vee c^{-1}\cdot (c\cdot a) = c^{-1}\cdot (c\cdot b) \)
with A1, A2 have \( False \) using inv_cancel_two
}
then show \( a\cdot c \neq b\cdot c \) and \( c\cdot a \neq c\cdot b \)
qed

Subgroups

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.

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

\( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)

The group is its own subgroup.

lemma (in group0) group_self_subgroup:

shows \( \text{IsAsubgroup}(G,P) \) using groupAssum, group_oper_fun, restrict_domain unfolding IsAsubgroup_def

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: \( \text{IsAsubgroup}(H,f) \) and A2: \( n = \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) \)

shows \( n \in H \), \( \forall h\in H.\ \text{restrict}(f,H\times H)\langle n,h \rangle = h \), \( \forall h\in H.\ \text{restrict}(f,H\times H)\langle h,n\rangle = h \)proof
let \( b = \text{restrict}(f,H\times H) \)
let \( e = \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) \)
from A1 have \( group0(H,b) \) using IsAsubgroup_def, group0_def
then have I: \( e \in H \wedge (\forall h\in H.\ (b\langle e,h \rangle = h \wedge b\langle h,e\rangle = h)) \) by (rule group0_2_L2 )
with A2 show \( n \in H \)
from A2, I show \( \forall h\in H.\ b\langle n,h\rangle = h \) and \( \forall h\in H.\ b\langle h,n\rangle = h \)
qed

A subgroup is contained in the group.

lemma (in group0) group0_3_L2:

assumes A1: \( \text{IsAsubgroup}(H,P) \)

shows \( H \subseteq G \)proof
fix \( h \)
assume \( h\in H \)
let \( b = \text{restrict}(P,H\times H) \)
let \( n = \text{ TheNeutralElement}(H,\text{restrict}(P,H\times H)) \)
from A1 have \( b \in H\times H\rightarrow H \) using IsAsubgroup_def, IsAgroup_def, IsAmonoid_def, IsAssociative_def
moreover
from A1, \( h\in H \) have \( \langle n,h\rangle \in H\times H \) using group0_3_L1
moreover
from A1, \( h\in H \) have \( h = b\langle n,h \rangle \) using group0_3_L1
ultimately have \( \langle \langle n,h\rangle ,h\rangle \in b \) using func1_1_L5A
then have \( \langle \langle n,h\rangle ,h\rangle \in P \) using restrict_subset
moreover
from groupAssum have \( P:G\times G\rightarrow G \) using IsAgroup_def, IsAmonoid_def, IsAssociative_def
ultimately show \( h\in G \) using func1_1_L5
qed

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 \( \text{IsAsubgroup}(H,P) \)

shows \( \forall h\in H.\ 1 \cdot h = h \wedge h\cdot 1 = h \) using assms, groupAssum, group0_3_L2, group0_2_L2

The neutral element of a subgroup is the same as that of the group.

lemma (in group0) group0_3_L4:

assumes A1: \( \text{IsAsubgroup}(H,P) \)

shows \( \text{ TheNeutralElement}(H,\text{restrict}(P,H\times H)) = 1 \)proof
let \( n = \text{ TheNeutralElement}(H,\text{restrict}(P,H\times H)) \)
from A1 have \( n \in H \) using group0_3_L1
with groupAssum, A1 have \( n\in G \) using group0_3_L2
with A1, \( n \in H \) show \( thesis \) using group0_3_L1, restrict_if, group0_2_L7
qed

The neutral element of the group (denoted \(1\) in the group0 context) belongs to every subgroup.

lemma (in group0) group0_3_L5:

assumes A1: \( \text{IsAsubgroup}(H,P) \)

shows \( 1 \in H \)proof
from A1 show \( 1 \in H \) using group0_3_L1, group0_3_L4
qed

Subgroups are closed with respect to the group operation.

lemma (in group0) group0_3_L6:

assumes A1: \( \text{IsAsubgroup}(H,P) \) and A2: \( a\in H \), \( b\in H \)

shows \( a\cdot b \in H \)proof
let \( f = \text{restrict}(P,H\times H) \)
from A1 have \( monoid0(H,f) \) using IsAsubgroup_def, IsAgroup_def, monoid0_def
with A2 have \( f (\langle a,b\rangle ) \in H \) using group0_1_L1
with A2 show \( a\cdot b \in H \) using restrict_if
qed

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: \( \text{IsAgroup}(G,f) \) and A2: \( \text{IsAsubgroup}(H,f) \) and A3: \( g = \text{restrict}(f,H\times H) \)

shows \( \text{GroupInv}(G,f) \cap H\times H = \text{GroupInv}(H,g) \)proof
let \( e = \text{ TheNeutralElement}(G,f) \)
let \( e_1 = \text{ TheNeutralElement}(H,g) \)
from A1 have \( group0(G,f) \) using group0_def
from A2, A3 have \( group0(H,g) \) using IsAsubgroup_def, group0_def
from \( group0(G,f) \), A2, A3 have \( \text{GroupInv}(G,f) = f^{-1}\{e_1\} \) using group0_3_L4, group0_2_T3
moreover
have \( g^{-1}\{e_1\} = f^{-1}\{e_1\} \cap H\times H \)proof
from A1 have \( f \in G\times G\rightarrow G \) using IsAgroup_def, IsAmonoid_def, IsAssociative_def
moreover
from A2, \( group0(G,f) \) have \( H\times H \subseteq G\times G \) using group0_3_L2
ultimately show \( g^{-1}\{e_1\} = f^{-1}\{e_1\} \cap H\times H \) using A3, func1_2_L1
qed
moreover
from A3, \( group0(H,g) \) have \( \text{GroupInv}(H,g) = g^{-1}\{e_1\} \) using group0_2_T3
ultimately show \( thesis \)
qed

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: \( \text{IsAsubgroup}(H,P) \) and A2: \( g = \text{restrict}(P,H\times H) \)

shows \( \text{GroupInv}(H,g) = \text{restrict}( \text{GroupInv}(G,P),H) \)proof
from groupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using group0_2_T2
moreover
from A1, A2 have \( \text{GroupInv}(H,g) : H\rightarrow H \) using IsAsubgroup_def, group0_2_T2
moreover
from A1 have \( H \subseteq G \) using group0_3_L2
moreover
from groupAssum, A1, A2 have \( \text{GroupInv}(G,P) \cap H\times H = \text{GroupInv}(H,g) \) using group0_3_L7A
ultimately show \( thesis \) using func1_2_L3
qed

A sligtly weaker, but more convenient in applications, reformulation of the above theorem.

theorem (in group0) group0_3_T2:

assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)

shows \( \forall h\in H.\ \text{GroupInv}(H,g)(h) = h^{-1} \) using assms, group0_3_T1, restrict_if

Subgroups are closed with respect to taking the group inverse.

theorem (in group0) group0_3_T3A:

assumes A1: \( \text{IsAsubgroup}(H,P) \) and A2: \( h\in H \)

shows \( h^{-1}\in H \)proof
let \( g = \text{restrict}(P,H\times H) \)
from A1 have \( \text{GroupInv}(H,g) \in H\rightarrow H \) using IsAsubgroup_def, group0_2_T2
with A2 have \( \text{GroupInv}(H,g)(h) \in H \) using apply_type
with A1, A2 show \( h^{-1}\in H \) using group0_3_T2
qed

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\neq 0 \) and A2: \( H\subseteq G \) and A3: \( H \text{ is closed under } P \) and A4: \( \forall x\in H.\ x^{-1} \in H \)

shows \( \text{IsAsubgroup}(H,P) \)proof
let \( g = \text{restrict}(P,H\times H) \)
let \( n = \text{ TheNeutralElement}(H,g) \)
from A3 have I: \( \forall x\in H.\ \forall y\in H.\ x\cdot y \in H \) using IsOpClosed_def
from A1 obtain \( x \) where \( x\in H \)
with A4, I, A2 have \( 1 \in H \) using group0_2_L6
with A3, A2 have T2: \( \text{IsAmonoid}(H,g) \) using group0_1_T1
moreover
have \( \forall h\in H.\ \exists b\in H.\ g\langle h,b\rangle = n \)proof
fix \( h \)
assume \( h\in H \)
with A4, A2 have \( h\cdot h^{-1} = 1 \) using group0_2_L6
moreover
from groupAssum, A2, A3, \( 1 \in H \) have \( 1 = n \) using IsAgroup_def, group0_1_L6
moreover
from A4, \( h\in H \) have \( g\langle h,h^{-1}\rangle = h\cdot h^{-1} \) using restrict_if
ultimately have \( g\langle h,h^{-1}\rangle = n \)
with A4, \( h\in H \) show \( \exists b\in H.\ g\langle h,b\rangle = n \)
qed
ultimately show \( \text{IsAsubgroup}(H,P) \) using IsAsubgroup_def, IsAgroup_def
qed

The singleton with the neutral element is a subgroup.

corollary (in group0) unit_singl_subgr:

shows \( \text{IsAsubgroup}(\{1 \},P) \) using group0_2_L2, group_inv_of_one, group0_3_T3 unfolding IsOpClosed_def

Intersection of subgroups is a subgroup. This lemma is obsolete and should be replaced by subgroup_inter.

lemma group0_3_L7:

assumes A1: \( \text{IsAgroup}(G,f) \) and A2: \( \text{IsAsubgroup}(H_1,f) \) and A3: \( \text{IsAsubgroup}(H_2,f) \)

shows \( \text{IsAsubgroup}(H_1\cap H_2,\text{restrict}(f,H_1\times H_1)) \)proof
let \( e = \text{ TheNeutralElement}(G,f) \)
let \( g = \text{restrict}(f,H_1\times H_1) \)
from A1 have I: \( group0(G,f) \) using group0_def
from A2 have \( group0(H_1,g) \) using IsAsubgroup_def, group0_def
moreover
have \( H_1\cap H_2 \neq 0 \)proof
from A1, A2, A3 have \( e \in H_1\cap H_2 \) using group0_def, group0_3_L5
thus \( thesis \)
qed
moreover
have \( H_1\cap H_2 \subseteq H_1 \)
moreover
from A2, A3, I, \( H_1\cap H_2 \subseteq H_1 \) have \( H_1\cap H_2 \text{ is closed under } g \) using group0_3_L6, IsOpClosed_def, func_ZF_4_L7, func_ZF_4_L5
moreover
from A2, A3, I have \( \forall x \in H_1\cap H_2.\ \text{GroupInv}(H_1,g)(x) \in H_1\cap H_2 \) using group0_3_T2, group0_3_T3A
ultimately show \( thesis \) using group0_3_T3
qed

Intersection of subgroups is a subgroup.

lemma (in group0) subgroup_inter:

assumes \( \ \lt H>\neq 0 \) and \( \forall H\in \ \lt H>.\ \text{IsAsubgroup}(H,P) \)

shows \( \text{IsAsubgroup}(\bigcap \ \lt H>,P) \)proof
{
fix \( H \)
assume \( H:\ \lt H> \)
with assms(2) have \( 1 :H \) using group0_3_L5
}
then have \( \bigcap \ \lt H> \neq 0 \) using assms(1)
moreover {
fix \( t \)
assume \( t:\bigcap \ \lt H> \)
then have \( \forall H\in \ \lt H>.\ t:H \)
with assms have \( t:G \) using group0_3_L2
}
then have \( \bigcap \ \lt H> \subseteq G \)
moreover {
fix \( x \) \( y \)
assume xy: \( x:\bigcap \ \lt H> \), \( y:\bigcap \ \lt H> \)
{
fix \( J \)
assume J: \( J:\ \lt H> \)
with xy have \( x:J \), \( y:J \)
with J have \( P\langle x,y\rangle :J \) using assms(2), group0_3_L6
}
then have \( P\langle x,y\rangle :\bigcap \ \lt H> \) using assms(1)
}
then have \( \bigcap \ \lt H> \text{ is closed under } P \) unfolding IsOpClosed_def
moreover {
fix \( x \)
assume x: \( x:\bigcap \ \lt H> \)
{
fix \( J \)
assume J: \( J:\ \lt H> \)
with x have \( x:J \)
with J, assms(2) have \( x^{-1} \in J \) using group0_3_T3A
}
then have \( x^{-1} \in \bigcap \ \lt H> \) using assms(1)
}
then have \( \forall x \in \bigcap \ \lt H>.\ x^{-1} \in \bigcap \ \lt H> \)
ultimately show \( thesis \) using group0_3_T3
qed

The range of the subgroup operation is the whole subgroup.

lemma image_subgr_op:

assumes A1: \( \text{IsAsubgroup}(H,P) \)

shows \( \text{restrict}(P,H\times H)(H\times H) = H \)proof
from A1 have \( monoid0(H,\text{restrict}(P,H\times H)) \) using IsAsubgroup_def, IsAgroup_def, monoid0_def
then show \( thesis \) by (rule range_carr )
qed

If we restrict the inverse to a subgroup, then the restricted inverse is onto the subgroup.

lemma (in group0) restr_inv_onto:

assumes A1: \( \text{IsAsubgroup}(H,P) \)

shows \( \text{restrict}( \text{GroupInv}(G,P),H)(H) = H \)proof
from A1 have \( \text{GroupInv}(H,\text{restrict}(P,H\times H))(H) = H \) using IsAsubgroup_def, group0_def, group_inv_surj
with A1 show \( thesis \) using group0_3_T1
qed

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 \( \text{IsAsubgroup}(H_1,P) \) and \( \text{IsAsubgroup}(H_2,P) \)

shows \( \text{IsAsubgroup}(H_1\cup H_2,P) \longleftrightarrow (H_1\subseteq H_2 \vee H_2\subseteq H_1) \)proof
assume \( H_1\subseteq H_2 \vee H_2\subseteq H_1 \)
show \( \text{IsAsubgroup}(H_1\cup H_2,P) \)proof
from \( H_1\subseteq H_2 \vee H_2\subseteq H_1 \) have \( H_2 = H_1\cup H_2 \vee H_1 = H_1\cup H_2 \)
with assms show \( \text{IsAsubgroup}(H_1\cup H_2,P) \)
qed
next
assume \( \text{IsAsubgroup}(H_1\cup H_2, P) \)
show \( H_1\subseteq H_2 \vee H_2\subseteq H_1 \)proof
{
assume \( \neg H_1\subseteq H_2 \)
then obtain \( x \) where \( x\in H_1 \) and \( x\notin H_2 \)
with assms(1) have \( x^{-1} \in H_1 \) using group0_3_T3A
{
fix \( y \)
assume \( y\in H_2 \)
let \( z = x\cdot y \)
from \( x\in H_1 \), \( y\in H_2 \) have \( x \in H_1\cup H_2 \) and \( y \in H_1\cup H_2 \)
with \( \text{IsAsubgroup}(H_1\cup H_2,P) \) have \( z \in H_1\cup H_2 \) using group0_3_L6
from assms, \( x \in H_1\cup H_2 \), \( y\in H_2 \) have \( x\in G \), \( y\in G \) and \( y^{-1}\in H_2 \) using group0_3_T3A, group0_3_L2
then have \( z\cdot y^{-1} = x \) and \( x^{-1}\cdot z = y \) using inv_cancel_two(2,3)
{
assume \( z \in H_2 \)
with \( \text{IsAsubgroup}(H_2,P) \), \( y^{-1}\in H_2 \) have \( z\cdot y^{-1} \in H_2 \) using group0_3_L6
with \( z\cdot y^{-1} = x \), \( x\notin H_2 \) have \( False \)
}
hence \( z \notin H_2 \)
with assms(1), \( x^{-1} \in H_1 \), \( z \in H_1\cup H_2 \) have \( x^{-1}\cdot z \in H_1 \) using group0_3_L6
with \( x^{-1}\cdot z = y \) have \( y\in H_1 \)
}
hence \( H_2\subseteq H_1 \)
}
thus \( thesis \)
qed
qed

Transitivity for "is a subgroup of" relation. The proof (probably) uses the lemma restrict_restrict from standard Isabelle/ZF library which states that \( \text{restrict}(\text{restrict}(f,A),B) = \text{restrict}(f,A\cap 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 \( \text{IsAgroup}(G_3,P) \), \( \text{IsAsubgroup}(G_2,P) \), \( \text{IsAsubgroup}(G_1,\text{restrict}(P,G_2\times G_2)) \)

shows \( \text{IsAsubgroup}(G_1,P) \)proof
from assms(2) have \( group0(G_2,\text{restrict}(P,G_2\times G_2)) \) unfolding IsAsubgroup_def, group0_def
with assms(3) have \( G_1\subseteq G_2 \) using group0_3_L2
hence \( G_2\times G_2 \cap G_1\times G_1 = G_1\times G_1 \)
with assms(3) show \( \text{IsAsubgroup}(G_1,P) \) unfolding IsAsubgroup_def
qed

Groups vs. loops

We defined groups as monoids with the inverse operation. An alternative way of defining a group is as a loop whose operation is associative.

Groups have left and right division.

lemma (in group0) gr_has_lr_div:

shows \( Has\text{ LeftDiv}(G,P) \) and \( Has\text{ RightDiv}(G,P) \)proof
{
fix \( x \) \( y \)
assume \( x\in G \), \( y\in G \)
then have \( x^{-1}\cdot y \in G \wedge x\cdot (x^{-1}\cdot y) = y \) using group_op_closed, inverse_in_group, inv_cancel_two(4)
hence \( \exists z.\ z\in G \wedge x\cdot z =y \)
moreover {
fix \( z_1 \) \( z_2 \)
assume \( z_1\in G \wedge x\cdot z_1 =y \) and \( z_2\in G \wedge x\cdot z_2 =y \)
with \( x\in G \) have \( z_1 = z_2 \) using cancel_left
} ultimately have \( \exists !z.\ z\in G \wedge x\cdot z =y \)
}
then show \( Has\text{ LeftDiv}(G,P) \) unfolding HasLeftDiv_def
{
fix \( x \) \( y \)
assume \( x\in G \), \( y\in G \)
then have \( y\cdot x^{-1} \in G \wedge (y\cdot x^{-1})\cdot x = y \) using group_op_closed, inverse_in_group, inv_cancel_two(1)
hence \( \exists z.\ z\in G \wedge z\cdot x =y \)
moreover {
fix \( z_1 \) \( z_2 \)
assume \( z_1\in G \wedge z_1\cdot x =y \) and \( z_2\in G \wedge z_2\cdot x =y \)
with \( x\in G \) have \( z_1 = z_2 \) using cancel_right
} ultimately have \( \exists !z.\ z\in G \wedge z\cdot x =y \)
}
then show \( Has\text{ RightDiv}(G,P) \) unfolding HasRightDiv_def
qed

A group is a quasigroup and a loop.

lemma (in group0) group_is_loop:

shows \( \text{IsAquasigroup}(G,P) \) and \( \text{IsAloop}(G,P) \)proof
show \( \text{IsAquasigroup}(G,P) \) unfolding IsAquasigroup_def, HasLatinSquareProp_def using gr_has_lr_div, group_oper_fun
then show \( \text{IsAloop}(G,P) \) unfolding IsAloop_def using group0_2_L2
qed

An associative loop is a group.

theorem assoc_loop_is_gr:

assumes \( \text{IsAloop}(G,P) \) and \( P \text{ is associative on } G \)

shows \( \text{IsAgroup}(G,P) \)proof
from assms(1) have \( \exists e\in G.\ \forall x\in G.\ P\langle e,x\rangle = x \wedge P\langle x,e\rangle = x \) unfolding IsAloop_def
with assms(2) have \( \text{IsAmonoid}(G,P) \) unfolding IsAmonoid_def
{
fix \( x \)
assume \( x\in G \)
let \( y = \text{RightInv}(G,P)(x) \)
from assms(1), \( x\in G \) have \( y \in G \) and \( P\langle x,y\rangle = \text{ TheNeutralElement}(G,P) \) using loop_loop0_valid, lr_inv_props(3,4)
hence \( \exists y\in G.\ P\langle x,y\rangle = \text{ TheNeutralElement}(G,P) \)
}
with \( \text{IsAmonoid}(G,P) \) show \( \text{IsAgroup}(G,P) \) unfolding IsAgroup_def
qed

For groups the left and right inverse are the same as the group inverse.

lemma (in group0) lr_inv_gr_inv:

shows \( \text{LeftInv}(G,P) = \text{GroupInv}(G,P) \) and \( \text{RightInv}(G,P) = \text{GroupInv}(G,P) \)proof
have \( \text{LeftInv}(G,P):G\rightarrow G \) using group_is_loop, loop_loop0_valid, lr_inv_fun(1)
moreover
from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2
moreover {
fix \( x \)
assume \( x\in G \)
let \( y = \text{LeftInv}(G,P)(x) \)
from \( x\in G \) have \( y \in G \) and \( y\cdot x = 1 \) using group_is_loop(2), loop_loop0_valid, lr_inv_props(1,2)
with \( x\in G \) have \( \text{LeftInv}(G,P)(x) = \text{GroupInv}(G,P)(x) \) using group0_2_L9(1)
} ultimately show \( \text{LeftInv}(G,P) = \text{GroupInv}(G,P) \) using func_eq
have \( \text{RightInv}(G,P):G\rightarrow G \) using group_is_loop, loop_loop0_valid, lr_inv_fun(2)
moreover
from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2
moreover {
fix \( x \)
assume \( x\in G \)
let \( y = \text{RightInv}(G,P)(x) \)
from \( x\in G \) have \( y \in G \) and \( x\cdot y = 1 \) using group_is_loop(2), loop_loop0_valid, lr_inv_props(3,4)
with \( x\in G \) have \( \text{RightInv}(G,P)(x) = \text{GroupInv}(G,P)(x) \) using group0_2_L9(2)
} ultimately show \( \text{RightInv}(G,P) = \text{GroupInv}(G,P) \) using func_eq
qed
end
Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) unit_is_neutral:

assumes \( e = \text{ TheNeutralElement}(G,f) \)

shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)
lemma (in monoid0) group0_1_L1:

assumes \( a\in G \), \( b\in G \)

shows \( a\oplus b \in G \)
Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group0) group_oper_assoc:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \)
theorem (in group0) group0_2_T1:

assumes \( g\in G \) and \( b\in G \) and \( g\cdot b = 1 \)

shows \( b\cdot g = 1 \)
Definition of GroupInv: \( \text{GroupInv}(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = \text{ TheNeutralElement}(G,f)\} \)
lemma (in group0) group0_2_L4:

assumes \( x\in G \)

shows \( \exists !y.\ y\in G \wedge x\cdot y = 1 \)
lemma func1_1_L11:

assumes \( f \subseteq X\times Y \) and \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)

shows \( f: X\rightarrow Y \)
lemma func1_1_L14:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(\{y\}) = \{x\in X.\ f(x) = y\} \)
theorem group0_2_T2:

assumes \( \text{IsAgroup}(G,f) \)

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
lemma (in group0) group0_2_L7:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = a \)

shows \( b=1 \)
lemma (in group0) group0_2_L8A:

assumes \( a\in G \) and \( a^{-1} = 1 \)

shows \( a = 1 \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in group0) group0_2_L9:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)
lemma (in group0) group_inv_of_two:

assumes \( a\in G \) and \( b\in G \)

shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \)
lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \)
lemma func_eq:

assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)

shows \( f = g \)
lemma comp_id_conv:

assumes \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(B,A) \) and \( b\circ a = id(A) \)

shows \( a = converse(b) \) and \( b = converse(a) \)
lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)
lemma (in group0) ginv_image:

assumes \( V\subseteq G \)

shows \( \text{GroupInv}(G,P)(V) \subseteq G \) and \( \text{GroupInv}(G,P)(V) = \{g^{-1}.\ g \in V\} \)
lemma (in group0) group_inv_bij: shows \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P) = id(G) \) and \( \text{GroupInv}(G,P) \in \text{bij}(G,G) \) and \( \text{GroupInv}(G,P) = converse( \text{GroupInv}(G,P)) \)
lemma vimage_converse: shows \( r^{-1}(A) = converse(r)(A) \)
lemma surj_range_image_domain:

assumes \( f \in \text{surj}(A,B) \)

shows \( f(A) = B \)
lemma (in group0) group_inv_of_three:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1} \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1}) \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1} \)
lemma (in group0) group0_2_L12:

assumes \( a\in G \), \( b\in G \)

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)
lemma (in group0) group0_2_L12:

assumes \( a\in G \), \( b\in G \)

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)
lemma (in group0) group0_2_L14A:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma restrict_domain:

assumes \( f:X\rightarrow Y \)

shows \( \text{restrict}(f,X) = f \)
Definition of IsAsubgroup: \( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)
lemma group0_3_L1:

assumes \( \text{IsAsubgroup}(H,f) \) and \( n = \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) \)

shows \( n \in H \), \( \forall h\in H.\ \text{restrict}(f,H\times H)\langle n,h \rangle = h \), \( \forall h\in H.\ \text{restrict}(f,H\times H)\langle h,n\rangle = h \)
lemma func1_1_L5A:

assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)

shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \)
lemma func1_1_L5:

assumes \( \langle x,y\rangle \in f \) and \( f:X\rightarrow Y \)

shows \( x\in X \wedge y\in Y \)
lemma (in group0) group0_3_L2:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H \subseteq G \)
lemma (in group0) group0_3_L4:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( \text{ TheNeutralElement}(H,\text{restrict}(P,H\times H)) = 1 \)
theorem (in group0) group0_2_T3: shows \( P^{-1}\{1 \} = \text{GroupInv}(G,P) \)
lemma func1_2_L1:

assumes \( f:X\rightarrow Y \) and \( B\subseteq X \)

shows \( \text{restrict}(f,B)^{-1}(A) = f^{-1}(A) \cap B \)
lemma group0_3_L7A:

assumes \( \text{IsAgroup}(G,f) \) and \( \text{IsAsubgroup}(H,f) \) and \( g = \text{restrict}(f,H\times H) \)

shows \( \text{GroupInv}(G,f) \cap H\times H = \text{GroupInv}(H,g) \)
lemma func1_2_L3:

assumes \( f:X\rightarrow Y \) and \( g:A\rightarrow Z \) and \( A\subseteq X \) and \( f \cap A\times Z = g \)

shows \( g = \text{restrict}(f,A) \)
theorem (in group0) group0_3_T1:

assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)

shows \( \text{GroupInv}(H,g) = \text{restrict}( \text{GroupInv}(G,P),H) \)
theorem (in group0) group0_3_T2:

assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)

shows \( \forall h\in H.\ \text{GroupInv}(H,g)(h) = h^{-1} \)
theorem (in monoid0) group0_1_T1:

assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)

shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \)
lemma group0_1_L6:

assumes \( \text{IsAmonoid}(G,f) \) and \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)

shows \( \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) = \text{ TheNeutralElement}(G,f) \)
theorem (in group0) group0_3_T3:

assumes \( H\neq 0 \) and \( H\subseteq G \) and \( H \text{ is closed under } P \) and \( \forall x\in H.\ x^{-1} \in H \)

shows \( \text{IsAsubgroup}(H,P) \)
lemma (in group0) group0_3_L5:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( 1 \in H \)
lemma (in group0) group0_3_L6:

assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)

shows \( a\cdot b \in H \)
lemma func_ZF_4_L7:

assumes \( A \text{ is closed under } f \), \( B \text{ is closed under } f \)

shows \( A\cap B \text{ is closed under } f \)
lemma func_ZF_4_L5:

assumes \( A \text{ is closed under } f \) and \( A\subseteq B \)

shows \( A \text{ is closed under } \text{restrict}(f,B\times B) \)
theorem (in group0) group0_3_T3A:

assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)

shows \( h^{-1}\in H \)
lemma (in monoid0) range_carr: shows \( f(G\times G) = G \)
lemma (in group0) group_inv_surj: shows \( \text{GroupInv}(G,P)(G) = G \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) cancel_left:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b = a\cdot c \)

shows \( b=c \)
Definition of HasLeftDiv: \( Has\text{ LeftDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle a,x\rangle = b) \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b = c\cdot b \)

shows \( a = c \)
Definition of HasRightDiv: \( Has\text{ RightDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle x,a\rangle = b) \)
Definition of IsAquasigroup: \( \text{IsAquasigroup}(G,A) \equiv A:G\times G\rightarrow G \wedge A \text{ has Latin square property on } G \)
Definition of HasLatinSquareProp: \( A \text{ has Latin square property on } G \equiv Has\text{ LeftDiv}(G,A) \wedge Has\text{ RightDiv}(G,A) \)
lemma (in group0) gr_has_lr_div: shows \( Has\text{ LeftDiv}(G,P) \) and \( Has\text{ RightDiv}(G,P) \)
Definition of IsAloop: \( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)
lemma loop_loop0_valid:

assumes \( \text{IsAloop}(G,A) \)

shows \( loop0(G,A) \)
lemma (in loop0) lr_inv_props:

assumes \( x\in G \)

shows \( \text{LeftInv}(G,A)(x) \in G \), \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \), \( \text{RightInv}(G,A)(x) \in G \), \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \)
lemma (in group0) group_is_loop: shows \( \text{IsAquasigroup}(G,P) \) and \( \text{IsAloop}(G,P) \)
lemma (in loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)
lemma (in group0) group_is_loop: shows \( \text{IsAquasigroup}(G,P) \) and \( \text{IsAloop}(G,P) \)
lemma (in loop0) lr_inv_props:

assumes \( x\in G \)

shows \( \text{LeftInv}(G,A)(x) \in G \), \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \), \( \text{RightInv}(G,A)(x) \in G \), \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \)
lemma (in group0) group0_2_L9:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)
lemma (in loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)
lemma (in group0) group0_2_L9:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)