# IsarMathLib

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

theory Group_ZF_4 imports Group_ZF_1 Group_ZF_2 Finite_ZF Cardinal_ZF
begin

This theory file deals with normal subgroup test and some finite group theory. Then we define group homomorphisms and prove that the set of endomorphisms forms a ring with unity and we also prove the first isomorphism theorem.

### Conjugation of subgroups

First we show some properties of conjugation

The conjugate of a subgroup is a subgroup.

theorem (in group0) conj_group_is_group:

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

shows $$\text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P)$$proof
have sub: $$H\subseteq G$$ using assms(1), group0_3_L2
from assms(2) have $$g^{-1}\in G$$ using inverse_in_group
{
fix $$r$$
assume $$r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
then obtain $$h$$ where h: $$h\in H$$, $$r=g\cdot (h\cdot (g^{-1}))$$
from h(1) have $$h^{-1}\in H$$ using group0_3_T3A, assms(1)
from h(1), sub have $$h\in G$$
then have $$h^{-1}\in G$$ using inverse_in_group
with $$g^{-1}\in G$$ have $$((h^{-1})\cdot (g)^{-1})\in G$$ using group_op_closed
from h(2) have $$r^{-1}=(g\cdot (h\cdot (g^{-1})))^{-1}$$
moreover
from $$h\in G$$, $$g^{-1}\in G$$ have s: $$h\cdot (g^{-1})\in G$$ using group_op_closed
ultimately have $$r^{-1}=(h\cdot (g^{-1}))^{-1}\cdot (g)^{-1}$$ using group_inv_of_two, assms(2)
moreover
from $$h\in G$$, $$g^{-1}\in G$$ have $$(h\cdot (g^{-1}))^{-1}=(g^{-1})^{-1}\cdot h^{-1}$$ using group_inv_of_two
moreover
have $$(g^{-1})^{-1}=g$$ using group_inv_of_inv, assms(2)
ultimately have $$r^{-1}=(g\cdot (h^{-1}))\cdot (g)^{-1}$$
with $$h^{-1}\in G$$, $$g^{-1}\in G$$ have $$r^{-1}=g\cdot ((h^{-1})\cdot (g)^{-1})$$ using group_oper_assoc, assms(2)
moreover
from s, assms(2), h(2) have $$r\in G$$ using group_op_closed
moreover
note $$h^{-1}\in H$$
ultimately have $$r^{-1}\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$, $$r\in G$$
}
then have $$\forall r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}.\ r^{-1}\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$ and $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq G$$
moreover {
fix $$s$$ $$t$$
assume s: $$s\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$ and t: $$t\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
then obtain $$hs$$ $$ht$$ where hs: $$hs\in H$$, $$s=g\cdot (hs\cdot (g^{-1}))$$ and ht: $$ht\in H$$, $$t=g\cdot (ht\cdot (g^{-1}))$$
from hs(1) have $$hs\in G$$ using sub
then have $$g\cdot hs\in G$$ using group_op_closed, assms(2)
then have $$(g\cdot hs)^{-1}\in G$$ using inverse_in_group
from ht(1) have $$ht\in G$$ using sub
with $$g^{-1}:G$$ have $$ht\cdot (g^{-1})\in G$$ using group_op_closed
from hs(2), ht(2) have $$s\cdot t=(g\cdot (hs\cdot (g^{-1})))\cdot (g\cdot (ht\cdot (g^{-1})))$$
moreover
from $$hs\in G$$ have $$hs\cdot ht = hs\cdot 1 \cdot ht$$ using group0_2_L2
then have $$hs\cdot ht = hs\cdot (g^{-1}\cdot g)\cdot ht$$ using group0_2_L6, assms(2)
then have $$g\cdot (hs\cdot ht) = g\cdot (hs\cdot (g^{-1}\cdot g)\cdot ht)$$
with $$hs\in G$$ have $$g\cdot (hs\cdot ht) = g\cdot ((hs\cdot g^{-1}\cdot g)\cdot ht)$$ using group_oper_assoc, assms(2), inverse_in_group
with $$hs\in G$$, $$ht\in G$$ have $$g\cdot (hs\cdot ht) = g\cdot (hs\cdot g^{-1}\cdot (g\cdot ht))$$ using group_oper_assoc, assms(2), inverse_in_group, group_op_closed
with $$hs\in G$$, $$ht\in G$$ have $$g\cdot (hs\cdot ht) = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht)$$ using group_oper_assoc, assms(2), inverse_in_group, group_op_closed
then have $$g\cdot (hs\cdot ht)\cdot g^{-1} = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht)\cdot g^{-1}$$
with $$hs\in G$$, $$ht\in G$$ have $$g\cdot ((hs\cdot ht)\cdot g^{-1}) = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht)\cdot g^{-1}$$ using group_oper_assoc, inverse_in_group, assms(2), group_op_closed
with $$hs\in G$$, $$ht\in G$$ have $$g\cdot ((hs\cdot ht)\cdot g^{-1}) = (g\cdot (hs\cdot g^{-1}))\cdot (g\cdot (ht\cdot g^{-1}))$$ using group_oper_assoc, inverse_in_group, assms(2), group_op_closed
ultimately have $$s\cdot t=g\cdot ((hs\cdot ht)\cdot (g^{-1}))$$
moreover
from hs(1), ht(1) have $$hs\cdot ht\in H$$ using assms(1), group0_3_L6
ultimately have $$s\cdot t\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
}
then have $$\{g\cdot (h\cdot g^{-1}).\ h\in H\} \text{ is closed under }P$$ unfolding IsOpClosed_def
moreover
from assms(1) have $$1 \in H$$ using group0_3_L5
then have $$g\cdot (1 \cdot g^{-1})\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
then have $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}\neq 0$$
ultimately show $$thesis$$ using group0_3_T3
qed

