Theory Group_ZF_4

theory Group_ZF_4
imports Group_ZF_1 Group_ZF_2 Ring_ZF Cardinal_ZF Semigroup_ZF
(* 
    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 Ring_ZF
  Cardinal_ZF Semigroup_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{*The conjugate of a subgroup is a subgroup.*}

theorem(in group0) semigr0:
  shows "semigr0(G,P)"
  unfolding semigr0_def using groupAssum IsAgroup_def IsAmonoid_def by auto

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[OF assms(2)] by auto
    moreover
    from s assms(2) h(2) have r:"r∈G" using group_op_closed by auto
    have "(h⋅(g¯))¯=(g¯)¯⋅h¯" using group_inv_of_two[OF `h∈G``g¯∈G`] by auto
    moreover have "(g¯)¯=g" using group_inv_of_inv[OF assms(2)] by auto
    ultimately have "r¯=(g⋅(h¯))⋅(g)¯" by auto
    then have "r¯=g⋅((h¯)⋅(g)¯)" using group_oper_assoc[OF assms(2) `h¯∈G``g¯∈G`] by auto
    with `h¯∈H` r 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
    have "g⋅(hs⋅(g¯))=g⋅hs⋅(g¯)" using group_oper_assoc[OF assms(2) `hs∈G` `g¯∈G`] by auto
    then have "(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))=(g⋅hs⋅(g¯))⋅(g⋅(ht⋅(g¯)))" by auto
    then have "(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))=(g⋅hs⋅(g¯))⋅(g¯¯⋅(ht⋅(g¯)))" using group_inv_of_inv[OF assms(2)] by auto
    also have "…=g⋅hs⋅(ht⋅(g¯))" using group0_2_L14A(2)[OF `(g⋅hs)¯∈G` `g¯∈G``ht⋅(g¯)∈G`] group_inv_of_inv[OF `(g⋅hs)∈G`]
      by auto
    ultimately have "s⋅t=g⋅hs⋅(ht⋅(g¯))" by auto moreover
    have "hs⋅(ht⋅(g¯))=(hs⋅ht)⋅(g¯)" using group_oper_assoc[OF `hs∈G``ht∈G``g¯∈G`] by auto moreover 
    have "g⋅hs⋅(ht⋅(g¯))=g⋅(hs⋅(ht⋅(g¯)))" using group_oper_assoc[OF `g∈G``hs∈G``(ht⋅g¯)∈G`] 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[OF _ inverse_in_group[OF assms(2)]] by auto
    then have "h1⋅g¯=h2⋅g¯" using group0_2_L19(2)[OF `h1⋅g¯∈G` `h2⋅g¯∈G` assms(2)] by auto
    then have "h1=h2" using group0_2_L19(1)[OF `h1∈G``h2∈G` inverse_in_group[OF 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 "r=g⋅(h⋅g¯)" "h∈H" by auto moreover
    then 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 have "h∈G""g¯∈G" using group0_3_L2 assms(1) `g∈G``h∈H` inverse_in_group by auto
    ultimately have "g⋅h⋅g¯∈H" using group_oper_assoc `g∈G` 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 "𝟭∈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∈M""b≠𝟭"
      then have "f`b≠f`𝟭" using inj `𝟭∈M` unfolding inj_def by auto
      then have "False" using `b∈M` `𝟭∈M` apply_type[OF fun] by auto
    }
    then have "M={𝟭}" using `𝟭∈M` by auto
  }
  ultimately show ?thesis using only_one_equipoll_sub by auto
qed

lemma(in group0) whole_normal_subgroup:
  shows "IsAnormalSubgroup(G,P,G)"
  unfolding IsAnormalSubgroup_def
  using group_op_closed inverse_in_group
  using group0_2_L2 group0_3_T3[of "G"] unfolding IsOpClosed_def
    by auto

text{*Since the whole group and the trivial subgroup are 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. 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{*Since every subgroup is normal in abelian
groups, it follows that commutative simple groups
do not have subgroups.*}

corollary (in group0) abelian_simple_noSubgroups:
  assumes "[G,P]{is a simple group}" "P{is commutative on}G"
  shows "∀H. IsAsubgroup(H,P)⟶ H=G∨H={𝟭}"
proof(safe)
  fix H assume A:"IsAsubgroup(H,P)""H ≠ {𝟭}"
  then have "IsAnormalSubgroup(G,P,H)" using Group_ZF_2_4_L6(1) groupAssum assms(2)
    by auto
  with assms(1) A show "H=G" unfolding IsSimple_def by auto
qed

subsection{*Finite groups*}

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)" "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"
    then obtain c where c:"c∈C" using EquivClass_1_L5[OF Group_ZF_2_4_L1[OF assms(2)]] assms(3) by auto
    with C have "r``{c}=C" using EquivClass_1_L2[OF Group_ZF_2_4_L3] assms(2,3) by auto
    with c C have "⟨c,C⟩∈{⟨g,r``{g}⟩. g∈G}" using EquivClass_1_L1[OF Group_ZF_2_4_L3] assms(2,3)
      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 moreover
  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
  then show "Finite(G//r)" using lepoll_nat_imp_Finite `n∈nat` by auto
qed

text{*All the cosets are equipollent.*}

lemma(in group0) cosets_equipoll:
  assumes "IsAsubgroup(H,P)" "r=QuotientGroupRel(G,P,H)" "g1∈G""g2∈G"
  shows "r``{g1}≈r``{g2}"
proof-
  from assms(3,4) have GG:"(g1¯)⋅g2∈G" using inverse_in_group group_op_closed by auto
  then have "RightTranslation(G,P,(g1¯)⋅g2)∈bij(G,G)" using trans_bij(1) by auto moreover
  have sub2:"r``{g2}⊆G" using EquivClass_1_L1[OF Group_ZF_2_4_L3[OF assms(1)]] assms(2,4) unfolding quotient_def by auto
  have sub:"r``{g1}⊆G" using EquivClass_1_L1[OF Group_ZF_2_4_L3[OF assms(1)]] assms(2,3) unfolding quotient_def by auto
  ultimately 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
  then have A0:"r``{g1}≈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}"
    using func_imagedef[OF group0_5_L1(1)[OF GG] sub] by auto
  {
    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 assms(2) inverse_in_group unfolding QuotientGroupRel_def by auto
    from q(1) have t:"t=q⋅((g1¯)⋅g2)" using group0_5_L2(1)[OF GG] q(2) sub by auto
    then have "g2⋅t¯=g2⋅(q⋅((g1¯)⋅g2))¯" by auto
    then have "g2⋅t¯=g2⋅(((g1¯)⋅g2)¯⋅q¯)" using group_inv_of_two[OF `q∈G` GG] by auto
    then have "g2⋅t¯=g2⋅(((g2¯)⋅g1¯¯)⋅q¯)" using group_inv_of_two[OF inverse_in_group[OF assms(3)] 
      assms(4)] by auto
    then have "g2⋅t¯=g2⋅(((g2¯)⋅g1)⋅q¯)" using group_inv_of_inv assms(3) by auto moreover
    have "t∈G" using t `q∈G` `g2∈G` inverse_in_group[OF assms(3)] group_op_closed by auto
    have "(g2¯)⋅g1∈G" using assms(3) inverse_in_group[OF assms(4)] group_op_closed by auto
    with assms(4) `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(3) inverse_in_group[OF assms(4)] assms(4)
      group_oper_assoc by auto
    then have "g2⋅((g2¯)⋅g1)=g1" using group0_2_L6[OF assms(4)] group0_2_L2 assms(3) by auto ultimately
    have "g2⋅t¯=g1⋅q¯" by auto
    with `g1⋅(q¯)∈H` have "g2⋅t¯∈H" by auto
    then have "⟨g2,t⟩∈r" using assms(2) unfolding QuotientGroupRel_def using assms(4) `t∈G` 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" using assms(2) unfolding QuotientGroupRel_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[OF assms(3) inverse_in_group[OF assms(3)]]
      by auto
    then have "g1⋅(g1¯⋅(g2⋅t¯))=g2⋅t¯" using group0_2_L6[OF assms(3)] group0_2_L2 G by auto
    with H have HH:"g1⋅(g1¯⋅(g2⋅t¯))∈H" by auto
    have GGG:"t⋅g2¯∈G" using `t∈G` inverse_in_group[OF assms(4)] group_op_closed by auto
    have "(t⋅g2¯)¯=g2¯¯⋅t¯" using group_inv_of_two[OF `t∈G` inverse_in_group[OF assms(4)]] by auto
    also have "…=g2⋅t¯" using group_inv_of_inv[OF assms(4)] by auto
    ultimately 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[OF GGG assms(3)] by auto
    then have HHH:"g1⋅((t⋅g2¯)⋅g1)¯∈H" using HH by auto
    have "(t⋅g2¯)⋅g1∈G" using assms(3) `t∈G` inverse_in_group[OF assms(4)] group_op_closed by auto
    with HHH have "⟨g1,(t⋅g2¯)⋅g1⟩∈r" using assms(2,3) unfolding QuotientGroupRel_def by auto
    then have rg1:"t⋅g2¯⋅g1∈r``{g1}" using image_iff by auto
    have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t⋅(g2¯⋅g1)⋅((g1¯)⋅g2)" using group_oper_assoc[OF `t∈G` inverse_in_group[OF assms(4)] assms(3)]
      by auto
    also have "…=t⋅((g2¯⋅g1)⋅((g1¯)⋅g2))" using group_oper_assoc[OF `t∈G` group_op_closed[OF inverse_in_group[OF assms(4)] assms(3)] GG]
      by auto
    also have "…=t⋅(g2¯⋅(g1⋅((g1¯)⋅g2)))" using group_oper_assoc[OF inverse_in_group[OF assms(4)] assms(3) GG] by auto
    also have "…=t⋅(g2¯⋅(g1⋅(g1¯)⋅g2))" using group_oper_assoc[OF assms(3) inverse_in_group[OF assms(3)] assms(4)] by auto
    also have "…=t" using group0_2_L6[OF assms(3)]group0_2_L6[OF assms(4)] group0_2_L2 `t∈G` assms(4) by auto
    ultimately have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t" by auto
    then have "RightTranslation(G,P,(g1¯)⋅g2)`(t⋅g2¯⋅g1)=t" using group0_5_L2(1)[OF GG] `(t⋅g2¯)⋅g1∈G` 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)" "r=QuotientGroupRel(G,P,H)"
  shows "|G|=|H| #* |G//r|"
proof-
  have "Finite(G//r)" using assms finite_cosets by auto moreover
  have un:"⋃(G//r)=G" using Union_quotient Group_ZF_2_4_L3 assms(2,3) by auto
  then 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[OF Group_ZF_2_4_L3[OF assms(2)]]
    assms(3) by auto moreover
  have "∀aa∈G. aa∈H ⟷ ⟨aa,𝟭⟩∈r" using Group_ZF_2_4_L5C assms(3) by auto
  then have "∀aa∈G. aa∈H ⟷ ⟨𝟭,aa⟩∈r" using Group_ZF_2_4_L2 assms(2,3) unfolding sym_def
    by auto
  then have "∀aa∈G. aa∈H ⟷ aa∈r``{𝟭}" using image_iff by auto
  then have H:"H=r``{𝟭}" using group0_3_L2[OF assms(2)] assms(3) unfolding QuotientGroupRel_def by auto
  {
    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[OF assms(2,3)] group0_2_L2 by auto
    then have "|c|=|H|" using H cardinal_cong by auto
  }
  then have "∀c∈(G//r). |c|=|H|" by auto ultimately
  show ?thesis using card_partition un by auto
qed

subsection{*Subgroups generated by sets*}

text{*Given a subset of a group, we can ask ourselves which is the 
  smallest group that contains that set; if it even exists.*}

lemma(in group0) inter_subgroups:
  assumes "∀H∈ℌ. IsAsubgroup(H,P)" "ℌ≠0"
  shows "IsAsubgroup(⋂ℌ,P)"
proof-
  from assms have "𝟭∈⋂ℌ" using group0_3_L5 by auto
  then have "⋂ℌ≠0" by auto moreover
  {
    fix A B assume "A∈⋂ℌ""B∈⋂ℌ"
    then have "∀H∈ℌ. A∈H∧B∈H" by auto
    then have "∀H∈ℌ. A⋅B∈H" using assms(1) group0_3_L6 by auto
    then have "A⋅B∈⋂ℌ" using assms(2) by auto
  }
  then have "(⋂ℌ){is closed under}P" using IsOpClosed_def by auto moreover
  {
    fix A assume "A∈⋂ℌ"
    then have "∀H∈ℌ. A∈H" by auto
    then have "∀H∈ℌ. A¯∈H" using assms(1) group0_3_T3A by auto
    then have "A¯∈⋂ℌ" using assms(2) by auto
  }
  then have "∀A∈⋂ℌ. A¯∈⋂ℌ" by auto moreover
  have "⋂ℌ⊆G" using assms(1,2) group0_3_L2 by force
  ultimately show ?thesis using group0_3_T3 by auto
qed

text{*As the previous lemma states, the subgroup that contains a subset
can be defined as an intersection of subgroups.*}

definition(in group0)
  SubgroupGenerated ("⟨_⟩G" 80)
  where "⟨X⟩G ≡ ⋂{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}"

theorem(in group0) subgroupGen_is_subgroup:
  assumes "X⊆G"
  shows "IsAsubgroup(⟨X⟩G,P)"
proof-
  have "restrict(P,G×G)=P" using group_oper_assocA 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 inter_subgroups unfolding SubgroupGenerated_def by auto
qed

subsection{*Homomorphisms*}

text{*A homomorphism is a function between groups that preserves
group operations.*}

definition
  Homomor ("_{is a homomorphism}{_,_}→{_,_}" 85)
  where "IsAgroup(G,P) ⟹ IsAgroup(H,F) ⟹ Homomor(f,G,P,H,F) ≡ ∀g1∈G. ∀g2∈G. f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩"

text{*Now a lemma about the definition:*}

lemma homomor_eq:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g1∈G" "g2∈G"
  shows "f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩"
  using assms Homomor_def by auto

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

definition
  End
  where "End(G,P) ≡ {f:G→G. Homomor(f,G,P,G,P)}"

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

lemma(in group0) end_composition:
  assumes "f1∈End(G,P)""f2∈End(G,P)"
  shows "Composition(G)`⟨f1,f2⟩∈End(G,P)"
proof-
  from assms have fun:"f1:G→G""f2:G→G" unfolding End_def by auto
  then have fun2:"f1 O f2:G→G" using comp_fun by auto
  have comp:"Composition(G)`⟨f1,f2⟩=f1 O f2" using func_ZF_5_L2 fun by auto
  {
    fix g1 g2 assume AS2:"g1∈G""g2∈G"
    then have g1g2:"g1⋅g2∈G" using group_op_closed by auto
    from fun2 have "(f1 O f2)`(g1⋅g2)=f1`(f2`(g1⋅g2))" using comp_fun_apply fun(2) g1g2 by auto
    also have "…=f1`((f2`g1)⋅(f2`g2))" using assms(2) unfolding End_def Homomor_def[OF groupAssum groupAssum]
      using AS2 by auto moreover
    have "f2`g1∈G""f2`g2∈G" using fun(2) AS2 apply_type by auto ultimately
    have "(f1 O f2)`(g1⋅g2)=(f1`(f2`g1))⋅(f1`(f2`g2))" using assms(1) unfolding End_def Homomor_def[OF groupAssum groupAssum]
      using AS2 by auto
    then have "(f1 O f2)`(g1⋅g2)=((f1 O f2)`g1)⋅((f1 O f2)`g2)" using comp_fun_apply fun(2) AS2 by auto
  }
  then have "∀g1∈G. ∀g2∈G. (f1 O f2)`(g1⋅g2)=((f1 O f2)`g1)⋅((f1 O f2)`g2)" by auto
  then have "(f1 O f2)∈End(G,P)" unfolding End_def Homomor_def[OF groupAssum groupAssum] using fun2 by auto
  with comp show "Composition(G)`⟨f1,f2⟩∈End(G,P)" by auto
qed

theorem(in group0) end_comp_monoid:
  shows "IsAmonoid(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))"
  and "TheNeutralElement(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))=id(G)"
proof-
  have fun:"id(G):G→G" unfolding id_def by auto
  {
    fix g h assume "g∈G""h∈G"
    then have id:"g⋅h∈G""id(G)`g=g""id(G)`h=h" using group_op_closed by auto
    then have "id(G)`(g⋅h)=g⋅h" unfolding id_def by auto
    with id(2,3) have "id(G)`(g⋅h)=(id(G)`g)⋅(id(G)`h)" by auto
  }
  with fun have "id(G)∈End(G,P)" unfolding End_def Homomor_def[OF groupAssum groupAssum] by auto moreover
  from Group_ZF_2_5_L2(2) have A0:"id(G)=TheNeutralElement(G → G, Composition(G))" by auto ultimately
  have A1:"TheNeutralElement(G → G, Composition(G))∈End(G,P)" by auto moreover
  have A2:"End(G,P)⊆G→G" unfolding End_def by auto moreover
  from end_composition have A3:"End(G,P){is closed under}Composition(G)" unfolding IsOpClosed_def by auto
  ultimately show "IsAmonoid(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))" 
    using monoid0.group0_1_T1 unfolding monoid0_def using Group_ZF_2_5_L2(1)
    by force
  have "IsAmonoid(G→G,Composition(G))" using Group_ZF_2_5_L2(1) by auto
  with A0 A1 A2 A3 show "TheNeutralElement(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))=id(G)"
    using group0_1_L6 by auto
qed

text{*The set of endomorphisms is closed under pointwise addition. This is so because the
group is abelian.*}
  
theorem(in group0) end_pointwise_addition:
  assumes "f∈End(G,P)""g∈End(G,P)""P{is commutative on}G""F = P {lifted to function space over} G"
  shows "F`⟨f,g⟩∈End(G,P)"
proof-
  from assms(1,2) have fun:"f∈G→G""g∈G→G" unfolding End_def by auto
  then have fun2:"F`⟨f,g⟩:G→G" using monoid0.Group_ZF_2_1_L0 group0_2_L1 assms(4) by auto
  {
    fix g1 g2 assume AS:"g1∈G""g2∈G"
    then have "g1⋅g2∈G" using group_op_closed by auto
    then have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1⋅g2))⋅(g`(g1⋅g2))" using Group_ZF_2_1_L3 fun assms(4) by auto
    also have "…=(f`(g1)⋅f`(g2))⋅(g`(g1)⋅g`(g2))" using assms unfolding End_def Homomor_def[OF groupAssum groupAssum]
      using AS by auto ultimately
    have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1)⋅f`(g2))⋅(g`(g1)⋅g`(g2))" by auto moreover
    have "f`g1∈G""f`g2∈G""g`g1∈G""g`g2∈G" using fun apply_type AS by auto ultimately
    have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1)⋅g`(g1))⋅(f`(g2)⋅g`(g2))" using group0_4_L8(3) assms(3)
      by auto
    with AS have "(F`⟨f,g⟩)`(g1⋅g2)=((F`⟨f,g⟩)`g1)⋅((F`⟨f,g⟩)`g2)"
      using Group_ZF_2_1_L3 fun assms(4) by auto
  }
  with fun2 show ?thesis unfolding End_def Homomor_def[OF groupAssum groupAssum] by auto
qed

text{*The inverse of an abelian group is an endomorphism.*}

lemma(in group0) end_inverse_group:
  assumes "P{is commutative on}G"
  shows "GroupInv(G,P)∈End(G,P)"
proof-
  {
    fix s t assume AS:"s∈G""t∈G"
    then have elinv:"s¯∈G""t¯∈G" using inverse_in_group by auto
    have "(s⋅t)¯=t¯⋅s¯" using group_inv_of_two AS by auto
    then have "(s⋅t)¯=s¯⋅t¯" using assms(1) elinv unfolding IsCommutative_def by auto
  }
  then have "∀s∈G. ∀t∈G. GroupInv(G,P)`(s⋅t)=GroupInv(G,P)`(s)⋅GroupInv(G,P)`(t)" by auto
  with group0_2_T2 groupAssum show ?thesis unfolding End_def using Homomor_def by auto
