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)\} \)