Theory Group_ZF_4

(* 
    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