# IsarMathLib

## A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory Group_ZF_2 imports AbelianGroup_ZF func_ZF EquivClass1
begin

This theory continues Group\_ZF.thy and considers lifting the group structure to function spaces and projecting the group structure to quotient spaces, in particular the quotient qroup.

### Lifting groups to function spaces

If we have a monoid (group) $$G$$ than we get a monoid (group) structure on a space of functions valued in in $$G$$ by defining $$(f\cdot g)(x) := f(x)\cdot g(x)$$. We call this process ''lifting the monoid (group) to function space''. This section formalizes this lifting.

The lifted operation is an operation on the function space.

lemma (in monoid0) Group_ZF_2_1_L0A:

assumes A1: $$F = f \text{ lifted to function space over } X$$

shows $$F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G)$$proof
from monoidAsssum have $$f : G\times G\rightarrow G$$ using IsAmonoid_def , IsAssociative_def
with A1 show $$thesis$$ using func_ZF_1_L3 , group0_1_L3B
qed

The result of the lifted operation is in the function space.

lemma (in monoid0) Group_ZF_2_1_L0:

assumes A1: $$F = f \text{ lifted to function space over } X$$ and A2: $$s:X\rightarrow G$$, $$r:X\rightarrow G$$

shows $$F\langle s,r\rangle : X\rightarrow G$$proof
from A1 have $$F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G)$$ using Group_ZF_2_1_L0A
with A2 show $$thesis$$ using apply_funtype
qed

The lifted monoid operation has a neutral element, namely the constant function with the neutral element as the value.

lemma (in monoid0) Group_ZF_2_1_L1:

assumes A1: $$F = f \text{ lifted to function space over } X$$ and A2: $$E = \text{ConstantFunction}(X, \text{TheNeutralElement}(G,f))$$

shows $$E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s)$$proof
from A2 show T1: $$E : X\rightarrow G$$ using unit_is_neutral , func1_3_L1
show $$\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s$$proof
fix $$s$$
assume A3: $$s:X\rightarrow G$$
from monoidAsssum have T2: $$f : G\times G\rightarrow G$$ using IsAmonoid_def , IsAssociative_def
from A3, A1, T1 have $$F\langle E,s\rangle : X\rightarrow G$$, $$F\langle s,E\rangle : X\rightarrow G$$, $$s : X\rightarrow G$$ using Group_ZF_2_1_L0
moreover
from T2, A1, T1, A2, A3 have $$\forall x\in X.\ (F\langle E,s\rangle )(x) = s(x)$$, $$\forall x\in X.\ (F\langle s,E\rangle )(x) = s(x)$$ using func_ZF_1_L4 , group0_1_L3B , func1_3_L2 , apply_type , unit_is_neutral
ultimately show $$F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s$$ using fun_extension_iff
qed
qed

Monoids can be lifted to a function space.

lemma (in monoid0) Group_ZF_2_1_T1:

assumes A1: $$F = f \text{ lifted to function space over } X$$

shows $$\text{IsAmonoid}(X\rightarrow G,F)$$proof
from monoidAsssum, A1 have $$F \text{ is associative on } (X\rightarrow G)$$ using IsAmonoid_def , func_ZF_2_L4 , group0_1_L3B
moreover
from A1 have $$\exists E \in X\rightarrow G.\ \forall s \in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s$$ using Group_ZF_2_1_L1
ultimately show $$thesis$$ using IsAmonoid_def
qed

The constant function with the neutral element as the value is the neutral element of the lifted monoid.

lemma Group_ZF_2_1_L2:

assumes A1: $$\text{IsAmonoid}(G,f)$$ and A2: $$F = f \text{ lifted to function space over } X$$ and A3: $$E = \text{ConstantFunction}(X, \text{TheNeutralElement}(G,f))$$

shows $$E = \text{TheNeutralElement}(X\rightarrow G,F)$$proof
from A1, A2 have T1: $$monoid0(G,f)$$ and T2: $$monoid0(X\rightarrow G,F)$$ using monoid0_def , Group_ZF_2_1_T1
from T1, A2, A3 have $$E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s)$$ using Group_ZF_2_1_L1
with T2 show $$thesis$$ using group0_1_L4
qed

The lifted operation acts on the functions in a natural way defined by the monoid operation.

lemma (in monoid0) lifted_val:

assumes $$F = f \text{ lifted to function space over } X$$ and $$s:X\rightarrow G$$, $$r:X\rightarrow G$$ and $$x\in X$$

shows $$(F\langle s,r\rangle )(x) = s(x) \oplus r(x)$$ using monoidAsssum , assms , IsAmonoid_def , IsAssociative_def , group0_1_L3B , func_ZF_1_L4

The lifted operation acts on the functions in a natural way defined by the group operation. This is the same as lifted_val, but in the group0 context.

lemma (in group0) Group_ZF_2_1_L3:

assumes $$F = P \text{ lifted to function space over } X$$ and $$s:X\rightarrow G$$, $$r:X\rightarrow G$$ and $$x\in X$$

shows $$(F\langle s,r\rangle )(x) = s(x)\cdot r(x)$$ using assms , group0_2_L1 , lifted_val

In the group0 context we can apply theorems proven in monoid0 context to the lifted monoid.

lemma (in group0) Group_ZF_2_1_L4:

