# IsarMathLib

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

theory Group_ZF_5 imports Group_ZF_4 Ring_ZF Semigroup_ZF
begin

In this theory we study group homomorphisms.

### Homomorphisms

A homomorphism is a function between groups that preserves the group operations.

Suppose we have two groups $$G$$ and $$H$$ with corresponding binary operations $$P:G\times G \rightarrow G$$ and $$F:H\times H \rightarrow H$$. Then $$f$$ is a homomorphism if for all $$g_1,g_2\in G$$ we have $$f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle$$.

definition

$$\text{IsAgroup}(G,P) \Longrightarrow \text{IsAgroup}(H,F) \Longrightarrow$$ $$\text{Homomor}(f,G,P,H,F) \equiv \forall g_1\in G.\ \forall g_2\in G.\ f(P\langle g_1,g_2\rangle )=F\langle f(g_1),f(g_2)\rangle$$

Now a lemma about the definition:

lemma homomor_eq:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$g_1\in G$$, $$g_2\in G$$

shows $$f(P\langle g_1,g_2\rangle )=F\langle f(g_1),f(g_2)\rangle$$ using assms, Homomor_def

An endomorphism is a homomorphism from a group to the same group. In case the group is abelian, it has a nice structure.

definition

$$\text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\}$$

The defining property of an endomorphism written in notation used in group0 context:

lemma (in group0) endomor_eq:

assumes $$f \in \text{End}(G,P)$$, $$g_1\in G$$, $$g_2\in G$$

shows $$f(g_1\cdot g_2) = f(g_1)\cdot f(g_2)$$ using groupAssum, assms, homomor_eq unfolding End_def

A function that maps a group $$G$$ into itself and satisfies $$f(g_1\cdot g2) = f(g_1)\cdot f(g_2)$$ is an endomorphism.

lemma (in group0) eq_endomor:

assumes $$f:G\rightarrow G$$ and $$\forall g_1\in G.\ \forall g_2\in G.\ f(g_1\cdot g_2)=f(g_1)\cdot f(g_2)$$

shows $$f \in \text{End}(G,P)$$ using groupAssum, assms, Homomor_def unfolding End_def

The set of endomorphisms forms a submonoid of the monoid of function from a set to that set under composition.

lemma (in group0) end_composition:

assumes $$f_1\in \text{End}(G,P)$$, $$f_2\in \text{End}(G,P)$$

shows $$\text{Composition}(G)\langle f_1,f_2\rangle \in \text{End}(G,P)$$proof
from assms have fun: $$f_1:G\rightarrow G$$, $$f_2:G\rightarrow G$$ unfolding End_def
then have $$f_1\circ f_2:G\rightarrow G$$ using comp_fun
from assms, fun(2) have $$\forall g_1\in G.\ \forall g_2\in G.\ (f_1\circ f_2)(g_1\cdot g_2) = ((f_1\circ f_2)(g_1))\cdot ((f_1\circ f_2)(g_2))$$ using group_op_closed, comp_fun_apply, endomor_eq, apply_type
with fun, $$f_1\circ f_2:G\rightarrow G$$ show $$thesis$$ using eq_endomor, func_ZF_5_L2
qed

We will use some binary operations that are naturally defined on the function space $$G\rightarrow G$$, but we consider them restricted to the endomorphisms of $$G$$. To shorten the notation in such case we define an abbreviation $$\text{InEnd}(F,G,P)$$ which restricts a binary operation $$F$$ to the set of endomorphisms of $$G$$.

abbreviation

$$\text{InEnd}(F,G,P) \equiv \text{restrict}(F, \text{End}(G,P)\times \text{End}(G,P))$$

Endomoprhisms of a group form a monoid with composition as the binary operation, with the identity map as the neutral element.

theorem (in group0) end_comp_monoid:

shows $$\text{IsAmonoid}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P))$$ and $$\text{ TheNeutralElement}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P))=id(G)$$proof
let $$C_0 = \text{InEnd}( \text{Composition}(G),G,P)$$
have fun: $$id(G):G\rightarrow G$$ unfolding id_def
{
fix $$g$$ $$h$$
assume $$g\in G$$, $$h\in G$$
then have $$id(G)(g\cdot h)=(id(G)g)\cdot (id(G)h)$$ using group_op_closed
}
with groupAssum, fun have $$id(G) \in \text{End}(G,P)$$ using eq_endomor
moreover
have A0: $$id(G)=\text{ TheNeutralElement}(G \rightarrow G, \text{Composition}(G))$$ using Group_ZF_2_5_L2(2)
ultimately have A1: $$\text{ TheNeutralElement}(G \rightarrow G, \text{Composition}(G)) \in \text{End}(G,P)$$
moreover
have A2: $$\text{End}(G,P) \subseteq G\rightarrow G$$ unfolding End_def
moreover
have A3: $$\text{End}(G,P) \text{ is closed under } \text{Composition}(G)$$ using end_composition unfolding IsOpClosed_def
ultimately show $$\text{IsAmonoid}( \text{End}(G,P),C_0)$$ using group0_1_T1, Group_ZF_2_5_L2(1) unfolding monoid0_def
have $$\text{IsAmonoid}(G\rightarrow G, \text{Composition}(G))$$ using Group_ZF_2_5_L2(1)
with A0, A1, A2, A3 show $$\text{ TheNeutralElement}( \text{End}(G,P),C_0) = id(G)$$ using group0_1_L6
qed