Every set is equipollent with its conjugates.

theorem (in group0) conj_set_is_eqpoll:

assumes $$H\subseteq G$$, $$g\in G$$

shows $$H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$proof
have fun: $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}:H\rightarrow \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$ unfolding Pi_def, function_def, domain_def
{
fix $$h1$$ $$h2$$
assume $$h1\in H$$, $$h2\in H$$, $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h1=\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h2$$
with fun have $$g\cdot (h1\cdot g^{-1})=g\cdot (h2\cdot g^{-1})$$, $$h1\cdot g^{-1}\in G$$, $$h2\cdot g^{-1}\in G$$, $$h1\in G$$, $$h2\in G$$ using apply_equality, assms(1), group_op_closed, inverse_in_group, assms(2)
then have $$h1\cdot g^{-1}=h2\cdot g^{-1}$$ using group0_2_L19(2), assms(2)
with $$h1\in G$$, $$h2\in G$$ have $$h1=h2$$ using group0_2_L19(1), inverse_in_group, assms(2)
}
then have $$\forall h1\in H.\ \forall h2\in H.\ \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h1=\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h2 \longrightarrow h1=h2$$
with fun have $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{inj}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\})$$ unfolding inj_def
moreover {
fix $$ghg$$
assume $$ghg\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
then obtain $$h$$ where $$h\in H$$, $$ghg=g\cdot (h\cdot g^{-1})$$
then have $$\langle h,ghg\rangle \in \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}$$
then have $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h=ghg$$ using apply_equality, fun
with $$h\in H$$ have $$\exists h\in H.\ \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h=ghg$$
}
with fun have $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{surj}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\})$$ unfolding surj_def
ultimately have $$\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{bij}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\})$$ unfolding bij_def
then show $$thesis$$ unfolding eqpoll_def
qed

Every normal subgroup contains its conjugate subgroups.

theorem (in group0) norm_group_cont_conj:

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

shows $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H$$proof
{
fix $$r$$
assume $$r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
then obtain $$h$$ where h: $$r=g\cdot (h\cdot g^{-1})$$, $$h\in H$$
moreover
from h(2) have $$h\in G$$ using group0_3_L2, assms(1) unfolding IsAnormalSubgroup_def
moreover
from assms(2) have $$g^{-1}\in G$$ using inverse_in_group
ultimately have $$r=g\cdot h\cdot g^{-1}$$, $$h\in H$$ using group_oper_assoc, assms(2)
then have $$r\in H$$ using assms unfolding IsAnormalSubgroup_def
}
then show $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H$$
qed