assumes A1: $$F = P \text{ lifted to function space over } X$$

shows $$monoid0(X\rightarrow G,F)$$proof
from A1 show $$thesis$$ using group0_2_L1 , Group_ZF_2_1_T1 , monoid0_def
qed

The compostion of a function $$f:X\rightarrow G$$ with the group inverse is a right inverse for the lifted group.

lemma (in group0) Group_ZF_2_1_L5:

assumes A1: $$F = P \text{ lifted to function space over } X$$ and A2: $$s : X\rightarrow G$$ and A3: $$i = \text{GroupInv}(G,P)\circ s$$

shows $$i: X\rightarrow G$$ and $$F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$proof
let $$E = \text{ConstantFunction}(X,1 )$$
have $$E : X\rightarrow G$$ using group0_2_L2 , func1_3_L1
moreover
from groupAssum, A2, A3, A1 have $$F\langle s,i\rangle : X\rightarrow G$$ using group0_2_T2 , comp_fun , Group_ZF_2_1_L4 , group0_1_L1
moreover
from groupAssum, A2, A3, A1 have $$\forall x\in X.\ (F\langle s,i\rangle )(x) = E(x)$$ using group0_2_T2 , comp_fun , Group_ZF_2_1_L3 , comp_fun_apply , apply_funtype , group0_2_L6 , func1_3_L2
moreover
from groupAssum, A1 have $$E = \text{TheNeutralElement}(X\rightarrow G,F)$$ using IsAgroup_def , Group_ZF_2_1_L2
ultimately show $$F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$ using fun_extension_iff , IsAgroup_def , Group_ZF_2_1_L2
from groupAssum, A2, A3 show $$i: X\rightarrow G$$ using group0_2_T2 , comp_fun
qed

Groups can be lifted to the function space.

theorem (in group0) Group_ZF_2_1_T2:

assumes A1: $$F = P \text{ lifted to function space over } X$$

shows $$\text{IsAgroup}(X\rightarrow G,F)$$proof
from A1 have $$\text{IsAmonoid}(X\rightarrow G,F)$$ using group0_2_L1 , Group_ZF_2_1_T1
moreover
have $$\forall s\in X\rightarrow G.\ \exists i\in X\rightarrow G.\ F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$proof
fix $$s$$
assume A2: $$s : X\rightarrow G$$
let $$i = \text{GroupInv}(G,P)\circ s$$
from groupAssum, A2 have $$i:X\rightarrow G$$ using group0_2_T2 , comp_fun
moreover
from A1, A2 have $$F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$ using Group_ZF_2_1_L5
ultimately show $$\exists i\in X\rightarrow G.\ F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$
qed
ultimately show $$thesis$$ using IsAgroup_def
qed

What is the group inverse for the lifted group?

lemma (in group0) Group_ZF_2_1_L6:

assumes A1: $$F = P \text{ lifted to function space over } X$$

shows $$\forall s\in (X\rightarrow G).\ \text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s$$proof
from A1 have $$group0(X\rightarrow G,F)$$ using group0_def , Group_ZF_2_1_T2
moreover
from A1 have $$\forall s\in X\rightarrow G.\ \text{GroupInv}(G,P)\circ s : X\rightarrow G \wedge$$ $$F\langle s, \text{GroupInv}(G,P)\circ s\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$ using Group_ZF_2_1_L5
ultimately have $$\forall s\in (X\rightarrow G).\ \text{GroupInv}(G,P)\circ s = \text{GroupInv}(X\rightarrow G,F)(s)$$ by (rule group0_2_L9A )
thus $$thesis$$
qed

What is the value of the group inverse for the lifted group?

corollary (in group0) lift_gr_inv_val:

assumes $$F = P \text{ lifted to function space over } X$$ and $$s : X\rightarrow G$$ and $$x\in X$$

shows $$( \text{GroupInv}(X\rightarrow G,F)(s))(x) = (s(x))^{-1}$$ using groupAssum , assms , Group_ZF_2_1_L6 , group0_2_T2 , comp_fun_apply

What is the group inverse in a subgroup of the lifted group?

lemma (in group0) Group_ZF_2_1_L6A:

assumes A1: $$F = P \text{ lifted to function space over } X$$ and A2: $$\text{IsAsubgroup}(H,F)$$ and A3: $$g = \text{restrict}(F,H\times H)$$ and A4: $$s\in H$$

shows $$\text{GroupInv}(H,g)(s) = \text{GroupInv}(G,P)\circ s$$proof
from A1 have T1: $$group0(X\rightarrow G,F)$$ using group0_def , Group_ZF_2_1_T2
with A2, A3, A4 have $$\text{GroupInv}(H,g)(s) = \text{GroupInv}(X\rightarrow G,F)(s)$$ using group0_3_T1 , restrict
moreover
from T1, A1, A2, A4 have $$\text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s$$ using group0_3_L2 , Group_ZF_2_1_L6
ultimately show $$thesis$$
qed

If a group is abelian, then its lift to a function space is also abelian.

lemma (in group0) Group_ZF_2_1_L7:

assumes A1: $$F = P \text{ lifted to function space over } X$$ and A2: $$P \text{ is commutative on } G$$