The set of endomorphisms is closed under pointwise addition (derived from the group operation). This is so because the group is abelian.

assumes $$f\in \text{End}(G,P)$$, $$g\in \text{End}(G,P)$$, $$F = P \text{ lifted to function space over } G$$

shows $$F\langle f,g\rangle \in \text{End}(G,P)$$proof
from assms(1,2) have fun: $$f:G\rightarrow G$$, $$g\in G\rightarrow G$$ unfolding End_def
with assms(3) have fun2: $$F\langle f,g\rangle :G\rightarrow G$$ using Group_ZF_2_1_L0, group0_2_L1
{
fix $$g_1$$ $$g_2$$
assume $$g_1\in G$$, $$g_2\in G$$
with isAbelian, assms, fun have $$(F\langle f,g\rangle )(g_1\cdot g_2) = (F\langle f,g\rangle )(g_1)\cdot (F\langle f,g\rangle )(g_2)$$ using Group_ZF_2_1_L3, group_op_closed, endomor_eq, apply_type, group0_4_L8(3), Group_ZF_2_1_L3
}
with fun2 show $$thesis$$ using eq_endomor
qed

The inverse of an abelian group is an endomorphism.

lemma (in abelian_group) end_inverse_group:

shows $$\text{GroupInv}(G,P) \in \text{End}(G,P)$$ using inverse_in_group, group_inv_of_two, isAbelian, IsCommutative_def, group0_2_T2, groupAssum, Homomor_def unfolding End_def

The set of homomorphisms of an abelian group is an abelian subgroup of the group of functions from a set to a group, under pointwise multiplication.

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

shows $$\text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P))$$ and $$\text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P)$$proof
have $$\text{End}(G,P)\neq 0$$ using end_comp_monoid(1), group0_1_L3A unfolding monoid0_def
moreover
have $$\text{End}(G,P) \subseteq G\rightarrow G$$ unfolding End_def
moreover
from isAbelian, assms(1) have $$\text{End}(G,P)\text{ is closed under }F$$ unfolding IsOpClosed_def using end_pointwise_addition
moreover
from groupAssum, assms(1) have $$\forall f\in \text{End}(G,P).\ \text{GroupInv}(G\rightarrow G,F)(f) \in \text{End}(G,P)$$ using group0_1_L1, end_composition(1), end_inverse_group, func_ZF_5_L2, group0_2_T2, Group_ZF_2_1_L6 unfolding monoid0_def, End_def
ultimately show $$\text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P))$$ using assms(1), group0_3_T3, Group_ZF_2_1_T2 unfolding IsAsubgroup_def, group0_def
from assms(1), isAbelian show $$\text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P)$$ using Group_ZF_2_1_L7 unfolding End_def, IsCommutative_def
qed

For the endomorphisms of a group $$G$$ the group operation lifted to the function space over $$G$$ is distributive with respect to the composition operation.

lemma (in abelian_group) distributive_comp_pointwise:

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

