(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Groups 4› theory Group_ZF_4 imports Group_ZF_1 Group_ZF_2 Finite_ZF Cardinal_ZF begin text‹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.› subsection‹Conjugation of subgroups› text‹First we show some properties of conjugation› text‹The conjugate of a subgroup is a subgroup.› theorem (in group0) conj_group_is_group: assumes "IsAsubgroup(H,P)" "g∈G" shows "IsAsubgroup({g⋅(h⋅g¯). h∈H},P)" proof- have sub:"H⊆G" using assms(1) group0_3_L2 by auto from assms(2) have "g¯∈G" using inverse_in_group by auto { fix r assume "r∈{g⋅(h⋅g¯). h∈H}" then obtain h where h:"h∈H" "r=g⋅(h⋅(g¯))" by auto from h(1) have "h¯∈H" using group0_3_T3A assms(1) by auto from h(1) sub have "h∈G" by auto then have "h¯∈G" using inverse_in_group by auto with ‹g¯∈G› have "((h¯)⋅(g)¯)∈G" using group_op_closed by auto from h(2) have "r¯=(g⋅(h⋅(g¯)))¯" by auto moreover from ‹h∈G› ‹g¯∈G› have s:"h⋅(g¯)∈G" using group_op_closed by blast ultimately have "r¯=(h⋅(g¯))¯⋅(g)¯" using group_inv_of_two assms(2) by auto moreover from ‹h∈G› ‹g¯∈G› have "(h⋅(g¯))¯=(g¯)¯⋅h¯" using group_inv_of_two by auto moreover have "(g¯)¯=g" using group_inv_of_inv assms(2) by auto ultimately have "r¯=(g⋅(h¯))⋅(g)¯" by auto with ‹h¯∈G›‹g¯∈G› have "r¯=g⋅((h¯)⋅(g)¯)" using group_oper_assoc assms(2) by auto moreover from s assms(2) h(2) have "r∈G" using group_op_closed by auto moreover note ‹h¯∈H› ultimately have "r¯∈{g⋅(h⋅g¯). h∈H}" "r∈G" by auto } then have "∀r∈{g⋅(h⋅g¯). h∈H}. r¯∈{g⋅(h⋅g¯). h∈H}" and "{g⋅(h⋅g¯). h∈H}⊆G" by auto moreover { fix s t assume s:"s∈{g⋅(h⋅g¯). h∈H}" and t:"t∈{g⋅(h⋅g¯). h∈H}" then obtain hs ht where hs:"hs∈H" "s=g⋅(hs⋅(g¯))" and ht:"ht∈H" "t=g⋅(ht⋅(g¯))" by auto from hs(1) have "hs∈G" using sub by auto then have "g⋅hs∈G" using group_op_closed assms(2) by auto then have "(g⋅hs)¯∈G" using inverse_in_group by auto from ht(1) have "ht∈G" using sub by auto with ‹g¯:G› have "ht⋅(g¯)∈G" using group_op_closed by auto from hs(2) ht(2) have "s⋅t=(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))" by auto moreover from ‹hs∈G› have "hs⋅ht = hs⋅𝟭⋅ht" using group0_2_L2 by auto then have "hs⋅ht = hs⋅(g¯⋅g)⋅ht" using group0_2_L6 assms(2) by auto then have "g⋅(hs⋅ht) = g⋅(hs⋅(g¯⋅g)⋅ht)" by auto with ‹hs∈G› have "g⋅(hs⋅ht) = g⋅((hs⋅g¯⋅g)⋅ht)" using group_oper_assoc assms(2) inverse_in_group by auto with ‹hs∈G› ‹ht∈G› have "g⋅(hs⋅ht) = g⋅(hs⋅g¯⋅(g⋅ht))" using group_oper_assoc assms(2) inverse_in_group group_op_closed by auto with ‹hs∈G› ‹ht∈G› have "g⋅(hs⋅ht) = g⋅(hs⋅g¯)⋅(g⋅ht)" using group_oper_assoc assms(2) inverse_in_group group_op_closed by auto then have "g⋅(hs⋅ht)⋅g¯ = g⋅(hs⋅g¯)⋅(g⋅ht)⋅g¯" by auto with ‹hs∈G› ‹ht∈G› have "g⋅((hs⋅ht)⋅g¯) = g⋅(hs⋅g¯)⋅(g⋅ht)⋅g¯" using group_oper_assoc inverse_in_group assms(2) group_op_closed by auto with ‹hs∈G› ‹ht∈G› have "g⋅((hs⋅ht)⋅g¯) = (g⋅(hs⋅g¯))⋅(g⋅(ht⋅g¯))" using group_oper_assoc inverse_in_group assms(2) group_op_closed by auto ultimately have "s⋅t=g⋅((hs⋅ht)⋅(g¯))" by auto moreover from hs(1) ht(1) have "hs⋅ht∈H" using assms(1) group0_3_L6 by auto ultimately have "s⋅t∈{g⋅(h⋅g¯). h∈H}" by auto } then have "{g⋅(h⋅g¯). h∈H} {is closed under}P" unfolding IsOpClosed_def by auto moreover from assms(1) have "𝟭∈H" using group0_3_L5 by auto then have "g⋅(𝟭⋅g¯)∈{g⋅(h⋅g¯). h∈H}" by auto then have "{g⋅(h⋅g¯). h∈H}≠0" by auto ultimately show ?thesis using group0_3_T3 by auto qed text‹Every set is equipollent with its conjugates.› theorem (in group0) conj_set_is_eqpoll: assumes "H⊆G" "g∈G" shows "H≈{g⋅(h⋅g¯). h∈H}" proof- have fun:"{⟨h,g⋅(h⋅g¯)⟩. h∈H}:H→{g⋅(h⋅g¯). h∈H}" unfolding Pi_def function_def domain_def by auto { fix h1 h2 assume "h1∈H""h2∈H""{⟨h,g⋅(h⋅g¯)⟩. h∈H}`h1={⟨h,g⋅(h⋅g¯)⟩. h∈H}`h2" with fun have "g⋅(h1⋅g¯)=g⋅(h2⋅g¯)""h1⋅g¯∈G""h2⋅g¯∈G""h1∈G""h2∈G" using apply_equality assms(1) group_op_closed inverse_in_group assms(2) by auto then have "h1⋅g¯=h2⋅g¯" using group0_2_L19(2) assms(2) by auto with ‹h1∈G› ‹h2∈G› have "h1=h2" using group0_2_L19(1) inverse_in_group assms(2) by auto } then have "∀h1∈H. ∀h2∈H. {⟨h,g⋅(h⋅g¯)⟩. h∈H}`h1={⟨h,g⋅(h⋅g¯)⟩. h∈H}`h2 ⟶ h1=h2" by auto with fun have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈inj(H,{g⋅(h⋅g¯). h∈H})" unfolding inj_def by auto moreover { fix ghg assume "ghg∈{g⋅(h⋅g¯). h∈H}" then obtain h where "h∈H" "ghg=g⋅(h⋅g¯)" by auto then have "⟨h,ghg⟩∈{⟨h,g⋅(h⋅g¯)⟩. h∈H}" by auto then have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}`h=ghg" using apply_equality fun by auto with ‹h∈H› have "∃h∈H. {⟨h,g⋅(h⋅g¯)⟩. h∈H}`h=ghg" by auto } with fun have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈surj(H,{g⋅(h⋅g¯). h∈H})" unfolding surj_def by auto ultimately have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈bij(H,{g⋅(h⋅g¯). h∈H})" unfolding bij_def by auto then show ?thesis unfolding eqpoll_def by auto qed text‹Every normal subgroup contains its conjugate subgroups.› theorem (in group0) norm_group_cont_conj: assumes "IsAnormalSubgroup(G,P,H)" "g∈G" shows "{g⋅(h⋅g¯). h∈H}⊆H" proof- { fix r assume "r∈{g⋅(h⋅g¯). h∈H}" then obtain h where h:"r=g⋅(h⋅g¯)" "h∈H" by auto moreover from h(2) have "h∈G" using group0_3_L2 assms(1) unfolding IsAnormalSubgroup_def by auto moreover from assms(2) have "g¯∈G" using inverse_in_group by auto ultimately have "r=g⋅h⋅g¯" "h∈H" using group_oper_assoc assms(2) by auto then have "r∈H" using assms unfolding IsAnormalSubgroup_def by auto } then show "{g⋅(h⋅g¯). h∈H}⊆H" by auto qed text‹If a subgroup contains all its conjugate subgroups, then it is normal.› theorem (in group0) cont_conj_is_normal: assumes "IsAsubgroup(H,P)" "∀g∈G. {g⋅(h⋅g¯). h∈H}⊆H" shows "IsAnormalSubgroup(G,P,H)" proof- { fix h g assume "h∈H" "g∈G" with assms(2) have "g⋅(h⋅g¯)∈H" by auto moreover from ‹g∈G›‹h∈H› have "h∈G" "g¯∈G" "g∈G" using group0_3_L2 assms(1) inverse_in_group by auto ultimately have "g⋅h⋅g¯∈H" using group_oper_assoc by auto } then show ?thesis using assms(1) unfolding IsAnormalSubgroup_def by auto qed text‹If a group has only one subgroup of a given order, then this subgroup is normal.› corollary (in group0) only_one_equipoll_sub: assumes "IsAsubgroup(H,P)" "∀M. IsAsubgroup(M,P)∧ H≈M ⟶ M=H" shows "IsAnormalSubgroup(G,P,H)" proof- { fix g assume g:"g∈G" with assms(1) have "IsAsubgroup({g⋅(h⋅g¯). h∈H},P)" using conj_group_is_group by auto moreover from assms(1) g have "H≈{g⋅(h⋅g¯). h∈H}" using conj_set_is_eqpoll group0_3_L2 by auto ultimately have "{g⋅(h⋅g¯). h∈H}=H" using assms(2) by auto then have "{g⋅(h⋅g¯). h∈H}⊆H" by auto } then show ?thesis using cont_conj_is_normal assms(1) by auto qed text‹The trivial subgroup is then a normal subgroup.› corollary (in group0) trivial_normal_subgroup: shows "IsAnormalSubgroup(G,P,{𝟭})" proof- have "{𝟭}⊆G" using group0_2_L2 by auto moreover have "{𝟭}≠0" by auto moreover { fix a b assume "a∈{𝟭}""b∈{𝟭}" then have "a=𝟭""b=𝟭" by auto then have "P`⟨a,b⟩=𝟭⋅𝟭" by auto then have "P`⟨a,b⟩=𝟭" using group0_2_L2 by auto then have "P`⟨a,b⟩∈{𝟭}" by auto } then have "{𝟭}{is closed under}P" unfolding IsOpClosed_def by auto moreover { fix a assume "a∈{𝟭}" then have "a=𝟭" by auto then have "a¯=𝟭¯" by auto then have "a¯=𝟭" using group_inv_of_one by auto then have "a¯∈{𝟭}" by auto } then have "∀a∈{𝟭}. a¯∈{𝟭}" by auto ultimately have "IsAsubgroup({𝟭},P)" using group0_3_T3 by auto moreover { fix M assume M:"IsAsubgroup(M,P)" "{𝟭}≈M" then have one:"𝟭∈M" "M≈{𝟭}" using eqpoll_sym group0_3_L5 by auto then obtain f where "f∈bij(M,{𝟭})" unfolding eqpoll_def by auto then have inj:"f∈inj(M,{𝟭})" unfolding bij_def by auto then have fun:"f:M→{𝟭}" unfolding inj_def by auto { fix b assume b:"b∈M" "b≠𝟭" with ‹𝟭∈M› have "f`b≠f`𝟭" using inj unfolding inj_def by auto moreover from fun b(1) have "f`b∈{𝟭}" by (rule apply_type) moreover from fun one(1) have "f`𝟭∈{𝟭}" by (rule apply_type) ultimately have "False" by auto } with ‹𝟭∈M› have "M={𝟭}" by auto } ultimately show ?thesis using only_one_equipoll_sub by auto qed text‹The whole group is normal as a subgroup› lemma (in group0) whole_normal_subgroup: shows "IsAnormalSubgroup(G,P,G)" proof- have "G⊆G" by auto moreover have "∀x∈G. x¯∈G" using inverse_in_group by auto moreover have "G≠0" using group0_2_L2 by auto moreover have "G{is closed under}P" using group_op_closed unfolding IsOpClosed_def by auto ultimately have "IsAsubgroup(G,P)" using group0_3_T3 by auto moreover { fix n g assume ng:"n∈G" "g∈G" then have "P ` ⟨P ` ⟨g, n⟩, GroupInv(G, P) ` g⟩ ∈ G" using group_op_closed inverse_in_group by auto } ultimately show ?thesis unfolding IsAnormalSubgroup_def by auto qed subsection‹Simple groups› text‹In this subsection we study the groups that build the rest of the groups: the simple groups.› text‹Since the whole group and the trivial subgroup are always normal, it is natural to define simplicity of groups in the following way:› definition IsSimple ("[_,_]{is a simple group}" 89) where "[G,f]{is a simple group} ≡ IsAgroup(G,f) ∧ (∀M. IsAnormalSubgroup(G,f,M) ⟶ M=G∨M={TheNeutralElement(G,f)})" text‹From the definition follows that if a group has no subgroups, then it is simple.› corollary (in group0) noSubgroup_imp_simple: assumes "∀H. IsAsubgroup(H,P)⟶ H=G∨H={𝟭}" shows "[G,P]{is a simple group}" proof- have "IsAgroup(G,P)" using groupAssum by auto moreover { fix M assume "IsAnormalSubgroup(G,P,M)" then have "IsAsubgroup(M,P)" unfolding IsAnormalSubgroup_def by auto with assms have "M=G∨M={𝟭}" by auto } ultimately show ?thesis unfolding IsSimple_def by auto qed text‹We add a context for an abelian group› locale abelian_group = group0 + assumes isAbelian: "P {is commutative on} G" text‹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]{is a simple group}" shows "∀H. IsAsubgroup(H,P)⟶ H=G∨H={𝟭}" proof- { fix H assume A:"IsAsubgroup(H,P)""H ≠ {𝟭}" then have "IsAnormalSubgroup(G,P,H)" using Group_ZF_2_4_L6(1) groupAssum isAbelian by auto with assms(1) A have "H=G" unfolding IsSimple_def by auto } then show ?thesis by auto qed subsection‹Finite groups› text‹This subsection deals with finite groups and their structure› text‹The subgroup of a finite group is finite.› lemma (in group0) finite_subgroup: assumes "Finite(G)" "IsAsubgroup(H,P)" shows "Finite(H)" using group0_3_L2 subset_Finite assms by force text‹The space of cosets is also finite. In particular, quotient groups.› lemma (in group0) finite_cosets: assumes "Finite(G)" "IsAsubgroup(H,P)" defines "r ≡ QuotientGroupRel(G,P,H)" shows "Finite(G//r)" proof- have fun:"{⟨g,r``{g}⟩. g∈G}:G→(G//r)" unfolding Pi_def function_def domain_def by auto { fix C assume C:"C∈G//r" have equiv:"equiv(G,r)" using Group_ZF_2_4_L3 assms(2) unfolding r_def by auto then have "refl(G,r)" unfolding equiv_def by auto with C have "C≠0" using EquivClass_1_L5 by auto then obtain c where c:"c∈C" by auto with C have "r``{c}=C" using EquivClass_1_L2 equiv by auto with c C have "⟨c,C⟩∈{⟨g,r``{g}⟩. g∈G}" using EquivClass_1_L1 equiv by auto then have "{⟨g,r``{g}⟩. g∈G}`c=C" "c∈G" using apply_equality fun by auto then have "∃c∈G. {⟨g,r``{g}⟩. g∈G}`c=C" by auto } with fun have surj:"{⟨g,r``{g}⟩. g∈G}∈surj(G,G//r)" unfolding surj_def by auto from assms(1) obtain n where "n∈nat" "G≈n" unfolding Finite_def by auto then have G:"G≲n" "Ord(n)" using eqpoll_imp_lepoll by auto then have "G//r≲G" using surj_fun_inv_2 surj by auto with G(1) have "G//r≲n" using lepoll_trans by blast with ‹n∈nat› show "Finite(G//r)" using lepoll_nat_imp_Finite by auto qed text‹All the cosets are equipollent.› lemma (in group0) cosets_equipoll: assumes "IsAsubgroup(H,P)" "g1∈G""g2∈G" defines "r ≡ QuotientGroupRel(G,P,H)" shows "r``{g1} ≈ r``{g2}" proof- have equiv:"equiv(G,r)" using Group_ZF_2_4_L3 assms(1) unfolding r_def by auto from assms(3,2) have GG:"(g1¯)⋅g2∈G" using inverse_in_group group_op_closed by auto then have bij:"RightTranslation(G,P,(g1¯)⋅g2)∈bij(G,G)" using trans_bij(1) by auto have "r``{g2}∈G//r" using assms(3) unfolding quotient_def by auto then have sub2:"r``{g2}⊆G" using EquivClass_1_L1 equiv assms(3) by blast have "r``{g1}∈G//r" using assms(2) unfolding quotient_def by auto then have sub:"r``{g1}⊆G" using EquivClass_1_L1 equiv assms(2) by blast with bij have "restrict(RightTranslation(G,P,(g1¯)⋅g2),r``{g1})∈bij(r``{g1},RightTranslation(G,P,(g1¯)⋅g2)``(r``{g1}))" using restrict_bij unfolding bij_def by auto then have "r``{g1}≈RightTranslation(G,P,(g1¯)⋅g2)``(r``{g1})" unfolding eqpoll_def by auto with GG sub have A0:"r``{g1}≈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" using func_imagedef group0_5_L1(1) by force { fix t assume "t∈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" then obtain q where q:"t=RightTranslation(G,P,(g1¯)⋅g2)`q" "q∈r``{g1}" by auto then have "⟨g1,q⟩∈r" "q∈G" using image_iff sub by auto then have "g1⋅(q¯)∈H" "q¯∈G" using inverse_in_group unfolding r_def QuotientGroupRel_def by auto from GG q sub have t:"t=q⋅((g1¯)⋅g2)" using group0_5_L2(1) by auto then have "g2⋅t¯=g2⋅(q⋅((g1¯)⋅g2))¯" by auto with ‹q∈G› GG have "g2⋅t¯=g2⋅(((g1¯)⋅g2)¯⋅q¯)" using group_inv_of_two by auto then have "g2⋅t¯=g2⋅(((g2¯)⋅g1¯¯)⋅q¯)" using group_inv_of_two inverse_in_group assms(2) assms(3) by auto then have "g2⋅t¯=g2⋅(((g2¯)⋅g1)⋅q¯)" using group_inv_of_inv assms(2) by auto moreover have "(g2¯)⋅g1∈G" using assms(2) inverse_in_group assms(3) group_op_closed by auto with assms(3) ‹q¯∈G› have "g2⋅(((g2¯)⋅g1)⋅q¯)=g2⋅((g2¯)⋅g1)⋅q¯" using group_oper_assoc by auto moreover have "g2⋅((g2¯)⋅g1)=g2⋅(g2¯)⋅g1" using assms(2) inverse_in_group assms(3) group_oper_assoc by auto then have "g2⋅((g2¯)⋅g1)=g1" using group0_2_L6 assms(3) group0_2_L2 assms(2) by auto ultimately have "g2⋅t¯=g1⋅q¯" by auto with ‹g1⋅(q¯)∈H› have "g2⋅t¯∈H" by auto moreover from t ‹q∈G› ‹g2∈G› have "t∈G" using inverse_in_group assms(2) group_op_closed by auto ultimately have "⟨g2,t⟩∈r" unfolding QuotientGroupRel_def r_def using assms(3) by auto then have "t∈r``{g2}" using image_iff assms(4) by auto } then have A1:"{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}⊆r``{g2}" by auto { fix t assume "t∈r``{g2}" then have "⟨g2,t⟩∈r" "t∈G" using sub2 image_iff by auto then have H:"g2⋅t¯∈H" unfolding QuotientGroupRel_def r_def by auto then have G:"g2⋅t¯∈G" using group0_3_L2 assms(1) by auto then have "g1⋅(g1¯⋅(g2⋅t¯))=g1⋅g1¯⋅(g2⋅t¯)" using group_oper_assoc assms(2) inverse_in_group by auto with G have "g1⋅(g1¯⋅(g2⋅t¯))=g2⋅t¯" using group0_2_L6 assms(2) group0_2_L2 by auto with H have HH:"g1⋅(g1¯⋅(g2⋅t¯))∈H" by auto from ‹t∈G› have GGG:"t⋅g2¯∈G" using inverse_in_group assms(3) group_op_closed by auto from ‹t∈G› have "(t⋅g2¯)¯=g2¯¯⋅t¯" using group_inv_of_two inverse_in_group assms(3) by auto also have "…=g2⋅t¯" using group_inv_of_inv assms(3) by auto finally have "(t⋅g2¯)¯=g2⋅t¯" by auto then have "g1¯⋅(t⋅g2¯)¯=g1¯⋅(g2⋅t¯)" by auto then have "((t⋅g2¯)⋅g1)¯=g1¯⋅(g2⋅t¯)" using group_inv_of_two GGG assms(2) by auto then have HHH:"g1⋅((t⋅g2¯)⋅g1)¯∈H" using HH by auto from ‹t∈G› have "(t⋅g2¯)⋅g1∈G" using assms(2) inverse_in_group assms(3) group_op_closed by auto with HHH have "⟨g1,(t⋅g2¯)⋅g1⟩∈r" using assms(2) unfolding r_def QuotientGroupRel_def by auto then have rg1:"t⋅g2¯⋅g1∈r``{g1}" using image_iff by auto from assms(3) have "g2¯:G" using inverse_in_group by auto from ‹t∈G› have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t⋅(g2¯⋅g1)⋅((g1¯)⋅g2)" using group_oper_assoc inverse_in_group assms(3) assms(2) by auto also from ‹t∈G› have "…=t⋅((g2¯⋅g1)⋅((g1¯)⋅g2))" using group_oper_assoc group_op_closed inverse_in_group assms(3) assms(2) by auto also from GG ‹g2¯:G› have "…=t⋅(g2¯⋅(g1⋅((g1¯)⋅g2)))" using group_oper_assoc assms(2) by auto also have "…=t⋅(g2¯⋅(g1⋅(g1¯)⋅g2))" using group_oper_assoc assms(2) inverse_in_group assms(3) by auto also from ‹t∈G› have "…=t" using group0_2_L6 assms(3) group0_2_L6 assms(2) group0_2_L2 assms(3) by auto finally have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t" by auto with ‹(t⋅g2¯)⋅g1∈G› GG have "RightTranslation(G,P,(g1¯)⋅g2)`(t⋅g2¯⋅g1)=t" using group0_5_L2(1) by auto then have "t∈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" using rg1 by force } then have "r``{g2}⊆{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" by blast with A1 have "r``{g2}={RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" by auto with A0 show ?thesis by auto qed text‹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)" "IsAsubgroup(H,P)" defines "r ≡ QuotientGroupRel(G,P,H)" shows "|G|=|H| #* |G//r|" proof- have equiv:"equiv(G,r)" using Group_ZF_2_4_L3 assms(2) unfolding r_def by auto have "r``{𝟭} ⊆G" unfolding r_def QuotientGroupRel_def by auto have "∀aa∈G. aa∈H ⟷ ⟨aa,𝟭⟩∈r" using Group_ZF_2_4_L5C unfolding r_def by auto then have "∀aa∈G. aa∈H ⟷ ⟨𝟭,aa⟩∈r" using equiv unfolding sym_def equiv_def by auto then have "∀aa∈G. aa∈H ⟷ aa∈r``{𝟭}" using image_iff by auto with ‹r``{𝟭} ⊆G› have H:"H=r``{𝟭}" using group0_3_L2 assms(2) by blast { fix c assume "c∈(G//r)" then obtain g where "g∈G" "c=r``{g}" unfolding quotient_def by auto then have "c≈r``{𝟭}" using cosets_equipoll assms(2) group0_2_L2 unfolding r_def by auto then have "|c|=|H|" using H cardinal_cong by auto } then have "∀c∈(G//r). |c|=|H|" by auto moreover have "Finite(G//r)" using assms finite_cosets by auto moreover have "⋃(G//r)=G" using Union_quotient Group_ZF_2_4_L3 assms(2,3) by auto moreover from ‹⋃(G//r)=G› have "Finite(⋃(G//r))" using assms(1) by auto moreover have "∀c1∈(G//r). ∀c2∈(G//r). c1≠c2 ⟶ c1∩c2=0" using quotient_disj equiv by blast ultimately show ?thesis using card_partition by auto qed subsection‹Subgroups generated by sets› text‹In this section we study the minimal subgroup containing a set› text‹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) SubgroupGenerated ("⟨_⟩⇩_{G}" 80) where "X⊆G ⟹ ⟨X⟩⇩_{G}≡ ⋂{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" text‹Every generated subgroup is a subgroup› theorem (in group0) subgroupGen_is_subgroup: assumes "X⊆G" shows "IsAsubgroup(⟨X⟩⇩_{G},P)" proof- have "restrict(P,G×G)=P" using group_oper_fun restrict_idem unfolding Pi_def by auto then have "IsAsubgroup(G,P)" unfolding IsAsubgroup_def using groupAssum by auto with assms have "G∈{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" by auto then have "{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}≠0" by auto then show ?thesis using subgroup_inter SubgroupGenerated_def assms by auto qed text‹The generated subgroup contains the original set› theorem (in group0) subgroupGen_contains_set: assumes "X⊆G" shows "X ⊆ ⟨X⟩⇩_{G}" proof- have "restrict(P,G×G)=P" using group_oper_fun restrict_idem unfolding Pi_def by auto then have "IsAsubgroup(G,P)" unfolding IsAsubgroup_def using groupAssum by auto with assms have "G∈{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" by auto then have "{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}≠0" by auto then show ?thesis using subgroup_inter SubgroupGenerated_def assms by auto qed text‹Given a subgroup that contains a set, the generated subgroup from that set is smaller than this subgroup› theorem (in group0) subgroupGen_minimal: assumes "IsAsubgroup(H,P)" "X⊆H" shows "⟨X⟩⇩_{G}⊆ H" proof- from assms have sub:"X⊆G" using group0_3_L2 by auto from assms have "H∈{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" using group0_3_L2 by auto then show ?thesis using sub subgroup_inter SubgroupGenerated_def assms by auto qed end