shows $$F \text{ is commutative on } (X\rightarrow G)$$proof
from A1, A2 have $$F \text{ is commutative on } (X\rightarrow \text{range}(P))$$ using group_oper_assocA , func_ZF_2_L2
moreover
from groupAssum have $$\text{range}(P) = G$$ using group0_2_L1 , group0_1_L3B
ultimately show $$thesis$$
qed

### Equivalence relations on groups

The goal of this section is to establish that (under some conditions) given an equivalence relation on a group or (monoid )we can project the group (monoid) structure on the quotient and obtain another group.

The neutral element class is neutral in the projection.

lemma (in monoid0) Group_ZF_2_2_L1:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,f)$$ and A3: $$F = \text{ProjFun2}(G,r,f)$$ and A4: $$e = \text{TheNeutralElement}(G,f)$$

shows $$r\{e\} \in G//r \wedge$$ $$(\forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c)$$proof
from A4 show T1: $$r\{e\} \in G//r$$ using unit_is_neutral , quotientI
show $$\forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c$$proof
fix $$c$$
assume A5: $$c \in G//r$$
then obtain $$g$$ where D1: $$g\in G$$, $$c = r\{g\}$$ using quotient_def
with A1, A2, A3, A4, D1 show $$F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c$$ using unit_is_neutral , EquivClass_1_L10
qed
qed

The projected structure is a monoid.

theorem (in monoid0) Group_ZF_2_2_T1:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,f)$$ and A3: $$F = \text{ProjFun2}(G,r,f)$$