shows $$\text{IsDistributive}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P))$$proof
let $$C_G = \text{Composition}(G)$$
let $$C_E = \text{InEnd}(C_G,G,P)$$
let $$F_E = \text{InEnd}(F,G,P)$$
{
fix $$b$$ $$c$$ $$d$$
assume AS: $$b\in \text{End}(G,P)$$, $$c\in \text{End}(G,P)$$, $$d\in \text{End}(G,P)$$
with assms(1) have ig1: $$C_G \langle b, F \langle c, d\rangle \rangle = b\circ (F\langle c,d\rangle )$$ using Group_ZF_2_1_L0, func_ZF_5_L2 unfolding End_def
with AS have ig2: $$F\langle C_G\langle b,c\rangle ,C_G \langle b,d\rangle \rangle = F\langle b\circ c,b\circ d\rangle$$ unfolding End_def using func_ZF_5_L2
from assms(1), AS have comp1fun: $$(b\circ (F\langle c,d\rangle )):G\rightarrow G$$ using Group_ZF_2_1_L0, comp_fun unfolding End_def
from assms(1), AS have comp2fun: $$(F \langle b\circ c,b\circ d\rangle ) : G\rightarrow G$$ using Group_ZF_2_1_L0, comp_fun unfolding End_def
{
fix $$g$$
assume $$g\in G$$
with assms(1), AS(2,3) have $$(b\circ (F\langle c,d\rangle ))(g) = b((F\langle c,d\rangle )(g))$$ using comp_fun_apply, Group_ZF_2_1_L0 unfolding End_def
with groupAssum, assms(1), AS, $$g\in G$$ have $$(b\circ (F\langle c,d\rangle ))(g) = (F\langle b\circ c,b\circ d\rangle )(g)$$ using Group_ZF_2_1_L3, apply_type, homomor_eq, comp_fun unfolding End_def
}
hence $$\forall g\in G.\ (b\circ (F\langle c,d\rangle ))(g) = (F\langle b\circ c,b\circ d\rangle )(g)$$
with comp1fun, comp2fun, ig1, ig2 have $$C_G\langle b,F\langle c, d\rangle \rangle = F\langle C_G\langle b , c\rangle ,C_G\langle b,d\rangle \rangle$$ using func_eq
moreover
from AS(2,3) have $$F\langle c, d\rangle = F_E\langle c, d\rangle$$ using restrict
moreover
from AS have $$C_G\langle b,c\rangle = C_E\langle b,c\rangle$$ and $$C_G\langle b,d\rangle = C_E\langle b,d\rangle$$ using restrict
moreover
from assms, AS have $$C_G\langle b,F \langle c,d\rangle \rangle = C_E\langle b, F\langle c, d\rangle \rangle$$ using end_pointwise_addition
moreover
from AS have $$F\langle C_G\langle b,c\rangle ,C_G\langle b,d\rangle \rangle = F_E\langle C_G \langle b,c\rangle ,C_G \langle b,d\rangle \rangle$$ using end_composition
ultimately have eq1: $$C_E\langle b, F_E\langle c,d\rangle \rangle = F_E \langle C_E\langle b,c\rangle ,C_E\langle b,d\rangle \rangle$$
from assms(1), AS have compfun: $$(F\langle c,d\rangle )\circ b : G\rightarrow G$$, $$F\langle c\circ b,d\circ b\rangle : G\rightarrow G$$ using Group_ZF_2_1_L0, comp_fun unfolding End_def
{
fix $$g$$
assume $$g\in G$$
with AS(1) have bg: $$b(g) \in G$$ unfolding End_def using apply_type
from $$g\in G$$, AS(1) have $$((F\langle c,d\rangle )\circ b)g = (F\langle c,d\rangle )(b(g))$$ using comp_fun_apply unfolding End_def
also
from assms(1), AS(2,3), bg have $$\ldots = (c(b(g)))\cdot (d(b(g)))$$ using Group_ZF_2_1_L3 unfolding End_def
also
from $$g\in G$$, AS have $$\ldots = ((c\circ b)(g))\cdot ((d\circ b)(g))$$ using comp_fun_apply unfolding End_def
also
from assms(1), $$g\in G$$, AS have $$\ldots = (F\langle c\circ b,d\circ b\rangle )g$$ using comp_fun, Group_ZF_2_1_L3 unfolding End_def
finally have $$((F\langle c,d\rangle )\circ b)(g) = (F\langle c\circ b,d\circ b\rangle )(g)$$
}
hence $$\forall g\in G.\ ((F\langle c,d\rangle )\circ b)(g) = (F\langle c\circ b,d\circ b\rangle )(g)$$
with compfun have $$(F\langle c,d\rangle )\circ b = F\langle c\circ b,d\circ b\rangle$$ using func_eq
with assms(1), AS have $$C_G\langle F\langle c,d\rangle ,b\rangle = F\langle C_G\langle c,b\rangle ,C_G\langle d , b\rangle \rangle$$ using Group_ZF_2_1_L0, func_ZF_5_L2 unfolding End_def
moreover
from AS(2,3) have $$F\langle c, d\rangle = F_E\langle c, d\rangle$$ using restrict
moreover
from AS have $$C_G\langle c,b\rangle = C_E\langle c , b\rangle$$, $$C_G\langle d,b\rangle = C_E\langle d,b\rangle$$ using restrict
moreover
from assms, AS have $$C_G\langle F\langle c,d\rangle ,b\rangle = C_E\langle F\langle c,d\rangle ,b\rangle$$ using end_pointwise_addition
moreover
from AS have $$F\langle C_G\langle c,b\rangle ,C_G\langle d,b\rangle \rangle = F_E\langle C_G\langle c,b\rangle ,C_G\langle d,b\rangle \rangle$$ using end_composition
ultimately have $$C_E\langle F_E\langle c,d\rangle ,b\rangle = F_E\langle C_E\langle c,b\rangle ,C_E\langle d,b\rangle \rangle$$
with eq1 have $$(C_E\langle b, F_E\langle c, d\rangle \rangle = F_E\langle C_E\langle b,c\rangle ,C_E\langle b,d\rangle \rangle ) \wedge$$ $$(C_E\langle F_E\langle c,d\rangle ,b\rangle = F_E\langle C_E\langle c,b\rangle ,C_E\langle d,b\rangle \rangle )$$
}
then show $$thesis$$ unfolding IsDistributive_def
qed

The endomorphisms of an abelian group is in fact a ring with the previous operations.

theorem (in abelian_group) end_is_ring:

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

shows $$\text{IsAring}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P))$$ using assms, end_addition_group, end_comp_monoid(1), distributive_comp_pointwise unfolding IsAring_def

The theorems proven in the ring0 context are valid in the abelian_group context as applied to the endomorphisms of $$G$$.

sublocale abelian_group < endo_ring: ring0

using end_is_ring unfolding ring0_def

### First isomorphism theorem

Now we will prove that any homomorphism $$f:G\to H$$ defines a bijective homomorphism between $$G/H$$ and $$f(G)$$.

A group homomorphism sends the neutral element to the neutral element.

lemma image_neutral:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$f(\text{ TheNeutralElement}(G,P)) = \text{ TheNeutralElement}(H,F)$$proof
let $$e_G = \text{ TheNeutralElement}(G,P)$$
let $$e_H = \text{ TheNeutralElement}(H,F)$$
have g: $$e_G = P\langle e_G,e_G\rangle$$, $$e_G \in G$$ using assms(1), group0_2_L2 unfolding group0_def
with assms have $$f(e_G) = F\langle f(e_G),f(e_G)\rangle$$ using Homomor_def
moreover
from assms(4), g(2) have h: $$f(e_G) \in H$$ using apply_type
with assms(2) have $$f(e_G) = F\langle f(e_G),e_H\rangle$$ using group0_2_L2 unfolding group0_def
ultimately have $$F\langle f(e_G),e_H\rangle = F\langle f(e_G),f(e_G)\rangle$$
with assms(2), h have $$\text{LeftTranslation}(H,F,f(e_G))(e_H) = \text{LeftTranslation}(H,F,f(e_G))(f(e_G))$$ using group0_5_L2(2), group0_2_L2 unfolding group0_def
moreover
from assms(2), h have $$\text{LeftTranslation}(H,F,f(e_G))\in \text{inj}(H,H)$$ using trans_bij(2) unfolding group0_def, bij_def
ultimately show $$thesis$$ using h, assms(2), group0_2_L2 unfolding inj_def, group0_def
qed