qed

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

theorem(in group0) end_addition_group:
  assumes "P{is commutative on}G" "F = P {lifted to function space over} G"
  shows "IsAgroup(End(G,P),restrict(F,End(G,P)×End(G,P)))" "restrict(F,End(G,P)×End(G,P)){is commutative on}End(G,P)"
proof-
  from end_comp_monoid(1) monoid0.group0_1_L3A have "End(G,P)≠0" unfolding monoid0_def by auto
  moreover have "End(G,P)⊆G→G" unfolding End_def by auto moreover
  have "End(G,P){is closed under}F" unfolding IsOpClosed_def using end_pointwise_addition
    assms(1,2) by auto moreover
  {
    fix ff assume AS:"ff∈End(G,P)"
    then have "restrict(Composition(G),End(G,P)×End(G,P))`⟨GroupInv(G,P), ff⟩∈End(G,P)" using monoid0.group0_1_L1
      unfolding monoid0_def using end_composition(1) end_inverse_group[OF assms(1)]
      by force
    then have "Composition(G)`⟨GroupInv(G,P), ff⟩∈End(G,P)" using AS end_inverse_group[OF assms(1)]
      by auto
    then have "GroupInv(G,P) O ff∈End(G,P)" using func_ZF_5_L2 AS group0_2_T2 groupAssum unfolding
      End_def by auto
    then have "GroupInv(G→G,F)`ff∈End(G,P)" using Group_ZF_2_1_L6 assms(2) AS unfolding End_def
      by auto
  }
  then have "∀ff∈End(G,P). GroupInv(G→G,F)`ff∈End(G,P)" by auto ultimately
  show "IsAgroup(End(G,P),restrict(F,End(G,P)×End(G,P)))" using group0.group0_3_T3 Group_ZF_2_1_T2[OF assms(2)] unfolding IsAsubgroup_def group0_def
    by auto
  show "restrict(F,End(G,P)×End(G,P)){is commutative on}End(G,P)" using Group_ZF_2_1_L7[OF assms(2,1)] unfolding End_def IsCommutative_def by auto