shows $$\text{IsAmonoid}(G//r,F)$$proof
let $$E = r\{ \text{TheNeutralElement}(G,f)\}$$
from A1, A2, A3 have $$E \in G//r \wedge (\forall c\in G//r.\ F\langle E,c\rangle = c \wedge F\langle c,E\rangle = c)$$ using Group_ZF_2_2_L1
hence $$\exists E\in G//r.\ \forall c\in G//r.\ F\langle E,c\rangle = c \wedge F\langle c,E\rangle = c$$
with monoidAsssum, A1, A2, A3 show $$thesis$$ using IsAmonoid_def , EquivClass_2_T2
qed

The class of the neutral element is the neutral element of the projected monoid.

lemma Group_ZF_2_2_L1:

assumes A1: $$\text{IsAmonoid}(G,f)$$ and A2: $$\text{equiv}(G,r)$$ and A3: $$\text{Congruent2}(r,f)$$ and A4: $$F = \text{ProjFun2}(G,r,f)$$ and A5: $$e = \text{TheNeutralElement}(G,f)$$

shows $$r\{e\} = \text{TheNeutralElement}(G//r,F)$$proof
from A1, A2, A3, A4 have T1: $$monoid0(G,f)$$ and T2: $$monoid0(G//r,F)$$ using monoid0_def , Group_ZF_2_2_T1
from T1, A2, A3, A4, A5 have $$r\{e\} \in G//r \wedge$$ $$(\forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c)$$ using Group_ZF_2_2_L1
with T2 show $$thesis$$ using group0_1_L4
qed

The projected operation can be defined in terms of the group operation on representants in a natural way.

lemma (in group0) Group_ZF_2_2_L2:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,P)$$ and A3: $$F = \text{ProjFun2}(G,r,P)$$ and A4: $$a\in G$$, $$b\in G$$

shows $$F\langle r\{a\},r\{b\}\rangle = r\{a\cdot b\}$$proof
from A1, A2, A3, A4 show $$thesis$$ using EquivClass_1_L10
qed

The class of the inverse is a right inverse of the class.

lemma (in group0) Group_ZF_2_2_L3:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,P)$$ and A3: $$F = \text{ProjFun2}(G,r,P)$$ and A4: $$a\in G$$

shows $$F\langle r\{a\},r\{a^{-1}\}\rangle = \text{TheNeutralElement}(G//r,F)$$proof
from A1, A2, A3, A4 have $$F\langle r\{a\},r\{a^{-1}\}\rangle = r\{1 \}$$ using inverse_in_group , Group_ZF_2_2_L2 , group0_2_L6
with groupAssum, A1, A2, A3 show $$thesis$$ using IsAgroup_def , Group_ZF_2_2_L1
qed

The group structure can be projected to the quotient space.

theorem (in group0) Group_ZF_3_T2:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,P)$$

shows $$\text{IsAgroup}(G//r, \text{ProjFun2}(G,r,P))$$proof
let $$F = \text{ProjFun2}(G,r,P)$$
let $$E = \text{TheNeutralElement}(G//r,F)$$
from groupAssum, A1, A2 have $$\text{IsAmonoid}(G//r,F)$$ using IsAgroup_def , monoid0_def , Group_ZF_2_2_T1
moreover
have $$\forall c\in G//r.\ \exists b\in G//r.\ F\langle c,b\rangle = E$$proof
fix $$c$$
assume A3: $$c \in G//r$$
then obtain $$g$$ where D1: $$g\in G$$, $$c = r\{g\}$$ using quotient_def
let $$b = r\{g^{-1}\}$$
from D1 have $$b \in G//r$$ using inverse_in_group , quotientI
moreover
from A1, A2, D1 have $$F\langle c,b\rangle = E$$ using Group_ZF_2_2_L3
ultimately show $$\exists b\in G//r.\ F\langle c,b\rangle = E$$
qed
ultimately show $$thesis$$ using IsAgroup_def
qed

The group inverse (in the projected group) of a class is the class of the inverse.

lemma (in group0) Group_ZF_2_2_L4:

assumes A1: $$\text{equiv}(G,r)$$ and A2: $$\text{Congruent2}(r,P)$$ and A3: $$F = \text{ProjFun2}(G,r,P)$$ and A4: $$a\in G$$

shows $$r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\})$$proof
from A1, A2, A3 have $$group0(G//r,F)$$ using Group_ZF_3_T2 , group0_def
moreover
from A4 have $$r\{a\} \in G//r$$, $$r\{a^{-1}\} \in G//r$$ using inverse_in_group , quotientI
moreover
from A1, A2, A3, A4 have $$F\langle r\{a\},r\{a^{-1}\}\rangle = \text{TheNeutralElement}(G//r,F)$$ using Group_ZF_2_2_L3
ultimately show $$thesis$$ by (rule group0_2_L9 )
qed

### Normal subgroups and quotient groups

If $$H$$ is a subgroup of $$G$$, then for every $$a\in G$$ we can cosider the sets $$\{a\cdot h. h \in H\}$$ and $$\{ h\cdot a. h \in H\}$$ (called a left and right ''coset of H'', resp.) These sets sometimes form a group, called the ''quotient group''. This section discusses the notion of quotient groups.

A normal subgorup $$N$$ of a group $$G$$ is such that $$aba^{-1}$$ belongs to $$N$$ if $$a\in G, b\in N$$.

Definition

$$\text{IsAnormalSubgroup}(G,P,N) \equiv \text{IsAsubgroup}(N,P) \wedge$$ $$(\forall n\in N.\ \forall g\in G.\ P\langle P\langle g,n \rangle , \text{GroupInv}(G,P)(g) \rangle \in N)$$

Having a group and a normal subgroup $$N$$ we can create another group consisting of eqivalence classes of the relation $$a\sim b \equiv a\cdot b^{-1} \in N$$. We will refer to this relation as the quotient group relation. The classes of this relation are in fact cosets of subgroup $$H$$.

Definition

$$\text{QuotientGroupRel}(G,P,H) \equiv$$ $$\{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\}$$

Next we define the operation in the quotient group as the projection of the group operation on the classses of the quotient group relation.

Definition

$$\text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P)$$

Definition of a normal subgroup in a more readable notation.

lemma (in group0) Group_ZF_2_4_L0:

assumes $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$g\in G$$, $$n\in H$$

shows $$g\cdot n\cdot g^{-1} \in H$$ using assms , IsAnormalSubgroup_def

The quotient group relation is reflexive.

lemma (in group0) Group_ZF_2_4_L1:

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

shows $$\text{refl}(G, \text{QuotientGroupRel}(G,P,H))$$ using assms , group0_2_L6 , group0_3_L5 , QuotientGroupRel_def , refl_def

The quotient group relation is symmetric.

lemma (in group0) Group_ZF_2_4_L2:

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

shows $$sym( \text{QuotientGroupRel}(G,P,H))$$proof
{
fix $$a$$ $$b$$
assume A2: $$\langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H)$$
with A1 have $$(a\cdot b^{-1})^{-1} \in H$$ using QuotientGroupRel_def , group0_3_T3A
moreover
from A2 have $$(a\cdot b^{-1})^{-1} = b\cdot a^{-1}$$ using QuotientGroupRel_def , group0_2_L12
ultimately have $$b\cdot a^{-1} \in H$$
with A2 have $$\langle b,a\rangle \in \text{QuotientGroupRel}(G,P,H)$$ using QuotientGroupRel_def
}
then show $$thesis$$ using symI
qed

The quotient group relation is transistive.

lemma (in group0) Group_ZF_2_4_L3A:

assumes A1: $$\text{IsAsubgroup}(H,P)$$ and A2: $$\langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H)$$ and A3: $$\langle b,c\rangle \in \text{QuotientGroupRel}(G,P,H)$$

shows $$\langle a,c\rangle \in \text{QuotientGroupRel}(G,P,H)$$proof
let $$r = \text{QuotientGroupRel}(G,P,H)$$
from A2, A3 have T1: $$a\in G$$, $$b\in G$$, $$c\in G$$ using QuotientGroupRel_def
from A1, A2, A3 have $$(a\cdot b^{-1})\cdot (b\cdot c^{-1}) \in H$$ using QuotientGroupRel_def , group0_3_L6
moreover
from T1 have $$a\cdot c^{-1} = (a\cdot b^{-1})\cdot (b\cdot c^{-1})$$ using group0_2_L14A
ultimately have $$a\cdot c^{-1} \in H$$
with T1 show $$thesis$$ using QuotientGroupRel_def
qed

The quotient group relation is an equivalence relation. Note we do not need the subgroup to be normal for this to be true.

lemma (in group0) Group_ZF_2_4_L3:

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

shows $$\text{equiv}(G, \text{QuotientGroupRel}(G,P,H))$$proof
let $$r = \text{QuotientGroupRel}(G,P,H)$$
from A1 have $$\forall a b c.\ (\langle a, b\rangle \in r \wedge \langle b, c\rangle \in r \longrightarrow \langle a, c\rangle \in r)$$ using Group_ZF_2_4_L3A
then have $$\text{trans}(r)$$ using Fol1_L2
with A1 show $$thesis$$ using Group_ZF_2_4_L1 , Group_ZF_2_4_L2 , QuotientGroupRel_def , equiv_def
qed

The next lemma states the essential condition for congruency of the group operation with respect to the quotient group relation.

lemma (in group0) Group_ZF_2_4_L4:

assumes A1: $$\text{IsAnormalSubgroup}(G,P,H)$$ and A2: $$\langle a1,a2\rangle \in \text{QuotientGroupRel}(G,P,H)$$ and A3: $$\langle b1,b2\rangle \in \text{QuotientGroupRel}(G,P,H)$$

shows $$\langle a1\cdot b1, a2\cdot b2\rangle \in \text{QuotientGroupRel}(G,P,H)$$proof
from A2, A3 have T1: $$a1\in G$$, $$a2\in G$$, $$b1\in G$$, $$b2\in G$$, $$a1\cdot b1 \in G$$, $$a2\cdot b2 \in G$$, $$b1\cdot b2^{-1} \in H$$, $$a1\cdot a2^{-1} \in H$$ using QuotientGroupRel_def , group0_2_L1 , group0_1_L1
with A1 show $$thesis$$ using IsAnormalSubgroup_def , group0_3_L6 , group0_2_L15 , QuotientGroupRel_def
qed

If the subgroup is normal, the group operation is congruent with respect to the quotient group relation.

lemma Group_ZF_2_4_L5A:

assumes $$\text{IsAgroup}(G,P)$$ and $$\text{IsAnormalSubgroup}(G,P,H)$$

shows $$\text{Congruent2}( \text{QuotientGroupRel}(G,P,H),P)$$ using assms , group0_def , Group_ZF_2_4_L4 , Congruent2_def

The quotient group is indeed a group.

theorem Group_ZF_2_4_T1:

assumes $$\text{IsAgroup}(G,P)$$ and $$\text{IsAnormalSubgroup}(G,P,H)$$

shows $$\text{IsAgroup}(G// \text{QuotientGroupRel}(G,P,H), \text{QuotientGroupOp}(G,P,H))$$ using assms , group0_def , Group_ZF_2_4_L3 , IsAnormalSubgroup_def , Group_ZF_2_4_L5A , Group_ZF_3_T2 , QuotientGroupOp_def

The class (coset) of the neutral element is the neutral element of the quotient group.

lemma Group_ZF_2_4_L5B:

assumes $$\text{IsAgroup}(G,P)$$ and $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$r = \text{QuotientGroupRel}(G,P,H)$$ and $$e = \text{TheNeutralElement}(G,P)$$

shows $$r\{e\} = \text{TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H))$$ using assms , IsAnormalSubgroup_def , group0_def , IsAgroup_def , Group_ZF_2_4_L3 , Group_ZF_2_4_L5A , QuotientGroupOp_def , Group_ZF_2_2_L1

A group element is equivalent to the neutral element iff it is in the subgroup we divide the group by.

lemma (in group0) Group_ZF_2_4_L5C:

assumes $$a\in G$$

shows $$\langle a,1 \rangle \in \text{QuotientGroupRel}(G,P,H) \longleftrightarrow a\in H$$ using assms , QuotientGroupRel_def , group_inv_of_one , group0_2_L2

A group element is in $$H$$ iff its class is the neutral element of $$G/H$$.

lemma (in group0) Group_ZF_2_4_L5D:

assumes A1: $$\text{IsAnormalSubgroup}(G,P,H)$$ and A2: $$a\in G$$ and A3: $$r = \text{QuotientGroupRel}(G,P,H)$$ and A4: $$\text{TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e$$

shows $$r\{a\} = e \longleftrightarrow \langle a,1 \rangle \in r$$proof
assume $$r\{a\} = e$$
with groupAssum, assms have $$r\{1 \} = r\{a\}$$ and I: $$\text{equiv}(G,r)$$ using Group_ZF_2_4_L5B , IsAnormalSubgroup_def , Group_ZF_2_4_L3
with A2 have $$\langle 1 ,a\rangle \in r$$ using eq_equiv_class
with I show $$\langle a,1 \rangle \in r$$ by (rule equiv_is_sym )
next
assume $$\langle a,1 \rangle \in r$$
moreover
from A1, A3 have $$\text{equiv}(G,r)$$ using IsAnormalSubgroup_def , Group_ZF_2_4_L3
ultimately have $$r\{a\} = r\{1 \}$$ using equiv_class_eq
with groupAssum, A1, A3, A4 show $$r\{a\} = e$$ using Group_ZF_2_4_L5B
qed

The class of $$a\in G$$ is the neutral element of the quotient $$G/H$$ iff $$a\in H$$.

lemma (in group0) Group_ZF_2_4_L5E:

assumes $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$a\in G$$ and $$r = \text{QuotientGroupRel}(G,P,H)$$ and $$\text{TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e$$

shows $$r\{a\} = e \longleftrightarrow a\in H$$ using assms , Group_ZF_2_4_L5C , Group_ZF_2_4_L5D

Essential condition to show that every subgroup of an abelian group is normal.

lemma (in group0) Group_ZF_2_4_L5:

assumes A1: $$P \text{ is commutative on } G$$ and A2: $$\text{IsAsubgroup}(H,P)$$ and A3: $$g\in G$$, $$h\in H$$

shows $$g\cdot h\cdot g^{-1} \in H$$proof
from A2, A3 have T1: $$h\in G$$, $$g^{-1} \in G$$ using group0_3_L2 , inverse_in_group
with A3, A1 have $$g\cdot h\cdot g^{-1} = g^{-1}\cdot g\cdot h$$ using group0_4_L4A
with A3, T1 show $$thesis$$ using group0_2_L6 , group0_2_L2
qed

Every subgroup of an abelian group is normal. Moreover, the quotient group is also abelian.

lemma Group_ZF_2_4_L6:

assumes A1: $$\text{IsAgroup}(G,P)$$ and A2: $$P \text{ is commutative on } G$$ and A3: $$\text{IsAsubgroup}(H,P)$$

shows $$\text{IsAnormalSubgroup}(G,P,H)$$, $$\text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H))$$proof
from A1, A2, A3 show T1: $$\text{IsAnormalSubgroup}(G,P,H)$$ using group0_def , IsAnormalSubgroup_def , Group_ZF_2_4_L5
let $$r = \text{QuotientGroupRel}(G,P,H)$$
from A1, A3, T1 have $$\text{equiv}(G,r)$$, $$\text{Congruent2}(r,P)$$ using group0_def , Group_ZF_2_4_L3 , Group_ZF_2_4_L5A
with A2 show $$\text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H))$$ using EquivClass_2_T1 , QuotientGroupOp_def
qed