If $$f:G\rightarrow H$$ is a homomorphism, then it commutes with the inverse

lemma image_inv:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$g\in G$$

shows $$f( \text{GroupInv}(G,P)(g)) = \text{GroupInv}(H,F)(f(g))$$proof
from assms(4,5) have im: $$f(g)\in H$$ using apply_type
from assms(1,5) have inv: $$\text{GroupInv}(G,P)(g)\in G$$ using inverse_in_group unfolding group0_def
with assms(4) have inv2: $$f( \text{GroupInv}(G,P)g)\in H$$ using apply_type
from assms(1,5) have $$f(\text{ TheNeutralElement}(G,P)) = f(P\langle g, \text{GroupInv}(G,P)(g)\rangle )$$ using group0_2_L6 unfolding group0_def
also
from assms(1,2,3,5), inv have $$\ldots = F\langle f(g),f( \text{GroupInv}(G,P)(g))\rangle$$ using Homomor_def
finally have $$f(\text{ TheNeutralElement}(G,P)) = F\langle f(g),f( \text{GroupInv}(G,P)(g))\rangle$$
with assms(1-4), im, inv2 show $$thesis$$ using group0_2_L9, image_neutral unfolding group0_def
qed

The preimage of a subgroup is a subgroup

theorem preimage_sub:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAsubgroup}(K,F)$$

shows $$\text{IsAsubgroup}(f^{-1}(K),P)$$proof
from assms(2) have Hgr: $$group0(H,F)$$ unfolding group0_def
from assms(1) have Ggr: $$group0(G,P)$$ unfolding group0_def
moreover
from assms, Ggr, Hgr have $$\text{ TheNeutralElement}(G,P) \in f^{-1}(K)$$ using image_neutral, group0_3_L5, func1_1_L15, group0_2_L2
hence $$f^{-1}(K)\neq 0$$
moreover
from assms(4) have $$f^{-1}(K) \subseteq G$$ using func1_1_L3
moreover
from assms, Ggr, Hgr have $$f^{-1}(K) \text{ is closed under } P$$ using func1_1_L15, group0_3_L6, Homomor_def, group_op_closed, func1_1_L15 unfolding IsOpClosed_def
moreover
from assms, Ggr, Hgr have $$\forall x\in f^{-1}(K).\ \text{GroupInv}(G, P)(x) \in f^{-1}(K)$$ using group0_3_T3A, image_inv, func1_1_L15, inverse_in_group
ultimately show $$thesis$$ by (rule group0_3_T3 )
qed

The preimage of a normal subgroup is normal

theorem preimage_normal_subgroup:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAnormalSubgroup}(H,F,K)$$

shows $$\text{IsAnormalSubgroup}(G,P,f^{-1}(K))$$proof
from assms(2) have Hgr: $$group0(H,F)$$ unfolding group0_def
with assms(5) have $$K\subseteq H$$ using group0_3_L2 unfolding IsAnormalSubgroup_def
from assms(1) have Ggr: $$group0(G,P)$$ unfolding group0_def
moreover
from assms have $$\text{IsAsubgroup}(f^{-1}(K),P)$$ using preimage_sub unfolding IsAnormalSubgroup_def
moreover {
fix $$g$$
assume gG: $$g\in G$$
{
fix $$h$$
assume $$h \in \{P\langle g,P\langle h, \text{GroupInv}(G, P)(g)\rangle \rangle .\ h \in f^{-1}(K)\}$$
then obtain $$k$$ where k: $$h = P\langle g,P\langle k, \text{GroupInv}(G, P)(g)\rangle \rangle$$, $$k \in f^{-1}(K)$$
from k(1) have $$f(h) = f(P\langle g,P\langle k, \text{GroupInv}(G, P)(g)\rangle \rangle )$$
moreover
from assms(4), k(2) have $$k\in G$$ using vimage_iff unfolding Pi_def
ultimately have f: $$f(h) = F\langle f(g),F\langle f(k), \text{GroupInv}(H,F)(f(g))\rangle \rangle$$ using assms(1-4), Ggr, gG, group_op_closed, inverse_in_group, image_inv, homomor_eq
from assms(1,4), Ggr, $$g\in G$$, k have $$h\in G$$ using group_op_closed, inverse_in_group, func1_1_L15
from assms(4,5), k(2), $$g\in G$$ have $$f(k)\in K$$, $$f(g)\in H$$ and $$F\langle F\langle f(g),f(k)\rangle , \text{GroupInv}(H,F)(f(g))\rangle \in K$$ using func1_1_L15, apply_type unfolding IsAnormalSubgroup_def
moreover
from $$f(k)\in K$$, $$K\subseteq H$$, Hgr, f, $$f(g)\in H$$ have $$f(h) = F\langle F\langle f(g),f(k)\rangle , \text{GroupInv}(H,F)(f(g))\rangle$$ using group_oper_assoc, inverse_in_group
ultimately have $$f(h) \in K$$
with assms(4), $$h\in G$$ have $$h \in f^{-1}(K)$$ using func1_1_L15
}
hence $$\{P\langle g,P\langle h, \text{GroupInv}(G,P)(g)\rangle \rangle .\ h\in f^{-1}(K)\} \subseteq f^{-1}(K)$$
}
hence $$\forall g\in G.\ \{P\langle g, P\langle h, \text{GroupInv}(G, P)(g)\rangle \rangle .\ h\in f^{-1}(K)\} \subseteq f^{-1}(K)$$
ultimately show $$thesis$$ using cont_conj_is_normal
qed