qed

lemma(in group0) distributive_comp_pointwise:
  assumes "P{is commutative on}G" "F = P {lifted to function space over} G"
  shows "IsDistributive(End(G,P),restrict(F,End(G,P)×End(G,P)),restrict(Composition(G),End(G,P)×End(G,P)))"
proof-
  {
    fix b c d assume AS:"b∈End(G,P)""c∈End(G,P)""d∈End(G,P)"
    have ig1:"Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =b O (F`⟨c,d⟩)" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)]
      AS unfolding End_def using func_ZF_5_L2 by auto
    have ig2:"F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩=F `⟨b O c,b O d⟩" using AS unfolding End_def using func_ZF_5_L2 by auto
    have comp1fun:"(b O (F`⟨c,d⟩)):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force
    have comp2fun:"(F `⟨b O c,b O d⟩):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force
    {
      fix g assume gG:"g∈G"
      then have "(b O (F`⟨c,d⟩))`g=b`((F`⟨c,d⟩)`g)" using comp_fun_apply monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)]
        AS(2,3) unfolding End_def by force
      also have "…=b`(c`(g)⋅d`(g))" using Group_ZF_2_1_L3[OF assms(2)] AS(2,3) gG unfolding End_def by auto
      ultimately have "(b O (F`⟨c,d⟩))`g=b`(c`(g)⋅d`(g))" by auto moreover
      have "c`g∈G""d`g∈G" using AS(2,3) unfolding End_def using apply_type gG by auto
      ultimately have "(b O (F`⟨c,d⟩))`g=(b`(c`g))⋅(b`(d`g))" using AS(1) unfolding End_def
        Homomor_def[OF groupAssum groupAssum] by auto
      then have "(b O (F`⟨c,d⟩))`g=((b O c)`g)⋅((b O d)`g)" using comp_fun_apply gG AS(2,3)
        unfolding End_def by auto
      then have "(b O (F`⟨c,d⟩))`g=(F`⟨b O c,b O d⟩)`g" using gG Group_ZF_2_1_L3[OF assms(2) comp_fun comp_fun gG]
        AS unfolding End_def by auto
    }
    then have "∀g∈G. (b O (F`⟨c,d⟩))`g=(F`⟨b O c,b O d⟩)`g" by auto
    then have "b O (F`⟨c,d⟩)=F`⟨b O c,b O d⟩" using fun_extension[OF comp1fun comp2fun] by auto
    with ig1 ig2 have "Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩" by auto moreover
    have "F ` ⟨c, d⟩=restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩" using AS(2,3) restrict by auto moreover
    have "Composition(G) `⟨b , c⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩" "Composition(G) `⟨b , d⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , d⟩"
      using restrict AS by auto moreover
    have "Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, F ` ⟨c, d⟩⟩" using AS(1)
      end_pointwise_addition[OF AS(2,3) assms] by auto
    moreover have "F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩=restrict(F,End(G,P)×End(G,P)) `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩"
      using end_composition[OF AS(1,2)] end_composition[OF AS(1,3)] by auto ultimately
    have eq1:"restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨b , d⟩⟩"
      by auto
    have ig1:"Composition(G) `⟨ F ` ⟨c, d⟩,b⟩ = (F`⟨c,d⟩) O b" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)]
      AS unfolding End_def using func_ZF_5_L2 by auto
    have ig2:"F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩=F `⟨c O b,d O b⟩" using AS unfolding End_def using func_ZF_5_L2 by auto
    have comp1fun:"((F`⟨c,d⟩) O b):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force
    have comp2fun:"(F `⟨c O b,d O b⟩):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force
    {
      fix g assume gG:"g∈G"
      then have bg:"b`g∈G" using AS(1) unfolding End_def using apply_type by auto
      from gG have "((F`⟨c,d⟩) O b)`g=(F`⟨c,d⟩)`(b`g)" using comp_fun_apply AS(1) unfolding End_def by force
      also have "…=(c`(b`g))⋅(d`(b`g))" using Group_ZF_2_1_L3[OF assms(2)] AS(2,3) bg unfolding End_def by auto
      also  have "…=((c O b)`g)⋅((d O b)`g)" using comp_fun_apply gG AS unfolding End_def by auto
      also have "…=(F`⟨c O b,d O b⟩)`g" using gG Group_ZF_2_1_L3[OF assms(2) comp_fun comp_fun gG]
        AS unfolding End_def by auto
      ultimately have"((F`⟨c,d⟩) O b)`g=(F`⟨c O b,d O b⟩)`g" by auto
    }
    then have "∀g∈G. ((F`⟨c,d⟩) O b)`g=(F`⟨c O b,d O b⟩)`g" by auto
    then have "(F`⟨c,d⟩) O b=F`⟨c O b,d O b⟩" using fun_extension[OF comp1fun comp2fun] by auto
    with ig1 ig2 have "Composition(G) `⟨F ` ⟨c, d⟩,b⟩ =F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩" by auto moreover
    have "F ` ⟨c, d⟩=restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩" using AS(2,3) restrict by auto moreover
    have "Composition(G) `⟨c , b⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨c , b⟩" "Composition(G) `⟨d , b⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨d , b⟩"
      using restrict AS by auto moreover
    have "Composition(G) `⟨F ` ⟨c, d⟩,b⟩ =restrict(Composition(G),End(G,P)×End(G,P)) `⟨F ` ⟨c, d⟩,b⟩" using AS(1)
      end_pointwise_addition[OF AS(2,3) assms] by auto
    moreover have "F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩=restrict(F,End(G,P)×End(G,P)) `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩"
      using end_composition[OF AS(2,1)] end_composition[OF AS(3,1)] by auto ultimately
    have eq2:"restrict(Composition(G),End(G,P)×End(G,P)) `⟨ restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩,b⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨c ,b⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨d , b⟩⟩"
      by auto
    with eq1 have "(restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨b , d⟩⟩)∧
      (restrict(Composition(G),End(G,P)×End(G,P)) `⟨ restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩,b⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨c ,b⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨d , b⟩⟩)"
      by auto
  }
  then show ?thesis unfolding IsDistributive_def by auto
qed

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

theorem(in group0) end_is_ring:
  assumes "P{is commutative on}G" "F = P {lifted to function space over} G"
  shows "IsAring(End(G,P),restrict(F,End(G,P)×End(G,P)),restrict(Composition(G),End(G,P)×End(G,P)))"
  unfolding IsAring_def using end_addition_group[OF assms] end_comp_monoid(1) distributive_comp_pointwise[OF assms]
  by auto

subsection{*First isomorphism theorem*}

text{*Now we will prove that any homomorphism $f:G\to H$ defines a bijective
homomorphism between $G/H$ and $f(G)$.*}
  
text{*A group homomorphism sends the neutral element to the neutral element
and commutes with the inverse.*}

lemma image_neutral:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H"
  shows "f`TheNeutralElement(G,P)=TheNeutralElement(H,F)"
proof-
  have g:"TheNeutralElement(G,P)=P`⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩" "TheNeutralElement(G,P)∈G"
    using assms(1) group0.group0_2_L2 unfolding group0_def by auto
  from g(1) have "f`TheNeutralElement(G,P)=f`(P`⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩)" by auto
  also have "…=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩"
    using assms(3) unfolding Homomor_def[OF assms(1,2)] using g(2) by auto
  ultimately have "f`TheNeutralElement(G,P)=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩" by auto moreover
  have h:"f`TheNeutralElement(G,P)∈H" using g(2) apply_type[OF assms(4)] by auto
  then have "f`TheNeutralElement(G,P)=F`⟨f`TheNeutralElement(G,P),TheNeutralElement(H,F)⟩"
    using assms(2) group0.group0_2_L2 unfolding group0_def by auto ultimately
  have "F`⟨f`TheNeutralElement(G,P),TheNeutralElement(H,F)⟩=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩" by auto
  with h have "LeftTranslation(H,F,f`TheNeutralElement(G,P))`TheNeutralElement(H,F)=LeftTranslation(H,F,f`TheNeutralElement(G,P))`(f`TheNeutralElement(G,P))"
    using group0.group0_5_L2(2)[OF _ h] assms(2) group0.group0_2_L2 unfolding group0_def by auto
  moreover have "LeftTranslation(H,F,f`TheNeutralElement(G,P))∈bij(H,H)" using group0.trans_bij(2)
    assms(2) h unfolding group0_def by auto
  then have "LeftTranslation(H,F,f`TheNeutralElement(G,P))∈inj(H,H)" unfolding bij_def by auto ultimately
  show "f`TheNeutralElement(G,P)=TheNeutralElement(H,F)" using h assms(2) group0.group0_2_L2 unfolding inj_def group0_def
    by force
qed

lemma image_inv:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" "g∈G"
  shows "f`( GroupInv(G,P)`g)=GroupInv(H,F)` (f`g)"
proof-
  have im:"f`g∈H" using apply_type[OF assms(4,5)].
  have inv:"GroupInv(G,P)`g∈G" using group0.inverse_in_group[OF _ assms(5)] assms(1) unfolding group0_def by auto
  then have inv2:"f`(GroupInv(G,P)`g)∈H"using apply_type[OF assms(4)] by auto
  have "f`TheNeutralElement(G,P)=f`(P`⟨g,GroupInv(G,P)`g⟩)" using assms(1,5) group0.group0_2_L6
    unfolding group0_def by auto
  also have "…=F`⟨f`g,f`(GroupInv(G,P)`g)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)] using
    assms(5) inv by auto
  ultimately have "TheNeutralElement(H,F)=F`⟨f`g,f`(GroupInv(G,P)`g)⟩" using image_neutral[OF assms(1-4)]
    by auto
  then show ?thesis using group0.group0_2_L9(2)[OF _ im inv2] assms(2) unfolding group0_def by auto
qed

text{*The kernel of an homomorphism is a normal subgroup.*}

theorem kerner_normal_sub:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H"
  shows "IsAnormalSubgroup(G,P,f-``{TheNeutralElement(H,F)})"
proof-
  have xy:"∀x y. ⟨x, y⟩ ∈ f ⟶ (∀y'. ⟨x, y'⟩ ∈ f ⟶ y = y')" using assms(4) unfolding Pi_def function_def
    by force 
  {
    fix g1 g2 assume "g1∈f-``{TheNeutralElement(H,F)}""g2∈f-``{TheNeutralElement(H,F)}"
    then have "⟨g1,TheNeutralElement(H,F)⟩∈f""⟨g2,TheNeutralElement(H,F)⟩∈f"
      using vimage_iff by auto moreover
    then have G:"g1∈G""g2∈G" using assms(4) unfolding Pi_def by auto
    then have "⟨g1,f`g1⟩∈f""⟨g2,f`g2⟩∈f" using apply_Pair[OF assms(4)] by auto moreover
    note xy ultimately
    have "f`g1=TheNeutralElement(H,F)""f`g2=TheNeutralElement(H,F)" by auto moreover
    have "f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩" using assms(3) G unfolding Homomor_def[OF assms(1,2)] by auto
    ultimately have "f`(P`⟨g1,g2⟩)=F`⟨TheNeutralElement(H,F),TheNeutralElement(H,F)⟩" by auto
    also have "…=TheNeutralElement(H,F)" using group0.group0_2_L2 assms(2) unfolding group0_def
      by auto
    ultimately have "f`(P`⟨g1,g2⟩)=TheNeutralElement(H,F)" by auto moreover
    from G have "P`⟨g1,g2⟩∈G" using group0.group_op_closed assms(1) unfolding group0_def by auto
    ultimately have "⟨P`⟨g1,g2⟩,TheNeutralElement(H,F)⟩∈f" using apply_Pair[OF assms(4)] by force
    then have "P`⟨g1,g2⟩∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto
  }
  then have "f-``{TheNeutralElement(H,F)} {is closed under}P" unfolding IsOpClosed_def by auto
  moreover have A:"f-``{TheNeutralElement(H,F)} ⊆ G" using func1_1_L3 assms(4) by auto
  moreover have "f`TheNeutralElement(G,P)=TheNeutralElement(H,F)" using image_neutral
    assms by auto
  then have "⟨TheNeutralElement(G,P),TheNeutralElement(H,F)⟩∈f" using apply_Pair[OF assms(4)]
    group0.group0_2_L2 assms(1) unfolding group0_def by force
  then have "TheNeutralElement(G,P)∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto
  then have "f-``{TheNeutralElement(H,F)}≠0" by auto moreover
  {
    fix x assume "x∈f-``{TheNeutralElement(H,F)}"
    then have "⟨x,TheNeutralElement(H,F)⟩∈f" and x:"x∈G" using vimage_iff A by auto moreover
    from x have "⟨x,f`x⟩∈f" using apply_Pair[OF assms(4)] by auto ultimately
    have "f`x=TheNeutralElement(H,F)" using xy by auto moreover
    have "f`(GroupInv(G,P)`x)=GroupInv(H,F)`(f`x)" using x image_inv assms by auto
    ultimately have "f`(GroupInv(G,P)`x)=GroupInv(H,F)`TheNeutralElement(H,F)" by auto
    then have "f`(GroupInv(G,P)`x)=TheNeutralElement(H,F)" using group0.group_inv_of_one
      assms(2) unfolding group0_def by auto moreover
    have "⟨GroupInv(G,P)`x,f`(GroupInv(G,P)`x)⟩∈f" using apply_Pair[OF assms(4)]
      x group0.inverse_in_group assms(1) unfolding group0_def by auto
    ultimately have "⟨GroupInv(G,P)`x,TheNeutralElement(H,F)⟩∈f" by auto
    then have "GroupInv(G,P)`x∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto
  }
  then have "∀x∈f-``{TheNeutralElement(H,F)}. GroupInv(G,P)`x∈f-``{TheNeutralElement(H,F)}" by auto
  ultimately have SS:"IsAsubgroup(f-``{TheNeutralElement(H,F)},P)" using group0.group0_3_T3
    assms(1) unfolding group0_def by auto
  {
    fix g h assume AS:"g∈G""h∈f-``{TheNeutralElement(H,F)}"
    from AS(1) have im:"f`g∈H" using assms(4) apply_type by auto
    then have iminv:"GroupInv(H,F)`(f`g)∈H" using assms(2) group0.inverse_in_group unfolding group0_def by auto
    from AS have "h∈G" and inv:"GroupInv(G,P)`g∈G" using A group0.inverse_in_group assms(1) unfolding group0_def by auto
    then have P:"P`⟨h,GroupInv(G,P)`g⟩∈G" using assms(1) group0.group_op_closed unfolding group0_def by auto
    with `g∈G` have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩∈G" using assms(1) group0.group_op_closed unfolding group0_def by auto
    then have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,f`(P`⟨h,GroupInv(G,P)`g⟩)⟩"
      using assms(3) unfolding Homomor_def[OF assms(1,2)] using `g∈G` P by auto
    also have "…=F`⟨f`g,F`(⟨f`h,f`(GroupInv(G,P)`g)⟩)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)]
      using `h∈G` inv by auto
    also have "…=F`⟨f`g,F`(⟨f`h,GroupInv(H,F)`(f`g)⟩)⟩" using image_inv[OF assms `g∈G`] by auto
    ultimately have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,F`(⟨f`h,GroupInv(H,F)`(f`g)⟩)⟩" by auto
    moreover from AS(2) have "f`h=TheNeutralElement(H,F)" using func1_1_L15[OF assms(4)]
      by auto ultimately
    have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,F`(⟨TheNeutralElement(H,F),GroupInv(H,F)`(f`g)⟩)⟩" by auto
    also have "…=F`⟨f`g,GroupInv(H,F)`(f`g)⟩" using assms(2) im group0.group0_2_L2 unfolding group0_def
      using iminv by auto
    also have "…=TheNeutralElement(H,F)" using assms(2) group0.group0_2_L6 im
      unfolding group0_def by auto
    ultimately have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=TheNeutralElement(H,F)" by auto moreover
    from P `g∈G` have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩⟩∈G" using group0.group_op_closed assms(1) unfolding group0_def by auto
    ultimately have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩∈f-``{TheNeutralElement(H,F)}" using func1_1_L15[OF assms(4)]
      by auto
  }
  then have "∀g∈G. {P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩. h∈f-``{TheNeutralElement(H,F)}}⊆f-``{TheNeutralElement(H,F)}"
    by auto
  then show ?thesis using group0.cont_conj_is_normal assms(1) SS unfolding group0_def by auto
qed

text{*The image of a homomorphism is a subgroup.*}

theorem image_sub:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H"
  shows "IsAsubgroup(f``G,F)"
proof-
  have "TheNeutralElement(G,P)∈G" using group0.group0_2_L2 assms(1) unfolding group0_def by auto
  then have "TheNeutralElement(H,F)∈f``G" using func_imagedef[OF assms(4),of "G"] image_neutral[OF assms]
    by force
  then have "f``G≠0" by auto moreover
  {
    fix h1 h2 assume "h1∈f``G""h2∈f``G"
    then obtain g1 g2 where "h1=f`g1" "h2=f`g2" and p:"g1∈G""g2∈G" using func_imagedef[OF assms(4)] by auto
    then have "F`⟨h1,h2⟩=F`⟨f`g1,f`g2⟩" by auto
    also have "…=f`(P`⟨g1,g2⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p by auto
    ultimately have "F`⟨h1,h2⟩=f`(P`⟨g1,g2⟩)" by auto
    moreover have "P`⟨g1,g2⟩∈G" using p group0.group_op_closed assms(1) unfolding group0_def
      by auto ultimately
    have "F`⟨h1,h2⟩∈f``G" using func_imagedef[OF assms(4)] by auto
  }
  then have "f``G {is closed under} F" unfolding IsOpClosed_def by auto
  moreover have "f``G⊆H" using func1_1_L6(2) assms(4) by auto moreover
  {
    fix h assume "h∈f``G"
    then obtain g where "h=f`g" and p:"g∈G" using func_imagedef[OF assms(4)] by auto
    then have "GroupInv(H,F)`h=GroupInv(H,F)`(f`g)" by auto
    then have "GroupInv(H,F)`h=f`(GroupInv(G,P)`g)" using p image_inv[OF assms] by auto
    then have "GroupInv(H,F)`h∈f``G" using p group0.inverse_in_group assms(1) unfolding group0_def
      using func_imagedef[OF assms(4)] by auto
  }
  then have "∀h∈f``G. GroupInv(H,F)`h∈f``G" by auto ultimately
  show ?thesis using group0.group0_3_T3 assms(2) unfolding group0_def by auto
qed

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

theorem isomorphism_first_theorem:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H"
  defines "r ≡ QuotientGroupRel(G,P,f-``{TheNeutralElement(H,F)})" and
  "PP ≡ QuotientGroupOp(G,P,f-``{TheNeutralElement(H,F)})"
  shows "∃ff. Homomor(ff,G//r,PP,f``G,restrict(F,(f``G)×(f``G))) ∧ ff∈bij(G//r,f``G)"
proof-
  let ?ff="{⟨r``{g},f`g⟩. g∈G}"
  {
    fix t assume "t∈{⟨r``{g},f`g⟩. g∈G}"
    then obtain g where "t=⟨r``{g},f`g⟩" "g∈G" by auto
    moreover then have "r``{g}∈G//r" unfolding r_def quotient_def by auto
    moreover from `g∈G` have "f`g∈f``G" using func_imagedef[OF assms(4)] by auto
    ultimately have "t∈(G//r)×f``G" by auto
  }
  then have "?ff∈Pow((G//r)×f``G)" by auto
  moreover have "(G//r)⊆domain(?ff)" unfolding domain_def quotient_def by auto moreover
  {
    fix x y t assume A:"⟨x,y⟩∈?ff" "⟨x,t⟩∈?ff"
    then obtain gy gr where "⟨x, y⟩=⟨r``{gy},f`gy⟩" "⟨x, t⟩=⟨r``{gr},f`gr⟩" and p:"gr∈G""gy∈G" by auto
    then have B:"r``{gy}=r``{gr}""y=f`gy""t=f`gr" by auto
    from B(2,3) have q:"y∈H""t∈H" using apply_type p assms(4) by auto
    have "⟨gy,gr⟩∈r" using eq_equiv_class[OF B(1) _ p(1)] group0.Group_ZF_2_4_L3 kerner_normal_sub[OF assms(1-4)]
      assms(1) unfolding group0_def IsAnormalSubgroup_def r_def by auto
    then have "P`⟨gy,GroupInv(G,P)`gr⟩∈f-``{TheNeutralElement(H,F)}" unfolding r_def QuotientGroupRel_def by auto
    then have eq:"f`(P`⟨gy,GroupInv(G,P)`gr⟩)=TheNeutralElement(H,F)" using func1_1_L15[OF assms(4)] by auto
    from B(2,3) have "F`⟨y,GroupInv(H,F)`t⟩=F`⟨f`gy,GroupInv(H,F)`(f`gr)⟩" by auto
    also have "…=F`⟨f`gy,f`(GroupInv(G,P)`gr)⟩" using image_inv[OF assms(1-4)] p(1) by auto
    also have "…=f`(P`⟨gy,GroupInv(G,P)`gr⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p(2)
      group0.inverse_in_group assms(1) p(1) unfolding group0_def by auto
    ultimately have "F`⟨y,GroupInv(H,F)`t⟩=TheNeutralElement(H,F)" using eq by auto
    then have "y=t" using assms(2) group0.group0_2_L11A q unfolding group0_def by auto
  }
  then have "∀x y. ⟨x,y⟩∈?ff ⟶ (∀y'. ⟨x,y'⟩∈?ff ⟶ y=y')" by auto
  ultimately have ff_fun:"?ff:G//r→f``G" unfolding Pi_def function_def by auto
  {
    fix a1 a2 assume AS:"a1∈G//r""a2∈G//r"
    then obtain g1 g2 where p:"g1∈G""g2∈G" and a:"a1=r``{g1}""a2=r``{g2}" unfolding quotient_def by auto
    have "equiv(G,r)" using group0.Group_ZF_2_4_L3 kerner_normal_sub[OF assms(1-4)]
      assms(1) unfolding group0_def IsAnormalSubgroup_def r_def by auto moreover
    have "Congruent2(r,P)" using Group_ZF_2_4_L5A[OF assms(1) kerner_normal_sub[OF assms(1-4)]]
      unfolding r_def by auto moreover
    have "PP=ProjFun2(G,r,P)" unfolding PP_def QuotientGroupOp_def r_def by auto moreover
    note a p ultimately have "PP`⟨a1,a2⟩=r``{P`⟨g1,g2⟩}" using group0.Group_ZF_2_2_L2 assms(1)
      unfolding group0_def by auto
    then have "⟨PP`⟨a1,a2⟩,f`(P`⟨g1,g2⟩)⟩∈?ff" using group0.group_op_closed[OF _ p] assms(1) unfolding group0_def
      by auto
    then have eq:"?ff`(PP`⟨a1,a2⟩)=f`(P`⟨g1,g2⟩)" using apply_equality ff_fun by auto
    from p a have "⟨a1,f`g1⟩∈?ff""⟨a2,f`g2⟩∈?ff" by auto
    then have "?ff`a1=f`g1""?ff`a2=f`g2" using apply_equality ff_fun by auto
    then have "F`⟨?ff`a1,?ff`a2⟩=F`⟨f`g1,f`g2⟩" by auto
    also have "…=f`(P`⟨g1,g2⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p by auto
    ultimately have "F`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" using eq by auto moreover
    have "?ff`a1∈f``G""?ff`a2∈f``G" using ff_fun apply_type AS by auto ultimately
    have "restrict(F,f``G×f``G)`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" by auto
  }
  then have r:"∀a1∈G//r. ∀a2∈G//r. restrict(F,f``G×f``G)`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" by auto
  have G:"IsAgroup(G//r,PP)" using Group_ZF_2_4_T1[OF assms(1) kerner_normal_sub[OF assms(1-4)]] unfolding r_def PP_def by auto
  have H:"IsAgroup(f``G, restrict(F,f``G×f``G))" using image_sub[OF assms(1-4)] unfolding IsAsubgroup_def .
  have HOM:"Homomor(?ff,G//r,PP,f``G,restrict(F,(f``G)×(f``G)))" using r unfolding Homomor_def[OF G H] by auto
  {
    fix b1 b2 assume AS:"?ff`b1=?ff`b2""b1∈G//r""b2∈G//r"
    have invb2:"GroupInv(G//r,PP)`b2∈G//r" using group0.inverse_in_group[OF _ AS(3)] G unfolding group0_def
      by auto
    with AS(2) have "PP`⟨b1,GroupInv(G//r,PP)`b2⟩∈G//r" using group0.group_op_closed G unfolding group0_def by auto moreover
    then obtain gg where gg:"gg∈G""PP`⟨b1,GroupInv(G//r,PP)`b2⟩=r``{gg}" unfolding quotient_def by auto
    ultimately have E:"?ff`(PP`⟨b1,GroupInv(G//r,PP)`b2⟩)=f`gg" using apply_equality[OF _ ff_fun] by auto
    from invb2 have pp:"?ff`(GroupInv(G//r,PP)`b2)∈f``G" using apply_type ff_fun by auto
    from AS(2,3) have fff:"?ff`b1∈f``G""?ff`b2∈f``G" using apply_type[OF ff_fun] by auto
    from fff(1) pp have EE:"F`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩=restrict(F,f``G×f``G)`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩"
      by auto
    from fff have fff2:"?ff`b1∈H""?ff`b2∈H" using func1_1_L6(2)[OF assms(4)] by auto
    with AS(1) have "TheNeutralElement(H,F)=F`⟨?ff`b1,GroupInv(H,F)`(?ff`b2)⟩" using group0.group0_2_L6(1)
      assms(2) unfolding group0_def by auto
    also have "…=F`⟨?ff`b1,restrict(GroupInv(H,F),f``G)`(?ff`b2)⟩" using restrict fff(2) by auto
    also have "…=F`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩" using image_inv[OF G H HOM ff_fun AS(3)]
      group0.group0_3_T1[OF _ image_sub[OF assms(1-4)]] assms(2) unfolding group0_def by auto
    also have "…=restrict(F,f``G×f``G)`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩" using EE by auto
    also have "…=?ff`(PP`⟨b1,GroupInv(G//r,PP)`b2⟩)" using HOM unfolding Homomor_def[OF G H] using AS(2)
      group0.inverse_in_group[OF _ AS(3)] G unfolding group0_def by auto
    also have "…=f`gg" using E by auto
    ultimately have "f`gg=TheNeutralElement(H,F)" by auto
    then have "gg∈f-``{TheNeutralElement(H,F)}" using func1_1_L15[OF assms(4)] `gg∈G` by auto
    then have "r``{gg}=TheNeutralElement(G//r,PP)" using group0.Group_ZF_2_4_L5E[OF _ kerner_normal_sub[OF assms(1-4)]
      `gg∈G` ] using assms(1) unfolding group0_def r_def PP_def by auto 
    with gg(2) have "PP`⟨b1,GroupInv(G//r,PP)`b2⟩=TheNeutralElement(G//r,PP)" by auto
    then have "b1=b2" using group0.group0_2_L11A[OF _ AS(2,3)] G unfolding group0_def by auto
  }
  then have "?ff∈inj(G//r,f``G)" unfolding inj_def using ff_fun by auto moreover
  {
    fix m assume "m∈f``G"
    then obtain g where "g∈G""m=f`g" using func_imagedef[OF assms(4)] by auto
    then have "⟨r``{g},m⟩∈?ff" by auto
    then have "?ff`(r``{g})=m" using apply_equality ff_fun by auto
    then have "∃A∈G//r. ?ff`A=m" unfolding quotient_def using `g∈G` by auto
  }
  ultimately have "?ff∈bij(G//r,f``G)" unfolding bij_def surj_def using ff_fun by auto
  with HOM show ?thesis by auto
qed

text{*As a last result, the inverse of a bijective homomorphism is an homomorphism.
Meaning that in the previous result, the homomorphism we found is an isomorphism.*}

theorem bij_homomor:
  assumes "f∈bij(G,H)""IsAgroup(G,P)""IsAgroup(H,F)""Homomor(f,G,P,H,F)"
  shows "Homomor(converse(f),H,F,G,P)"
proof-
  {
    fix h1 h2 assume A:"h1∈H" "h2∈H"
    from A(1) obtain g1 where g1:"g1∈G" "f`g1=h1" using assms(1) unfolding bij_def surj_def by auto moreover
    from A(2) obtain g2 where g2:"g2∈G" "f`g2=h2" using assms(1) unfolding bij_def surj_def by auto ultimately
    have "F`⟨f`g1,f`g2⟩=F`⟨h1,h2⟩" by auto
    then have "f`(P`⟨g1,g2⟩)=F`⟨h1,h2⟩" using assms(2,3,4) homomor_eq g1(1) g2(1) by auto
    then have "converse(f)`(f`(P`⟨g1,g2⟩))=converse(f)`(F`⟨h1,h2⟩)" by auto
    then have "P`⟨g1,g2⟩=converse(f)`(F`⟨h1,h2⟩)" using left_inverse assms(1) group0.group_op_closed
      assms(2) g1(1) g2(1) unfolding group0_def bij_def by auto moreover
    from g1(2) have "converse(f)`(f`g1)=converse(f)`h1" by auto
    then have "g1=converse(f)`h1" using left_inverse assms(1) unfolding bij_def using g1(1) by auto moreover
    from g2(2) have "converse(f)`(f`g2)=converse(f)`h2" by auto
    then have "g2=converse(f)`h2" using left_inverse assms(1) unfolding bij_def using g2(1) by auto ultimately
    have "P`⟨converse(f)`h1,converse(f)`h2⟩=converse(f)`(F`⟨h1,h2⟩)" by auto
  }
  then show ?thesis using assms(2,3) Homomor_def by auto
qed

end