The group inverse (in the quotient group) of a class (coset) is the class of the inverse.

lemma (in group0) Group_ZF_2_4_L7:

assumes $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$a\in G$$ and $$r = \text{QuotientGroupRel}(G,P,H)$$ and $$F = \text{QuotientGroupOp}(G,P,H)$$

shows $$r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\})$$ using groupAssum , assms , IsAnormalSubgroup_def , Group_ZF_2_4_L3 , Group_ZF_2_4_L5A , QuotientGroupOp_def , Group_ZF_2_2_L4

### Function spaces as monoids

On every space of functions $$\{f : X\rightarrow X\}$$ we can define a natural monoid structure with composition as the operation. This section explores this fact.

The next lemma states that composition has a neutral element, namely the identity function on $$X$$ (the one that maps $$x\in X$$ into itself).

lemma Group_ZF_2_5_L1:

assumes A1: $$F = \text{Composition}(X)$$

shows $$\exists I\in (X\rightarrow X).\ \forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f$$proof
let $$I = id(X)$$
from A1 have $$I \in X\rightarrow X \wedge (\forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f)$$ using id_type , func_ZF_6_L1A
thus $$thesis$$
qed

The space of functions that map a set $$X$$ into itsef is a monoid with composition as operation and the identity function as the neutral element.