The kernel of an homomorphism is a normal subgroup.

corollary kernel_normal_sub:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$\text{IsAnormalSubgroup}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\})$$ using assms, preimage_normal_subgroup, trivial_normal_subgroup unfolding group0_def

The image of a subgroup is a subgroup

theorem image_subgroup:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAsubgroup}(K,P)$$

shows $$\text{IsAsubgroup}(fK,F)$$proof
from assms(1,5) have sub: $$K\subseteq G$$ using group0_3_L2 unfolding group0_def
from assms(2) have $$group0(H,F)$$ unfolding group0_def
moreover
from assms(4) have $$f(K) \subseteq H$$ using func_imagedef, sub, apply_type
moreover
from assms(1,4,5), sub have $$f(\text{ TheNeutralElement}(G,P)) \in f(K)$$ using group0_3_L5, func_imagedef unfolding group0_def
hence $$f(K) \neq 0$$
moreover {
fix $$x$$
assume $$x\in f(K)$$
with assms(4), sub obtain $$q$$ where q: $$q\in K$$, $$x=f(q)$$ using func_imagedef
with assms(1-4), sub have $$\text{GroupInv}(H,F)(x) = f( \text{GroupInv}(G,P)q)$$ using image_inv
with assms(1,4,5), q(1), sub have $$\text{GroupInv}(H,F)(x) \in f(K)$$ using group0_3_T3A, func_imagedef unfolding group0_def
}
hence $$\forall x\in f(K).\ \text{GroupInv}(H, F)(x) \in f(K)$$
moreover {
fix $$x$$ $$y$$
assume $$x\in f(K)$$, $$y\in f(K)$$
with assms(4), sub obtain $$q_x$$ $$q_y$$ where q: $$q_x\in K$$, $$x=f(q_x)$$, $$q_y\in K$$, $$y=f(q_y)$$ using func_imagedef
with assms(1-3), sub have $$F\langle x,y\rangle = f(P\langle q_x,q_y\rangle )$$ using homomor_eq
moreover
from assms(1,5), q(1,3) have $$P\langle q_x,q_y\rangle \in K$$ using group0_3_L6 unfolding group0_def
ultimately have $$F\langle x,y\rangle \in f(K)$$ using assms(4), sub, func_imagedef
}
then have $$f(K) \text{ is closed under } F$$ unfolding IsOpClosed_def
ultimately show $$thesis$$ using group0_3_T3
qed

The image of a group under a homomorphism is a subgroup of the target group.

corollary image_group:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$\text{IsAsubgroup}(f(G),F)$$proof
from assms(1) have $$\text{restrict}(P,G\times G) = P$$ using group_oper_fun, restrict_domain unfolding group0_def
with assms show $$thesis$$ using image_subgroup unfolding IsAsubgroup_def
qed

Now we are able to prove the first isomorphism theorem. This theorem states that any group homomorphism $$f:G\to H$$ gives an isomorphism between a quotient group of $$G$$ and a subgroup of $$H$$.

theorem isomorphism_first_theorem:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

defines $$r \equiv \text{QuotientGroupRel}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\})$$ and $$\mathcal{P} \equiv \text{QuotientGroupOp}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\})$$