If a subgroup contains all its conjugate subgroups, then it is normal.

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)$$proof
{
fix $$h$$ $$g$$
assume $$h\in H$$, $$g\in G$$
with assms(2) have $$g\cdot (h\cdot g^{-1})\in H$$
moreover
from $$g\in G$$, $$h\in H$$ have $$h\in G$$, $$g^{-1}\in G$$, $$g\in G$$ using group0_3_L2, assms(1), inverse_in_group
ultimately have $$g\cdot h\cdot g^{-1}\in H$$ using group_oper_assoc
}
then show $$thesis$$ using assms(1) unfolding IsAnormalSubgroup_def
qed

If a group has only one subgroup of a given order, then this subgroup is normal.

corollary (in group0) only_one_equipoll_sub:

assumes $$\text{IsAsubgroup}(H,P)$$, $$\forall M.\ \text{IsAsubgroup}(M,P)\wedge H\approx M \longrightarrow M=H$$

shows $$\text{IsAnormalSubgroup}(G,P,H)$$proof
{
fix $$g$$
assume g: $$g\in G$$
with assms(1) have $$\text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P)$$ using conj_group_is_group
moreover
from assms(1), g have $$H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$ using conj_set_is_eqpoll, group0_3_L2
ultimately have $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}=H$$ using assms(2)
then have $$\{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H$$
}
then show $$thesis$$ using cont_conj_is_normal, assms(1)
qed

The trivial subgroup is then a normal subgroup.

corollary (in group0) trivial_normal_subgroup:

shows $$\text{IsAnormalSubgroup}(G,P,\{1 \})$$proof
have $$\{1 \}\subseteq G$$ using group0_2_L2
moreover
have $$\{1 \}\neq 0$$
moreover {
fix $$a$$ $$b$$
assume $$a\in \{1 \}$$, $$b\in \{1 \}$$
then have $$a=1$$, $$b=1$$
then have $$P\langle a,b\rangle =1 \cdot 1$$
then have $$P\langle a,b\rangle =1$$ using group0_2_L2
then have $$P\langle a,b\rangle \in \{1 \}$$
}
then have $$\{1 }\text{ is closed under }\}$$ unfolding IsOpClosed_def
moreover {
fix $$a$$
assume $$a\in \{1 \}$$
then have $$a=1$$
then have $$a^{-1}=1 ^{-1}$$
then have $$a^{-1}=1$$ using group_inv_of_one
then have $$a^{-1}\in \{1 \}$$
}
then have $$\forall a\in \{1 \}.\ a^{-1}\in \{1 \}$$
ultimately have $$\text{IsAsubgroup}(\{1 \},P)$$ using group0_3_T3
moreover {
fix $$M$$
assume M: $$\text{IsAsubgroup}(M,P)$$, $$\{1 \}\approx M$$
then have one: $$1 \in M$$, $$M\approx \{1 \}$$ using eqpoll_sym, group0_3_L5
then obtain $$f$$ where $$f\in \text{bij}(M,\{1 \})$$ unfolding eqpoll_def
then have inj: $$f\in \text{inj}(M,\{1 \})$$ unfolding bij_def
then have fun: $$f:M\rightarrow \{1 \}$$ unfolding inj_def
{
fix $$b$$
assume b: $$b\in M$$, $$b\neq 1$$
with $$1 \in M$$ have $$fb\neq f1$$ using inj unfolding inj_def
moreover
from fun, b(1) have $$fb\in \{1 \}$$ by (rule apply_type )
moreover
from fun, one(1) have $$f1 \in \{1 \}$$ by (rule apply_type )
ultimately have $$False$$
}
with $$1 \in M$$ have $$M=\{1 \}$$
} ultimately show $$thesis$$ using only_one_equipoll_sub
qed

The whole group is normal as a subgroup

lemma (in group0) whole_normal_subgroup:

shows $$\text{IsAnormalSubgroup}(G,P,G)$$proof
have $$G\subseteq G$$
moreover
have $$\forall x\in G.\ x^{-1}\in G$$ using inverse_in_group
moreover
have $$G\neq 0$$ using group0_2_L2
moreover
have $$G\text{ is closed under }P$$ using group_op_closed unfolding IsOpClosed_def
ultimately have $$\text{IsAsubgroup}(G,P)$$ using group0_3_T3
moreover {
fix $$n$$ $$g$$
assume ng: $$n\in G$$, $$g\in G$$
then have $$P \langle P \langle g, n\rangle , \text{GroupInv}(G, P) g\rangle \in G$$ using group_op_closed, inverse_in_group
} ultimately show $$thesis$$ unfolding IsAnormalSubgroup_def
qed

### Simple groups

In this subsection we study the groups that build the rest of the groups: the simple groups.

Since the whole group and the trivial subgroup are always normal, it is natural to define simplicity of groups in the following way:

definition

$$[G,f]\text{ is a simple group } \equiv \text{IsAgroup}(G,f) \wedge (\forall M.\ \text{IsAnormalSubgroup}(G,f,M) \longrightarrow M=G\vee M=\{\text{ TheNeutralElement}(G,f)\})$$

From the definition follows that if a group has no subgroups, then it is simple.

corollary (in group0) noSubgroup_imp_simple:

assumes $$\forall H.\ \text{IsAsubgroup}(H,P)\longrightarrow H=G\vee H=\{1 \}$$

shows $$[G,P]\text{ is a simple group }$$proof
have $$\text{IsAgroup}(G,P)$$ using groupAssum
moreover {
fix $$M$$
assume $$\text{IsAnormalSubgroup}(G,P,M)$$
then have $$\text{IsAsubgroup}(M,P)$$ unfolding IsAnormalSubgroup_def
with assms have $$M=G\vee M=\{1 \}$$
} ultimately show $$thesis$$ unfolding IsSimple_def
qed

We add a context for an abelian group

locale abelian_group = group0 +

assumes isAbelian: $$P \text{ is commutative on } G$$

Since every subgroup is normal in abelian groups, it follows that commutative simple groups do not have subgroups.

corollary (in abelian_group) abelian_simple_noSubgroups:

assumes $$[G,P]\text{ is a simple group }$$

shows $$\forall H.\ \text{IsAsubgroup}(H,P)\longrightarrow H=G\vee H=\{1 \}$$proof
{
fix $$H$$
assume A: $$\text{IsAsubgroup}(H,P)$$, $$H \neq \{1 \}$$
then have $$\text{IsAnormalSubgroup}(G,P,H)$$ using Group_ZF_2_4_L6(1), groupAssum, isAbelian
with assms(1), A have $$H=G$$ unfolding IsSimple_def
}
then show $$thesis$$
qed

### Finite groups

This subsection deals with finite groups and their structure

The subgroup of a finite group is finite.

lemma (in group0) finite_subgroup:

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

shows $$Finite(H)$$ using group0_3_L2, subset_Finite, assms

The space of cosets is also finite. In particular, quotient groups.

lemma (in group0) finite_cosets:

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

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$