lemma Group_ZF_2_5_L2:

shows $$\text{IsAmonoid}(X\rightarrow X, \text{Composition}(X))$$, $$id(X) = \text{TheNeutralElement}(X\rightarrow X, \text{Composition}(X))$$proof
let $$I = id(X)$$
let $$F = \text{Composition}(X)$$
show $$\text{IsAmonoid}(X\rightarrow X, \text{Composition}(X))$$ using func_ZF_5_L5 , Group_ZF_2_5_L1 , IsAmonoid_def
then have $$monoid0(X\rightarrow X,F)$$ using monoid0_def
moreover
have $$I \in X\rightarrow X \wedge (\forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f)$$ using id_type , func_ZF_6_L1A
ultimately show $$I = \text{TheNeutralElement}(X\rightarrow X,F)$$ using group0_1_L4
qed
end
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 )))$$
theorem func_ZF_1_L3:

assumes $$f : Y\times Y\rightarrow Y$$ and $$F = f \text{ lifted to function space over } X$$

shows $$F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f))$$
lemma (in monoid0) group0_1_L3B: shows $$\text{range}(f) = G$$
lemma (in monoid0) Group_ZF_2_1_L0A:

assumes $$F = f \text{ lifted to function space over } X$$

shows $$F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G)$$
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 func1_3_L1:

assumes $$c\in Y$$

shows $$\text{ConstantFunction}(X,c) : X\rightarrow Y$$
lemma (in monoid0) Group_ZF_2_1_L0:

assumes $$F = f \text{ lifted to function space over } X$$ and $$s:X\rightarrow G$$, $$r:X\rightarrow G$$

shows $$F\langle s,r\rangle : X\rightarrow G$$
theorem func_ZF_1_L4:

assumes $$f : Y\times Y\rightarrow Y$$ and $$F = f \text{ lifted to function space over } X$$ and $$s:X\rightarrow \text{range}(f)$$, $$r:X\rightarrow \text{range}(f)$$ and $$x\in X$$

shows $$(F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle$$
lemma func1_3_L2:

assumes $$x\in X$$

shows $$\text{ConstantFunction}(X,c)(x) = c$$
lemma func_ZF_2_L4:

assumes $$f \text{ is associative on } G$$ and $$F = f \text{ lifted to function space over } X$$

shows $$F \text{ is associative on } (X\rightarrow \text{range}(f))$$
lemma (in monoid0) Group_ZF_2_1_L1:

assumes $$F = f \text{ lifted to function space over } X$$ and $$E = \text{ConstantFunction}(X, \text{TheNeutralElement}(G,f))$$

shows $$E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s)$$
lemma (in monoid0) Group_ZF_2_1_T1:

assumes $$F = f \text{ lifted to function space over } X$$

shows $$\text{IsAmonoid}(X\rightarrow G,F)$$
lemma (in monoid0) group0_1_L4:

assumes $$e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g)$$

shows $$e = \text{TheNeutralElement}(G,f)$$
lemma (in group0) group0_2_L1: shows $$monoid0(G,P)$$
lemma (in monoid0) lifted_val:

assumes $$F = f \text{ lifted to function space over } X$$ and $$s:X\rightarrow G$$, $$r:X\rightarrow G$$ and $$x\in X$$

shows $$(F\langle s,r\rangle )(x) = s(x) \oplus r(x)$$
lemma (in group0) group0_2_L2: shows $$1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$$
theorem group0_2_T2:

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

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

assumes $$F = P \text{ lifted to function space over } X$$

shows $$monoid0(X\rightarrow G,F)$$
lemma (in monoid0) group0_1_L1:

assumes $$a\in G$$, $$b\in G$$

shows $$a\oplus b \in G$$
lemma (in group0) Group_ZF_2_1_L3:

assumes $$F = P \text{ lifted to function space over } X$$ and $$s:X\rightarrow G$$, $$r:X\rightarrow G$$ and $$x\in X$$

shows $$(F\langle s,r\rangle )(x) = s(x)\cdot r(x)$$
lemma (in group0) group0_2_L6:

assumes $$x\in G$$

shows $$x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1$$
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 Group_ZF_2_1_L2:

assumes $$\text{IsAmonoid}(G,f)$$ and $$F = f \text{ lifted to function space over } X$$ and $$E = \text{ConstantFunction}(X, \text{TheNeutralElement}(G,f))$$

shows $$E = \text{TheNeutralElement}(X\rightarrow G,F)$$
lemma (in group0) Group_ZF_2_1_L5:

assumes $$F = P \text{ lifted to function space over } X$$ and $$s : X\rightarrow G$$ and $$i = \text{GroupInv}(G,P)\circ s$$

shows $$i: X\rightarrow G$$ and $$F\langle s,i\rangle = \text{TheNeutralElement}(X\rightarrow G,F)$$
theorem (in group0) Group_ZF_2_1_T2:

assumes $$F = P \text{ lifted to function space over } X$$

shows $$\text{IsAgroup}(X\rightarrow G,F)$$
lemma (in group0) group0_2_L9A:

assumes $$\forall g\in G.\ b(g) \in G \wedge g\cdot b(g) = 1$$

shows $$\forall g\in G.\ b(g) = g^{-1}$$
lemma (in group0) Group_ZF_2_1_L6:

assumes $$F = P \text{ lifted to function space over } X$$

shows $$\forall s\in (X\rightarrow G).\ \text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s$$
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)$$
lemma (in group0) group0_3_L2:

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

shows $$H \subseteq G$$
lemma (in group0) group_oper_assocA: shows $$P : G\times G\rightarrow G$$
lemma func_ZF_2_L2:

assumes $$f : G\times G\rightarrow G$$ and $$f \text{ is commutative on } G$$ and $$F = f \text{ lifted to function space over } X$$

shows $$F \text{ is commutative on } (X\rightarrow \text{range}(f))$$
lemma EquivClass_1_L10:

assumes $$\text{equiv}(A,r)$$ and $$\text{Congruent2}(r,f)$$ and $$x\in A$$, $$y\in A$$

shows $$\text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \}$$
lemma Group_ZF_2_2_L1:

assumes $$\text{IsAmonoid}(G,f)$$ and $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,f)$$ and $$F = \text{ProjFun2}(G,r,f)$$ and $$e = \text{TheNeutralElement}(G,f)$$

shows $$r\{e\} = \text{TheNeutralElement}(G//r,F)$$
theorem EquivClass_2_T2:

assumes $$\text{equiv}(A,r)$$ and $$\text{Congruent2}(r,f)$$ and $$f \text{ is associative on } A$$

shows $$\text{ProjFun2}(A,r,f) \text{ is associative on } A//r$$
theorem (in monoid0) Group_ZF_2_2_T1:

assumes $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,f)$$ and $$F = \text{ProjFun2}(G,r,f)$$

shows $$\text{IsAmonoid}(G//r,F)$$
lemma (in group0) inverse_in_group:

assumes $$x\in G$$

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

assumes $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,P)$$ and $$F = \text{ProjFun2}(G,r,P)$$ and $$a\in G$$, $$b\in G$$

shows $$F\langle r\{a\},r\{b\}\rangle = r\{a\cdot b\}$$
lemma (in group0) Group_ZF_2_2_L3:

assumes $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,P)$$ and $$F = \text{ProjFun2}(G,r,P)$$ and $$a\in G$$

shows $$F\langle r\{a\},r\{a^{-1}\}\rangle = \text{TheNeutralElement}(G//r,F)$$
theorem (in group0) Group_ZF_3_T2:

assumes $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,P)$$