shows $$\exists \mathfrak{f} .\ \text{Homomor}(\mathfrak{f} ,G//r,\mathcal{P},f(G),\text{restrict}(F,(f(G))\times (f(G)))) \wedge \mathfrak{f} \in \text{bij}(G//r,f(G))$$proof
let $$\mathfrak{f} = \{\langle r\{g\},f(g)\rangle .\ g\in G\}$$
from assms(1-5) have $$\text{equiv}(G,r)$$ using Group_ZF_2_4_L3, kernel_normal_sub unfolding group0_def, IsAnormalSubgroup_def
from assms(4,5) have $$\mathfrak{f} \in Pow((G//r)\times fG)$$ unfolding quotient_def using func_imagedef
moreover
have $$(G//r) \subseteq domain(\mathfrak{f} )$$ unfolding domain_def, quotient_def
moreover {
fix $$x$$ $$y$$ $$t$$
assume A: $$\langle x,y\rangle \in \mathfrak{f}$$, $$\langle x,t\rangle \in \mathfrak{f}$$
then obtain $$g_y$$ $$g_r$$ where $$\langle x, y\rangle =\langle r\{g_y\},f(g_y)\rangle$$, $$\langle x, t\rangle =\langle r\{g_r\},f(g_r)\rangle$$ and $$g_r\in G$$, $$g_y\in G$$
hence B: $$r\{g_y\}=r\{g_r\}$$, $$y=f(g_y)$$, $$t=f(g_r)$$
from assms(4), $$g_y\in G$$, $$g_r\in G$$, B(2,3) have $$y\in H$$, $$t\in H$$ using apply_type
with $$\text{equiv}(G,r)$$, $$g_r\in G$$, $$r\{g_y\}=r\{g_r\}$$ have $$\langle g_y,g_r\rangle \in r$$ using same_image_equiv
with assms(4,5) have $$f(P\langle g_y, \text{GroupInv}(G,P)(g_r)\rangle ) = \text{ TheNeutralElement}(H,F)$$ unfolding QuotientGroupRel_def using func1_1_L15
with assms(1-4), B(2,3), $$g_y\in G$$, $$g_r\in G$$, $$y\in H$$, $$t\in H$$ have $$y=t$$ using image_inv, Homomor_def, inverse_in_group, group0_2_L11A unfolding group0_def
}
hence $$\forall x y.\ \langle x,y\rangle \in \mathfrak{f} \longrightarrow (\forall z.\ \langle x,z\rangle \in \mathfrak{f} \longrightarrow y=z)$$
ultimately have ff_fun: $$\mathfrak{f} :G//r\rightarrow f(G)$$ unfolding Pi_def, function_def
{
fix $$a_1$$ $$a_2$$
assume AS: $$a_1\in G//r$$, $$a_2\in G//r$$
then obtain $$g_1$$ $$g_2$$ where $$g_1\in G$$, $$g_2\in G$$ and a: $$a_1=r\{g_1\}$$, $$a_2=r\{g_2\}$$ unfolding quotient_def
with assms, $$\text{equiv}(G,r)$$ have $$\langle \mathcal{P}\langle a_1,a_2\rangle ,f(P\langle g_1,g_2\rangle )\rangle \in \mathfrak{f}$$ using Group_ZF_2_4_L5A, kernel_normal_sub, Group_ZF_2_2_L2, group_op_closed unfolding QuotientGroupOp_def, group0_def
with ff_fun have eq: $$\mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle ) = f(P\langle g_1,g_2\rangle )$$ using apply_equality
from $$g_1\in G$$, $$g_2\in G$$, a have $$\langle a_1,f(g_1)\rangle \in \mathfrak{f}$$ and $$\langle a_2,f(g_2)\rangle \in \mathfrak{f}$$
with assms(1,2,3), ff_fun, $$g_1\in G$$, $$g_2\in G$$, eq have $$F\langle \mathfrak{f} (a_1),\mathfrak{f} (a_2)\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle )$$ using apply_equality, Homomor_def
moreover
from AS, ff_fun have $$\mathfrak{f} (a_1) \in f(G)$$, $$\mathfrak{f} (a_2) \in f(G)$$ using apply_type
ultimately have $$\text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (a_1),\mathfrak{f} (a_2)\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle )$$
}
hence r: $$\forall a_1\in G//r.\ \forall a_2\in G//r.\ \text{restrict}(F,fG\times fG)\langle \mathfrak{f} a_1,\mathfrak{f} a_2\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle )$$
moreover
from assms have G: $$\text{IsAgroup}(G//r,\mathcal{P})$$ using Group_ZF_2_4_T1, kernel_normal_sub
moreover
from assms(1-4) have H: $$\text{IsAgroup}(f(G), \text{restrict}(F,f(G)\times f(G)))$$ using image_group unfolding IsAsubgroup_def
ultimately have HOM: $$\text{Homomor}(\mathfrak{f} ,G//r,\mathcal{P},f(G),\text{restrict}(F,(f(G))\times (f(G))))$$ using Homomor_def
{
fix $$b_1$$ $$b_2$$
assume AS: $$\mathfrak{f} (b_1) = \mathfrak{f} (b_2)$$, $$b_1\in G//r$$, $$b_2\in G//r$$
from G, AS(3) have invb2: $$\text{GroupInv}(G//r,\mathcal{P})(b_2)\in G//r$$ using inverse_in_group unfolding group0_def
with G, AS(2) have I: $$\mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle \in G//r$$ using group_op_closed unfolding group0_def
then obtain $$g$$ where $$g\in G$$ and gg: $$\mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle =r\{g\}$$ unfolding quotient_def
from $$g\in G$$ have $$\langle r\{g\},f(g)\rangle \in \mathfrak{f}$$
with ff_fun, gg have E: $$\mathfrak{f} (\mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle ) = f(g)$$ using apply_equality
from ff_fun, invb2 have pp: $$\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\in f(G)$$ using apply_type
from ff_fun, AS(2,3) have fff: $$\mathfrak{f} (b_1) \in f(G)$$, $$\mathfrak{f} (b_2) \in f(G)$$ using apply_type
from fff(1), pp have EE: $$F\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle =$$ $$\text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle$$
from assms(4) have $$f(G) \subseteq H$$ using func1_1_L6(2)
with fff have $$\mathfrak{f} (b_1)\in H$$, $$\mathfrak{f} (b_2)\in H$$
with assms(1-4), G, H, HOM, ff_fun, AS(1,3), fff(2), EE have $$\text{ TheNeutralElement}(H,F) = \text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle$$ using group0_2_L6(1), restrict, image_inv, group0_3_T1, image_group unfolding group0_def
also
from G, H, HOM, AS(2,3), E have $$\ldots = f(g)$$ using Homomor_def, inverse_in_group unfolding group0_def
finally have $$\text{ TheNeutralElement}(H,F) = f(g)$$
with assms(4), $$g\in G$$ have $$g\in f^{-1}\{\text{ TheNeutralElement}(H,F)\}$$ using func1_1_L15
with assms, $$g\in G$$, gg have $$\mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle = \text{ TheNeutralElement}(G//r,\mathcal{P})$$ using Group_ZF_2_4_L5E, kernel_normal_sub unfolding group0_def
with AS(2,3), G have $$b_1=b_2$$ using group0_2_L11A unfolding group0_def
}
with ff_fun have $$\mathfrak{f} \in \text{inj}(G//r,f(G))$$ unfolding inj_def
moreover {
fix $$m$$
assume $$m \in f(G)$$
with assms(4) obtain $$g$$ where $$g\in G$$, $$m=f(g)$$ using func_imagedef
hence $$\langle r\{g\},m\rangle \in \mathfrak{f}$$
with ff_fun have $$\mathfrak{f} (r\{g\})=m$$ using apply_equality
with $$g\in G$$ have $$\exists A\in G//r.\ \mathfrak{f} (A) = m$$ unfolding quotient_def
} ultimately have $$\mathfrak{f} \in \text{bij}(G//r,fG)$$ unfolding bij_def, surj_def using ff_fun
with HOM show $$thesis$$
qed

The inverse of a bijective homomorphism is an homomorphism. Meaning that in the previous result, the homomorphism we found is an isomorphism.

theorem bij_homomor:

assumes $$f\in \text{bij}(G,H)$$, $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$

shows $$\text{Homomor}(converse(f),H,F,G,P)$$proof
{
fix $$h_1$$ $$h_2$$
assume $$h_1\in H$$, $$h_2\in H$$
with assms(1) obtain $$g_1$$ $$g_2$$ where g1: $$g_1\in G$$, $$f(g_1)=h_1$$ and g2: $$g_2\in G$$, $$f(g_2)=h_2$$ unfolding bij_def, surj_def
with assms(2,3,4) have $$converse(f)(f(P\langle g_1,g_2\rangle )) = converse(f)(F\langle h_1,h_2\rangle )$$ using homomor_eq
with assms(1,2), g1, g2 have $$P\langle converse(f)(h_1),converse(f)(h_2)\rangle = converse(f)(F\langle h_1,h_2\rangle )$$ using left_inverse, group_op_closed unfolding group0_def, bij_def
}
with assms(2,3) show $$thesis$$ using Homomor_def
qed

A very important homomorphism is given by taking every element to its class in a group quotient. Recall that $$\lambda x\in X. p(x)$$ is an alternative notation for function defined as a set of pairs, see lemma lambda_fun_alt in theory func1.thy.

lemma (in group0) quotient_map:

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

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$ and $$q \equiv \lambda x\in G.\ \text{QuotientGroupRel}(G,P,H)\{x\}$$

shows $$\text{Homomor}(q,G,P,G//r, \text{QuotientGroupOp}(G,P,H))$$ using groupAssum, assms, group_op_closed, lam_funtype, lamE, EquivClass_1_L10, Group_ZF_2_4_L3, Group_ZF_2_4_L5A, Homomor_def, Group_ZF_2_4_T1 unfolding IsAnormalSubgroup_def, QuotientGroupOp_def

In the context of group0, we may use all results of semigr0.

sublocale group0 < semigroup: semigr0

unfolding semigr0_def using groupAssum, IsAgroup_def, IsAmonoid_def

end
Definition of Homomor: $$\text{IsAgroup}(G,P) \Longrightarrow \text{IsAgroup}(H,F) \Longrightarrow$$ $$\text{Homomor}(f,G,P,H,F) \equiv \forall g_1\in G.\ \forall g_2\in G.\ f(P\langle g_1,g_2\rangle )=F\langle f(g_1),f(g_2)\rangle$$
lemma homomor_eq:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$g_1\in G$$, $$g_2\in G$$

shows $$f(P\langle g_1,g_2\rangle )=F\langle f(g_1),f(g_2)\rangle$$
Definition of End: $$\text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\}$$
lemma (in group0) group_op_closed:

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

shows $$a\cdot b \in G$$
lemma (in group0) endomor_eq:

assumes $$f \in \text{End}(G,P)$$, $$g_1\in G$$, $$g_2\in G$$

shows $$f(g_1\cdot g_2) = f(g_1)\cdot f(g_2)$$
lemma (in group0) eq_endomor:

assumes $$f:G\rightarrow G$$ and $$\forall g_1\in G.\ \forall g_2\in G.\ f(g_1\cdot g_2)=f(g_1)\cdot f(g_2)$$

shows $$f \in \text{End}(G,P)$$
lemma func_ZF_5_L2:

assumes $$f:X\rightarrow X$$ and $$g:X\rightarrow X$$

shows $$\text{Composition}(X)\langle f,g\rangle = f\circ g$$
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))$$
lemma (in group0) end_composition:

assumes $$f_1\in \text{End}(G,P)$$, $$f_2\in \text{End}(G,P)$$

shows $$\text{Composition}(G)\langle f_1,f_2\rangle \in \text{End}(G,P)$$
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$$
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 Group_ZF_2_5_L2: shows $$\text{IsAmonoid}(X\rightarrow X, \text{Composition}(X))$$, $$id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X))$$
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)$$
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$$
lemma (in group0) group0_2_L1: shows $$monoid0(G,P)$$
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_4_L8:

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

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

assumes $$x\in G$$

shows $$x^{-1}\in G$$
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}$$
Definition of IsCommutative: $$f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle$$
theorem group0_2_T2:

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

shows $$\text{GroupInv}(G,f) : G\rightarrow G$$
theorem (in group0) end_comp_monoid: shows $$\text{IsAmonoid}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P))$$ and $$\text{ TheNeutralElement}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P))=id(G)$$
lemma (in monoid0) group0_1_L3A: shows $$G\neq 0$$