shows $$Finite(G//r)$$proof
have fun: $$\{\langle g,r\{g\}\rangle .\ g\in G\}:G\rightarrow (G//r)$$ unfolding Pi_def, function_def, domain_def
{
fix $$C$$
assume C: $$C\in G//r$$
have equiv: $$\text{equiv}(G,r)$$ using Group_ZF_2_4_L3, assms(2) unfolding r_def
then have $$\text{refl}(G,r)$$ unfolding equiv_def
with C have $$C\neq 0$$ using EquivClass_1_L5
then obtain $$c$$ where c: $$c\in C$$
with C have $$r\{c\}=C$$ using EquivClass_1_L2, equiv
with c, C have $$\langle c,C\rangle \in \{\langle g,r\{g\}\rangle .\ g\in G\}$$ using EquivClass_1_L1, equiv
then have $$\{\langle g,r\{g\}\rangle .\ g\in G\}c=C$$, $$c\in G$$ using apply_equality, fun
then have $$\exists c\in G.\ \{\langle g,r\{g\}\rangle .\ g\in G\}c=C$$
}
with fun have surj: $$\{\langle g,r\{g\}\rangle .\ g\in G\}\in \text{surj}(G,G//r)$$ unfolding surj_def
from assms(1) obtain $$n$$ where $$n\in nat$$, $$G\approx n$$ unfolding Finite_def
then have G: $$G\preceq n$$, $$Ord(n)$$ using eqpoll_imp_lepoll
then have $$G//r\preceq G$$ using surj_fun_inv_2, surj
with G(1) have $$G//r\preceq n$$ using lepoll_trans
with $$n\in nat$$ show $$Finite(G//r)$$ using lepoll_nat_imp_Finite
qed

All the cosets are equipollent.

lemma (in group0) cosets_equipoll:

assumes $$\text{IsAsubgroup}(H,P)$$, $$g1\in G$$, $$g2\in G$$

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$

shows $$r\{g1\} \approx r\{g2\}$$proof
have equiv: $$\text{equiv}(G,r)$$ using Group_ZF_2_4_L3, assms(1) unfolding r_def
from assms(3,2) have GG: $$(g1^{-1})\cdot g2\in G$$ using inverse_in_group, group_op_closed
then have bij: $$\text{RightTranslation}(G,P,(g1^{-1})\cdot g2)\in \text{bij}(G,G)$$ using trans_bij(1)
have $$r\{g2\}\in G//r$$ using assms(3) unfolding quotient_def
then have sub2: $$r\{g2\}\subseteq G$$ using EquivClass_1_L1, equiv, assms(3)
have $$r\{g1\}\in G//r$$ using assms(2) unfolding quotient_def
then have sub: $$r\{g1\}\subseteq G$$ using EquivClass_1_L1, equiv, assms(2)
with bij have $$\text{restrict}( \text{RightTranslation}(G,P,(g1^{-1})\cdot g2),r\{g1\})\in \text{bij}(r\{g1\}, \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(r\{g1\}))$$ using restrict_bij unfolding bij_def
then have $$r\{g1\}\approx \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(r\{g1\})$$ unfolding eqpoll_def
with GG, sub have A0: $$r\{g1\}\approx \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}$$ using func_imagedef, group0_5_L1(1)
{
fix $$t$$
assume $$t\in \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}$$
then obtain $$q$$ where q: $$t= \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)q$$, $$q\in r\{g1\}$$
then have $$\langle g1,q\rangle \in r$$, $$q\in G$$ using image_iff, sub
then have $$g1\cdot (q^{-1})\in H$$, $$q^{-1}\in G$$ using inverse_in_group unfolding r_def, QuotientGroupRel_def
from GG, q, sub have t: $$t=q\cdot ((g1^{-1})\cdot g2)$$ using group0_5_L2(1)
then have $$g2\cdot t^{-1}=g2\cdot (q\cdot ((g1^{-1})\cdot g2))^{-1}$$
with $$q\in G$$, GG have $$g2\cdot t^{-1}=g2\cdot (((g1^{-1})\cdot g2)^{-1}\cdot q^{-1})$$ using group_inv_of_two
then have $$g2\cdot t^{-1}=g2\cdot (((g2^{-1})\cdot g1^{-1}^{-1})\cdot q^{-1})$$ using group_inv_of_two, inverse_in_group, assms(2), assms(3)
then have $$g2\cdot t^{-1}=g2\cdot (((g2^{-1})\cdot g1)\cdot q^{-1})$$ using group_inv_of_inv, assms(2)
moreover
have $$(g2^{-1})\cdot g1\in G$$ using assms(2), inverse_in_group, assms(3), group_op_closed
with assms(3), $$q^{-1}\in G$$ have $$g2\cdot (((g2^{-1})\cdot g1)\cdot q^{-1})=g2\cdot ((g2^{-1})\cdot g1)\cdot q^{-1}$$ using group_oper_assoc
moreover
have $$g2\cdot ((g2^{-1})\cdot g1)=g2\cdot (g2^{-1})\cdot g1$$ using assms(2), inverse_in_group, assms(3), group_oper_assoc
then have $$g2\cdot ((g2^{-1})\cdot g1)=g1$$ using group0_2_L6, assms(3), group0_2_L2, assms(2)
ultimately have $$g2\cdot t^{-1}=g1\cdot q^{-1}$$
with $$g1\cdot (q^{-1})\in H$$ have $$g2\cdot t^{-1}\in H$$
moreover
from t, $$q\in G$$, $$g2\in G$$ have $$t\in G$$ using inverse_in_group, assms(2), group_op_closed
ultimately have $$\langle g2,t\rangle \in r$$ unfolding QuotientGroupRel_def, r_def using assms(3)
then have $$t\in r\{g2\}$$ using image_iff, assms(4)
}
then have A1: $$\{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}\subseteq r\{g2\}$$
{
fix $$t$$
assume $$t\in r\{g2\}$$
then have $$\langle g2,t\rangle \in r$$, $$t\in G$$ using sub2, image_iff
then have H: $$g2\cdot t^{-1}\in H$$ unfolding QuotientGroupRel_def, r_def
then have G: $$g2\cdot t^{-1}\in G$$ using group0_3_L2, assms(1)
then have $$g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))=g1\cdot g1^{-1}\cdot (g2\cdot t^{-1})$$ using group_oper_assoc, assms(2), inverse_in_group
with G have $$g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))=g2\cdot t^{-1}$$ using group0_2_L6, assms(2), group0_2_L2
with H have HH: $$g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))\in H$$
from $$t\in G$$ have GGG: $$t\cdot g2^{-1}\in G$$ using inverse_in_group, assms(3), group_op_closed
from $$t\in G$$ have $$(t\cdot g2^{-1})^{-1}=g2^{-1}^{-1}\cdot t^{-1}$$ using group_inv_of_two, inverse_in_group, assms(3)
also
have $$\ldots =g2\cdot t^{-1}$$ using group_inv_of_inv, assms(3)
finally have $$(t\cdot g2^{-1})^{-1}=g2\cdot t^{-1}$$
then have $$g1^{-1}\cdot (t\cdot g2^{-1})^{-1}=g1^{-1}\cdot (g2\cdot t^{-1})$$
then have $$((t\cdot g2^{-1})\cdot g1)^{-1}=g1^{-1}\cdot (g2\cdot t^{-1})$$ using group_inv_of_two, GGG, assms(2)
then have HHH: $$g1\cdot ((t\cdot g2^{-1})\cdot g1)^{-1}\in H$$ using HH
from $$t\in G$$ have $$(t\cdot g2^{-1})\cdot g1\in G$$ using assms(2), inverse_in_group, assms(3), group_op_closed
with HHH have $$\langle g1,(t\cdot g2^{-1})\cdot g1\rangle \in r$$ using assms(2) unfolding r_def, QuotientGroupRel_def
then have rg1: $$t\cdot g2^{-1}\cdot g1\in r\{g1\}$$ using image_iff
from assms(3) have $$g2^{-1}:G$$ using inverse_in_group
from $$t\in G$$ have $$t\cdot g2^{-1}\cdot g1\cdot ((g1^{-1})\cdot g2)=t\cdot (g2^{-1}\cdot g1)\cdot ((g1^{-1})\cdot g2)$$ using group_oper_assoc, inverse_in_group, assms(3), assms(2)
also
from $$t\in G$$ have $$\ldots =t\cdot ((g2^{-1}\cdot g1)\cdot ((g1^{-1})\cdot g2))$$ using group_oper_assoc, group_op_closed, inverse_in_group, assms(3), assms(2)
also
from GG, $$g2^{-1}:G$$ have $$\ldots =t\cdot (g2^{-1}\cdot (g1\cdot ((g1^{-1})\cdot g2)))$$ using group_oper_assoc, assms(2)
also
have $$\ldots =t\cdot (g2^{-1}\cdot (g1\cdot (g1^{-1})\cdot g2))$$ using group_oper_assoc, assms(2), inverse_in_group, assms(3)
also
from $$t\in G$$ have $$\ldots =t$$ using group0_2_L6, assms(3), group0_2_L6, assms(2), group0_2_L2, assms(3)
finally have $$t\cdot g2^{-1}\cdot g1\cdot ((g1^{-1})\cdot g2)=t$$
with $$(t\cdot g2^{-1})\cdot g1\in G$$, GG have $$\text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(t\cdot g2^{-1}\cdot g1)=t$$ using group0_5_L2(1)
then have $$t\in \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}$$ using rg1
}
then have $$r\{g2\}\subseteq \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}$$
with A1 have $$r\{g2\}=\{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}$$
with A0 show $$thesis$$
qed