shows $$\text{IsAgroup}(G//r, \text{ProjFun2}(G,r,P))$$
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}$$
Definition of IsAnormalSubgroup: $$\text{IsAnormalSubgroup}(G,P,N) \equiv \text{IsAsubgroup}(N,P) \wedge$$ $$(\forall n\in N.\ \forall g\in G.\ P\langle P\langle g,n \rangle , \text{GroupInv}(G,P)(g) \rangle \in N)$$
lemma (in group0) group0_3_L5:

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

shows $$1 \in H$$
Definition of QuotientGroupRel: $$\text{QuotientGroupRel}(G,P,H) \equiv$$ $$\{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\}$$
theorem (in group0) group0_3_T3A:

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

shows $$h^{-1}\in H$$
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_3_L6:

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

shows $$a\cdot b \in H$$
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) Group_ZF_2_4_L3A:

assumes $$\text{IsAsubgroup}(H,P)$$ and $$\langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H)$$ and $$\langle b,c\rangle \in \text{QuotientGroupRel}(G,P,H)$$

shows $$\langle a,c\rangle \in \text{QuotientGroupRel}(G,P,H)$$
lemma Fol1_L2:

assumes $$\forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r$$

shows $$\text{trans}(r)$$
lemma (in group0) Group_ZF_2_4_L1:

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

shows $$\text{refl}(G, \text{QuotientGroupRel}(G,P,H))$$
lemma (in group0) Group_ZF_2_4_L2:

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

shows $$sym( \text{QuotientGroupRel}(G,P,H))$$
lemma (in group0) group0_2_L15:

assumes $$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})$$
lemma (in group0) Group_ZF_2_4_L4:

assumes $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$\langle a1,a2\rangle \in \text{QuotientGroupRel}(G,P,H)$$ and $$\langle b1,b2\rangle \in \text{QuotientGroupRel}(G,P,H)$$

shows $$\langle a1\cdot b1, a2\cdot b2\rangle \in \text{QuotientGroupRel}(G,P,H)$$
Definition of Congruent2: $$\text{Congruent2}(r,f) \equiv$$ $$(\forall x_1 x_2 y_1 y_2.\ \langle x_1,x_2\rangle \in r \wedge \langle y_1,y_2\rangle \in r \longrightarrow$$ $$\langle f\langle x_1,y_1\rangle , f\langle x_2,y_2\rangle \rangle \in r)$$
lemma (in group0) Group_ZF_2_4_L3:

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

shows $$\text{equiv}(G, \text{QuotientGroupRel}(G,P,H))$$
lemma Group_ZF_2_4_L5A:

assumes $$\text{IsAgroup}(G,P)$$ and $$\text{IsAnormalSubgroup}(G,P,H)$$

shows $$\text{Congruent2}( \text{QuotientGroupRel}(G,P,H),P)$$
Definition of QuotientGroupOp: $$\text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P)$$
lemma (in group0) group_inv_of_one: shows $$1 ^{-1} = 1$$
lemma Group_ZF_2_4_L5B:

assumes $$\text{IsAgroup}(G,P)$$ and $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$r = \text{QuotientGroupRel}(G,P,H)$$ and $$e = \text{TheNeutralElement}(G,P)$$

shows $$r\{e\} = \text{TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H))$$
lemma equiv_is_sym:

assumes $$\text{equiv}(X,r)$$ and $$\langle x,y\rangle \in r$$

shows $$\langle y,x\rangle \in r$$
lemma (in group0) Group_ZF_2_4_L5C:

assumes $$a\in G$$

shows $$\langle a,1 \rangle \in \text{QuotientGroupRel}(G,P,H) \longleftrightarrow a\in H$$
lemma (in group0) Group_ZF_2_4_L5D:

assumes $$\text{IsAnormalSubgroup}(G,P,H)$$ and $$a\in G$$ and $$r = \text{QuotientGroupRel}(G,P,H)$$ and $$\text{TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e$$

shows $$r\{a\} = e \longleftrightarrow \langle a,1 \rangle \in r$$
lemma (in group0) group0_4_L4A:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$

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

assumes $$P \text{ is commutative on } G$$ and $$\text{IsAsubgroup}(H,P)$$ and $$g\in G$$, $$h\in H$$

shows $$g\cdot h\cdot g^{-1} \in H$$
theorem EquivClass_2_T1:

assumes $$\text{equiv}(A,r)$$ and $$\text{Congruent2}(r,f)$$ and $$f \text{ is commutative on } A$$

shows $$\text{ProjFun2}(A,r,f) \text{ is commutative on } A//r$$
lemma (in group0) Group_ZF_2_2_L4:

assumes $$\text{equiv}(G,r)$$ and $$\text{Congruent2}(r,P)$$ and $$F = \text{ProjFun2}(G,r,P)$$ and $$a\in G$$

shows $$r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\})$$
lemma func_ZF_6_L1A:

assumes $$f : X\rightarrow X$$

shows $$\text{Composition}(X)\langle f,id(X)\rangle = f$$, $$\text{Composition}(X)\langle id(X),f\rangle = f$$
lemma func_ZF_5_L5: shows $$\text{Composition}(X) \text{ is associative on } (X\rightarrow X)$$
lemma Group_ZF_2_5_L1:

assumes $$F = \text{Composition}(X)$$

shows $$\exists I\in (X\rightarrow X).\ \forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f$$
122
159
32
32