assumes $$f\in \text{End}(G,P)$$, $$g\in \text{End}(G,P)$$, $$F = P \text{ lifted to function space over } G$$

shows $$F\langle f,g\rangle \in \text{End}(G,P)$$
lemma (in monoid0) group0_1_L1:

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

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

assumes $$f_1\in \text{End}(G,P)$$, $$f_2\in \text{End}(G,P)$$

shows $$\text{Composition}(G)\langle f_1,f_2\rangle \in \text{End}(G,P)$$
lemma (in abelian_group) end_inverse_group: shows $$\text{GroupInv}(G,P) \in \text{End}(G,P)$$
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_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)$$
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)$$
Definition of IsAsubgroup: $$\text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H))$$
lemma (in group0) Group_ZF_2_1_L7:

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

shows $$F \text{ is commutative on } (X\rightarrow G)$$
lemma func_eq:

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

shows $$f = g$$
Definition of IsDistributive: $$\text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\$$ $$M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge$$ $$M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle )$$

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

shows $$\text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P))$$ and $$\text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P)$$
lemma (in abelian_group) distributive_comp_pointwise:

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

shows $$\text{IsDistributive}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P))$$
Definition of IsAring: $$\text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge$$ $$\text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M)$$
theorem (in abelian_group) end_is_ring:

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