The order of a subgroup multiplied by the order of the space of cosets is the order of the group. We only prove the theorem for finite groups.

theorem (in group0) Lagrange:

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

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$

shows $$|G|=|H| \cdot |G//r|$$proof
have equiv: $$\text{equiv}(G,r)$$ using Group_ZF_2_4_L3, assms(2) unfolding r_def
have $$r\{1 \} \subseteq G$$ unfolding r_def, QuotientGroupRel_def
have $$\forall aa\in G.\ aa\in H \longleftrightarrow \langle aa,1 \rangle \in r$$ using Group_ZF_2_4_L5C unfolding r_def
then have $$\forall aa\in G.\ aa\in H \longleftrightarrow \langle 1 ,aa\rangle \in r$$ using equiv unfolding sym_def, equiv_def
then have $$\forall aa\in G.\ aa\in H \longleftrightarrow aa\in r\{1 \}$$ using image_iff
with $$r\{1 \} \subseteq G$$ have H: $$H=r\{1 \}$$ using group0_3_L2, assms(2)
{
fix $$c$$
assume $$c\in (G//r)$$
then obtain $$g$$ where $$g\in G$$, $$c=r\{g\}$$ unfolding quotient_def
then have $$c\approx r\{1 \}$$ using cosets_equipoll, assms(2), group0_2_L2 unfolding r_def
then have $$|c|=|H|$$ using H, cardinal_cong
}
then have $$\forall c\in (G//r).\ |c|=|H|$$
moreover
have $$Finite(G//r)$$ using assms, finite_cosets
moreover
have $$\bigcup (G//r)=G$$ using Union_quotient, Group_ZF_2_4_L3, assms(2,3)
moreover
from $$\bigcup (G//r)=G$$ have $$Finite(\bigcup (G//r))$$ using assms(1)
moreover
have $$\forall c1\in (G//r).\ \forall c2\in (G//r).\ c1\neq c2 \longrightarrow c1\cap c2=0$$ using quotient_disj, equiv
ultimately show $$thesis$$ using card_partition
qed

### Subgroups generated by sets

In this section we study the minimal subgroup containing a set

Since G is always a group containing the set, we may take the intersection of all subgroups bigger than the set; and hence the result is the subgroup we searched.

definition (in group0)

$$X\subseteq G \Longrightarrow \langle X\rangle _G \equiv \bigcap \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}$$

Every generated subgroup is a subgroup

theorem (in group0) subgroupGen_is_subgroup:

assumes $$X\subseteq G$$

shows $$\text{IsAsubgroup}(\langle X\rangle _G,P)$$proof
have $$\text{restrict}(P,G\times G)=P$$ using group_oper_fun, restrict_idem unfolding Pi_def
then have $$\text{IsAsubgroup}(G,P)$$ unfolding IsAsubgroup_def using groupAssum
with assms have $$G\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}$$
then have $$\{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}\neq 0$$
then show $$thesis$$ using subgroup_inter, SubgroupGenerated_def, assms
qed

The generated subgroup contains the original set

theorem (in group0) subgroupGen_contains_set:

assumes $$X\subseteq G$$

shows $$X \subseteq \langle X\rangle _G$$proof
have $$\text{restrict}(P,G\times G)=P$$ using group_oper_fun, restrict_idem unfolding Pi_def
then have $$\text{IsAsubgroup}(G,P)$$ unfolding IsAsubgroup_def using groupAssum
with assms have $$G\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}$$
then have $$\{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}\neq 0$$
then show $$thesis$$ using subgroup_inter, SubgroupGenerated_def, assms
qed

Given a subgroup that contains a set, the generated subgroup from that set is smaller than this subgroup

theorem (in group0) subgroupGen_minimal:

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

shows $$\langle X\rangle _G \subseteq H$$proof
from assms have sub: $$X\subseteq G$$ using group0_3_L2
from assms have $$H\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}$$ using group0_3_L2
then show $$thesis$$ using sub, subgroup_inter, SubgroupGenerated_def, assms
qed
end
lemma (in group0) group0_3_L2:

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

shows $$H \subseteq G$$
lemma (in group0) inverse_in_group:

assumes $$x\in G$$

shows $$x^{-1}\in G$$
theorem (in group0) group0_3_T3A:

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

shows $$h^{-1}\in H$$
lemma (in group0) group_op_closed:

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

shows $$a\cdot b \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}$$
lemma (in group0) group_inv_of_inv:

assumes $$a\in G$$

shows $$a = (a^{-1})^{-1}$$
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$$
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_2_L6:

assumes $$x\in G$$

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

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

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

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

shows $$1 \in H$$
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_2_L19:

assumes $$a\in G$$, $$b\in G$$, $$c\in G$$ and $$a\neq b$$

shows $$a\cdot c \neq b\cdot c$$ and $$c\cdot a \neq c\cdot b$$
lemma (in group0) group0_2_L19:

assumes $$a\in G$$, $$b\in G$$, $$c\in G$$ and $$a\neq b$$

shows $$a\cdot c \neq b\cdot c$$ and $$c\cdot a \neq c\cdot b$$
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 (in group0) conj_group_is_group:

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

shows $$\text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P)$$
theorem (in group0) conj_set_is_eqpoll:

assumes $$H\subseteq G$$, $$g\in G$$

shows $$H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\}$$
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)$$
lemma (in group0) group_inv_of_one: shows $$1 ^{-1} = 1$$
corollary (in group0) only_one_equipoll_sub:

assumes $$\text{IsAsubgroup}(H,P)$$, $$\forall M.\ \text{IsAsubgroup}(M,P)\wedge H\approx M \longrightarrow M=H$$

shows $$\text{IsAnormalSubgroup}(G,P,H)$$
Definition of IsSimple: $$[G,f]\text{ is a simple group } \equiv \text{IsAgroup}(G,f) \wedge (\forall M.\ \text{IsAnormalSubgroup}(G,f,M) \longrightarrow M=G\vee M=\{\text{ TheNeutralElement}(G,f)\})$$
lemma Group_ZF_2_4_L6:

assumes $$\text{IsAgroup}(G,P)$$ and $$P \text{ is commutative on } G$$ and $$\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))$$
lemma (in group0) Group_ZF_2_4_L3:

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

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

assumes $$\text{refl}(A,r)$$ and $$C \in A//r$$

shows $$C\neq 0$$
lemma EquivClass_1_L2:

assumes $$\text{equiv}(A,r)$$, $$C \in A//r$$ and $$x\in C$$

shows $$r\{x\} = C$$
lemma EquivClass_1_L1:

assumes $$\text{equiv}(A,r)$$ and $$C \in A//r$$ and $$x\in C$$

shows $$x\in A$$
theorem surj_fun_inv_2:

assumes $$f:\text{surj}(A,B)$$, $$A\preceq Q$$, $$Ord(Q)$$

shows $$B\preceq 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 func_imagedef:

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

shows $$f(A) = \{f(x).\ x \in A\}$$
lemma (in group0) group0_5_L1:

assumes $$g\in G$$

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

assumes $$\text{IsAsubgroup}(H,P)$$, $$g1\in G$$, $$g2\in G$$

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$

shows $$r\{g1\} \approx r\{g2\}$$
lemma (in group0) finite_cosets:

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

defines $$r \equiv \text{QuotientGroupRel}(G,P,H)$$

shows $$Finite(G//r)$$
lemma (in group0) group_oper_fun: shows $$P : G\times G\rightarrow G$$
Definition of IsAsubgroup: $$\text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H))$$
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)$$
Definition of SubgroupGenerated: $$X\subseteq G \Longrightarrow \langle X\rangle _G \equiv \bigcap \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}$$