shows $$\text{IsAring}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P))$$
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) group0_5_L2:

assumes $$g\in G$$, $$a\in G$$

shows $$\text{RightTranslation}(G,P,g)(a) = a\cdot g$$, $$\text{LeftTranslation}(G,P,g)(a) = g\cdot a$$
lemma (in group0) trans_bij:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) \in \text{bij}(G,G)$$ and $$\text{LeftTranslation}(G,P,g) \in \text{bij}(G,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_L9:

assumes $$a\in G$$ and $$b\in G$$ and $$a\cdot b = 1$$

shows $$a = b^{-1}$$ and $$b = a^{-1}$$
lemma image_neutral:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$f(\text{ TheNeutralElement}(G,P)) = \text{ TheNeutralElement}(H,F)$$
lemma (in group0) group0_3_L5:

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

shows $$1 \in H$$
lemma func1_1_L15:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(A) = \{x\in X.\ f(x) \in A\}$$
lemma func1_1_L3:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(D) \subseteq X$$
lemma (in group0) group0_3_L6:

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

shows $$a\cdot b \in H$$
theorem (in group0) group0_3_T3A:

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

shows $$h^{-1}\in H$$
lemma image_inv:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$g\in G$$

shows $$f( \text{GroupInv}(G,P)(g)) = \text{GroupInv}(H,F)(f(g))$$
lemma (in group0) group0_3_L2:

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

shows $$H \subseteq G$$
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)$$
theorem preimage_sub:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAsubgroup}(K,F)$$

shows $$\text{IsAsubgroup}(f^{-1}(K),P)$$
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) cont_conj_is_normal:

assumes $$\text{IsAsubgroup}(H,P)$$, $$\forall g\in G.\ \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H$$

shows $$\text{IsAnormalSubgroup}(G,P,H)$$
theorem preimage_normal_subgroup:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAnormalSubgroup}(H,F,K)$$

shows $$\text{IsAnormalSubgroup}(G,P,f^{-1}(K))$$
corollary (in group0) trivial_normal_subgroup: shows $$\text{IsAnormalSubgroup}(G,P,\{1 \})$$
lemma func_imagedef:

assumes $$f:X\rightarrow Y$$ and $$A\subseteq X$$

shows $$f(A) = \{f(x).\ x \in A\}$$
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$$
theorem image_subgroup:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$, $$\text{IsAsubgroup}(K,P)$$

shows $$\text{IsAsubgroup}(fK,F)$$
lemma (in group0) Group_ZF_2_4_L3:

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

shows $$\text{equiv}(G, \text{QuotientGroupRel}(G,P,H))$$
corollary kernel_normal_sub:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$\text{IsAnormalSubgroup}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\})$$
lemma same_image_equiv:

assumes $$\text{equiv}(A,r)$$, $$y\in A$$, $$r\{x\} = r\{y\}$$

shows $$\langle x,y\rangle \in r$$
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\}$$
lemma (in group0) group0_2_L11A:

assumes $$a\in G$$, $$b\in G$$ and $$a\cdot b^{-1} = 1$$

shows $$a=b$$
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)$$
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\}$$
Definition of QuotientGroupOp: $$\text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P)$$
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))$$
corollary image_group:

assumes $$\text{IsAgroup}(G,P)$$, $$\text{IsAgroup}(H,F)$$, $$\text{Homomor}(f,G,P,H,F)$$, $$f:G\rightarrow H$$

shows $$\text{IsAsubgroup}(f(G),F)$$
lemma func1_1_L6:

assumes $$f:X\rightarrow Y$$

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

assumes $$x\in G$$

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