Theory TopologicalGroup_ZF_3

theory TopologicalGroup_ZF_3
imports Topology_ZF_10 TopologicalGroup_ZF_2 TopologicalGroup_ZF_1 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 ‹Topological groups 3›

theory TopologicalGroup_ZF_3 imports Topology_ZF_10 TopologicalGroup_ZF_2 TopologicalGroup_ZF_1
  Group_ZF_4

begin

text{*This theory deals with topological properties of subgroups, quotient groups
and relations between group theorical properties and topological properties.*}

subsection{*Subgroups topologies*}

text{*The closure of a subgroup is a subgroup.*}

theorem (in topgroup) closure_subgroup:
  assumes "IsAsubgroup(H,f)"
  shows "IsAsubgroup(cl(H),f)"
proof-
  have two:"two_top_spaces0(ProductTopology(T,T),T,f)" unfolding two_top_spaces0_def using
    topSpaceAssum Top_1_4_T1(1,3) topgroup_f_binop by auto
  from fcon have cont:"IsContinuous(ProductTopology(T,T),T,f)" by auto
  then have closed:"∀D. D{is closed in}T ⟶ f-``D{is closed in}τ" using two_top_spaces0.TopZF_2_1_L1
    two by auto
  then have closure:"∀A∈Pow(⋃τ). f``(Closure(A,τ))⊆cl(f``A)" using two_top_spaces0.Top_ZF_2_1_L2
    two by force
  have sub1:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup assms by force
  then have sub:"(H)×(H)⊆⋃τ" using prod_top_on_G(2) by auto
  from sub1 have clHG:"cl(H)⊆G" using Top_3_L11(1) by auto
  then have clHsub1:"cl(H)×cl(H)⊆G×G" by auto
  have "Closure(H×H,ProductTopology(T,T))=cl(H)×cl(H)" using cl_product
    topSpaceAssum group0.group0_3_L2 group0_valid_in_tgroup assms by auto
  then have "f``(Closure(H×H,ProductTopology(T,T)))=f``(cl(H)×cl(H))" by auto
  with closure sub have clcl:"f``(cl(H)×cl(H))⊆cl(f``(H×H))" by force
  from assms have fun:"restrict(f,H×H):H×H→H" unfolding IsAsubgroup_def using
    group0.group_oper_assocA unfolding group0_def by auto
  then have "restrict(f,H×H)``(H×H)=f``(H×H)" using restrict_image by auto
  moreover from fun have "restrict(f,H×H)``(H×H)⊆H" using func1_1_L6(2) by blast
  ultimately have "f``(H×H)⊆H" by auto
  with sub1 have "f``(H×H)⊆H""f``(H×H)⊆G""H⊆G" by auto
  then have "cl(f``(H×H))⊆cl(H)" using top_closure_mono by auto
  with clcl have img:"f``(cl(H)×cl(H))⊆cl(H)" by auto
  {
    fix x y assume "x∈cl(H)""y∈cl(H)"
    then have "⟨x,y⟩∈cl(H)×cl(H)" by auto moreover
    have "f``(cl(H)×cl(H))={f`t. t∈cl(H)×cl(H)}" using func_imagedef topgroup_f_binop 
      clHsub1 by auto ultimately
    have "f`⟨x,y⟩∈f``(cl(H)×cl(H))" by auto
    with img have "f`⟨x,y⟩∈cl(H)" by auto
  }
  then have A1:"cl(H){is closed under} f" unfolding IsOpClosed_def by auto
  have two:"two_top_spaces0(T,T,GroupInv(G,f))" unfolding two_top_spaces0_def using
    topSpaceAssum Ggroup group0_2_T2 by auto
  from inv_cont have cont:"IsContinuous(T,T,GroupInv(G,f))" by auto
  then have closed:"∀D. D{is closed in}T ⟶ GroupInv(G,f)-``D{is closed in}T" using two_top_spaces0.TopZF_2_1_L1
    two by auto
  then have closure:"∀A∈Pow(⋃T). GroupInv(G,f)``(cl(A))⊆cl(GroupInv(G,f)``A)" using two_top_spaces0.Top_ZF_2_1_L2
    two by force
  with sub1 have Inv:"GroupInv(G,f)``(cl(H))⊆cl(GroupInv(G,f)``H)" by auto moreover
  have "GroupInv(H,restrict(f,H×H)):H→H" using assms unfolding IsAsubgroup_def using group0_2_T2 by auto then
  have "GroupInv(H,restrict(f,H×H))``H⊆H" using func1_1_L6(2) by auto
  then have "restrict(GroupInv(G,f),H)``H⊆H" using group0.group0_3_T1 assms group0_valid_in_tgroup by auto
  then have sss:"GroupInv(G,f)``H⊆H" using restrict_image by auto
  then have "H⊆G" "GroupInv(G,f)``H⊆G" using sub1 by auto
  with sub1 sss have "cl(GroupInv(G,f)``H)⊆cl(H)" using top_closure_mono by auto ultimately
  have img:"GroupInv(G,f)``(cl(H))⊆cl(H)" by auto
  {
    fix x assume "x∈cl(H)" moreover
    have "GroupInv(G,f)``(cl(H))={GroupInv(G,f)`t. t∈cl(H)}" using func_imagedef Ggroup group0_2_T2
      clHG by force ultimately
    have "GroupInv(G,f)`x∈GroupInv(G,f)``(cl(H))" by auto
    with img have "GroupInv(G,f)`x∈cl(H)" by auto
  }
  then have A2:"∀x∈cl(H). GroupInv(G,f)`x∈cl(H)" by auto
  from assms have "H≠0" using group0.group0_3_L5 group0_valid_in_tgroup by auto moreover
  have "H⊆cl(H)" using cl_contains_set sub1 by auto ultimately
  have "cl(H)≠0" by auto
  with clHG A2 A1 show ?thesis using group0.group0_3_T3 group0_valid_in_tgroup by auto
qed

text{*The closure of a normal subgroup is normal.*}

theorem (in topgroup) normal_subg:
  assumes "IsAnormalSubgroup(G,f,H)"
  shows "IsAnormalSubgroup(G,f,cl(H))"
proof-
  have A:"IsAsubgroup(cl(H),f)" using closure_subgroup assms unfolding IsAnormalSubgroup_def by auto
  have sub1:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup assms unfolding IsAnormalSubgroup_def by auto
  then have sub2:"cl(H)⊆G" using Top_3_L11(1) by auto
  {
    fix g assume g:"g∈G"
    then have cl1:"cl(g\<ltr>H)=g\<ltr>cl(H)" using trans_closure sub1 by auto
    have ss:"g\<ltr>cl(H)⊆G" unfolding ltrans_def LeftTranslation_def by auto
    have "g\<ltr>H⊆G" unfolding ltrans_def LeftTranslation_def by auto
    moreover from g have "(\<rm>g)∈G" using neg_in_tgroup by auto
    ultimately have cl2:"cl((g\<ltr>H)\<rtr>(\<rm>g))=cl(g\<ltr>H)\<rtr>(\<rm>g)" using trans_closure2
      by auto
    with cl1 have clcon:"cl((g\<ltr>H)\<rtr>(\<rm>g))=(g\<ltr>(cl(H)))\<rtr>(\<rm>g)" by auto
    {
      fix r assume "r∈(g\<ltr>H)\<rtr>(\<rm>g)"
      then obtain q where q:"q∈g\<ltr>H" "r=q\<ra>(\<rm>g)" unfolding rtrans_def RightTranslation_def
        by force
      from q(1) obtain h where "h∈H" "q=g\<ra>h" unfolding ltrans_def LeftTranslation_def by auto
      with q(2) have "r=(g\<ra>h)\<ra>(\<rm>g)" by auto
      with `h∈H` `g∈G` `(\<rm>g)∈G` have "r∈H" using assms unfolding IsAnormalSubgroup_def
        grinv_def grop_def by auto
    }
    then have "(g\<ltr>H)\<rtr>(\<rm>g)⊆H" by auto
    moreover then have "(g\<ltr>H)\<rtr>(\<rm>g)⊆G""H⊆G" using sub1 by auto ultimately
    have "cl((g\<ltr>H)\<rtr>(\<rm>g))⊆cl(H)" using top_closure_mono by auto
    with clcon have "(g\<ltr>(cl(H)))\<rtr>(\<rm>g)⊆cl(H)" by auto moreover
    {
      fix b assume "b∈{g\<ra>(d\<rs>g). d∈cl(H)}"
      then obtain d where d:"d∈cl(H)" "b=g\<ra>(d\<rs>g)" by auto moreover
      then have "d∈G" using sub2 by auto 
      then have "g\<ra>d∈G" using group0.group_op_closed[OF group0_valid_in_tgroup `g∈G`] by auto
      from d(2) have b:"b=(g\<ra>d)\<rs>g" using group0.group_oper_assoc[OF group0_valid_in_tgroup `g∈G` `d∈G``(\<rm>g)∈G`] 
        unfolding grsub_def grop_def grinv_def by blast
      have "(g\<ra>d)=LeftTranslation(G,f,g)`d" using group0.group0_5_L2(2)[OF group0_valid_in_tgroup]
        `g∈G``d∈G` by auto
      with `d∈cl(H)` have "g\<ra>d∈g\<ltr>cl(H)" unfolding ltrans_def using func_imagedef[OF group0.group0_5_L1(2)[
        OF group0_valid_in_tgroup `g∈G`] sub2] by auto
      moreover from b have "b=RightTranslation(G,f,\<rm>g)`(g\<ra>d)" using group0.group0_5_L2(1)[OF group0_valid_in_tgroup]
        `(\<rm>g)∈G``g\<ra>d∈G` by auto
      ultimately have "b∈(g\<ltr>cl(H))\<rtr>(\<rm>g)" unfolding rtrans_def using func_imagedef[OF group0.group0_5_L1(1)[
        OF group0_valid_in_tgroup `(\<rm>g)∈G`] ss] by force
    }
    ultimately have "{g\<ra>(d\<rs>g). d∈cl(H)}⊆cl(H)" by force
  }
  then show ?thesis using A group0.cont_conj_is_normal[OF group0_valid_in_tgroup, of "cl(H)"]
    unfolding grsub_def grinv_def grop_def by auto
qed

text{*Every open subgroup is also closed.*}

theorem (in topgroup) open_subgroup_closed:
  assumes "IsAsubgroup(H,f)" "H∈T"
  shows "H{is closed in}T"
proof-
  from assms(1) have sub:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup by force
  {
    fix t assume "t∈G-H"
    then have tnH:"t∉H" and tG:"t∈G" by auto
    from assms(1) have sub:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup by force
    from assms(1) have nSubG:"𝟬∈H" using group0.group0_3_L5 group0_valid_in_tgroup by auto
    from assms(2) tG have op:"t\<ltr>H∈T" using open_tr_open(1) by auto
    from nSubG sub tG have tp:"t∈t\<ltr>H" using group0_valid_in_tgroup group0.neut_trans_elem
      by auto
    {
      fix x assume "x∈(t\<ltr>H)∩H"
      then obtain u where "x=t\<ra>u" "u∈H" "x∈H" unfolding ltrans_def LeftTranslation_def by auto
      then have "u∈G""x∈G""t∈G" using sub tG by auto
      with `x=t\<ra>u` have "x\<ra>(\<rm>u)=t" using group0.group0_2_L18(1) group0_valid_in_tgroup
        unfolding grop_def grinv_def by auto
      from `u∈H` have "(\<rm>u)∈H" unfolding grinv_def using assms(1) group0.group0_3_T3A group0_valid_in_tgroup
        by auto
      with `x∈H` have "x\<ra>(\<rm>u)∈H" unfolding grop_def using assms(1) group0.group0_3_L6 group0_valid_in_tgroup
        by auto
      with `x\<ra>(\<rm>u)=t` have "False" using tnH by auto
    }
    then have "(t\<ltr>H)∩H=0" by auto moreover
    have "t\<ltr>H⊆G" unfolding ltrans_def LeftTranslation_def by auto ultimately
    have "(t\<ltr>H)⊆G-H" by auto
    with tp op have "∃V∈T. t∈V ∧ V⊆G-H" unfolding Bex_def by auto
  }
  then have "∀t∈G-H. ∃V∈T. t∈V ∧ V⊆G-H" by auto
  then have "G-H∈T" using open_neigh_open by auto
  then show ?thesis unfolding IsClosed_def using sub by auto
qed

text{*Any subgroup with non-empty interior is open.*}

theorem (in topgroup) clopen_or_emptyInt:
  assumes "IsAsubgroup(H,f)" "int(H)≠0"
  shows "H∈T"
proof-
  from assms(1) have sub:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup by force
  {
    fix h assume "h∈H"
    have intsub:"int(H)⊆H" using Top_2_L1 by auto
    from assms(2) obtain u where "u∈int(H)" by auto
    with intsub have "u∈H" by auto
    then have "(\<rm>u)∈H" unfolding grinv_def using assms(1) group0.group0_3_T3A group0_valid_in_tgroup
      by auto
    with `h∈H` have "h\<rs>u∈H" unfolding grop_def using assms(1) group0.group0_3_L6 group0_valid_in_tgroup
      by auto
    {
      fix t assume "t∈(h\<rs>u)\<ltr>(int(H))"
      then obtain r where "r∈int(H)""t=(h\<rs>u)\<ra>r" unfolding grsub_def grinv_def grop_def
        ltrans_def LeftTranslation_def by auto
      then have "r∈H" using intsub by auto
      with `h\<rs>u∈H` have "(h\<rs>u)\<ra>r∈H" unfolding grop_def using assms(1) group0.group0_3_L6 group0_valid_in_tgroup
        by auto
      with `t=(h\<rs>u)\<ra>r` have "t∈H" by auto
    }
    then have ss:"(h\<rs>u)\<ltr>(int(H))⊆H" by auto
    have op:"(h\<rs>u)\<ltr>(int(H))∈T" using open_tr_open(1) `h\<rs>u∈H` Top_2_L2 sub by blast
    from `h\<rs>u∈H``u∈H``h∈H` sub have "(h\<rs>u)∈G" "u∈G""h∈G" by auto
    have "int(H)⊆G" using sub intsub by auto moreover
    have "LeftTranslation(G,f,(h\<rs>u))∈G→G" using group0.group0_5_L1(2) group0_valid_in_tgroup `(h\<rs>u)∈G`
      by auto ultimately
    have "LeftTranslation(G,f,(h\<rs>u))``(int(H))={LeftTranslation(G,f,(h\<rs>u))`r. r∈int(H)}" 
      using func_imagedef by auto moreover
    from `(h\<rs>u)∈G` `u∈G` have "LeftTranslation(G,f,(h\<rs>u))`u=(h\<rs>u)\<ra>u" using group0.group0_5_L2(2) group0_valid_in_tgroup
      by auto
    with `u∈int(H)` have "(h\<rs>u)\<ra>u∈{LeftTranslation(G,f,(h\<rs>u))`r. r∈int(H)}" by force ultimately
    have "(h\<rs>u)\<ra>u∈(h\<rs>u)\<ltr>(int(H))" unfolding ltrans_def by auto moreover
    have "(h\<rs>u)\<ra>u=h" using group0.inv_cancel_two(1) group0_valid_in_tgroup
      `u∈G``h∈G` by auto ultimately
    have "h∈(h\<rs>u)\<ltr>(int(H))" by auto
    with op ss have "∃V∈T. h∈V∧ V⊆H" unfolding Bex_def by auto
  }
  then show ?thesis using open_neigh_open by auto
qed

text{*In conclusion, a subgroup is either open or has empty interior.*}

corollary(in topgroup) emptyInterior_xor_op:
  assumes "IsAsubgroup(H,f)"
  shows "(int(H)=0) Xor (H∈T)"
  unfolding Xor_def using clopen_or_emptyInt assms Top_2_L3 
  group0.group0_3_L5 group0_valid_in_tgroup by force

text{*Then no connected topological groups has proper subgroups with non-empty interior.*}

corollary(in topgroup) connected_emptyInterior:
  assumes "IsAsubgroup(H,f)" "T{is connected}"
  shows "(int(H)=0) Xor (H=G)"
proof-
  have "(int(H)=0) Xor (H∈T)" using emptyInterior_xor_op assms(1) by auto moreover
  {
    assume "H∈T" moreover
    then have "H{is closed in}T" using open_subgroup_closed assms(1) by auto ultimately
    have "H=0∨H=G" using assms(2) unfolding IsConnected_def by auto
    then have "H=G" using group0.group0_3_L5 group0_valid_in_tgroup assms(1) by auto
  } moreover
  have "G∈T" using topSpaceAssum unfolding IsATopology_def G_def by auto
  ultimately show ?thesis unfolding Xor_def by auto
qed

text{*Every locally-compact subgroup of a $T_0$ group is closed.*}

theorem (in topgroup) loc_compact_T0_closed:
  assumes "IsAsubgroup(H,f)" "(T{restricted to}H){is locally-compact}" "T{is T0}"
  shows "H{is closed in}T"
proof-
  from assms(1) have clsub:"IsAsubgroup(cl(H),f)" using closure_subgroup by auto
  then have subcl:"cl(H)⊆G" using group0.group0_3_L2 group0_valid_in_tgroup by force
  from assms(1) have sub:"H⊆G" using group0.group0_3_L2 group0_valid_in_tgroup by force
  from assms(3) have "T{is T2}" using T1_imp_T2 neu_closed_imp_T1 T0_imp_neu_closed by auto
  then have "(T{restricted to}H){is T2}" using T2_here sub by auto
  have tot:"⋃(T{restricted to}H)=H" using sub unfolding RestrictedTo_def by auto
  with assms(2) have "∀x∈H. ∃A∈Pow(H). A {is compact in} (T{restricted to}H) ∧ x ∈ Interior(A, (T{restricted to}H))" using 
    topology0.locally_compact_exist_compact_neig[of "T{restricted to}H"] Top_1_L4 unfolding topology0_def
    by auto
  then obtain K where K:"K⊆H" "K{is compact in} (T{restricted to}H)""𝟬∈Interior(K,(T{restricted to}H))"
    using group0.group0_3_L5 group0_valid_in_tgroup assms(1) unfolding gzero_def by force
  from K(1,2) have "K{is compact in} T" using compact_subspace_imp_compact by auto
  with `T{is T2}` have Kcl:"K{is closed in}T" using in_t2_compact_is_cl by auto
  have "Interior(K,(T{restricted to}H))∈(T{restricted to}H)" using topology0.Top_2_L2 unfolding topology0_def
    using Top_1_L4 by auto
  then obtain U where U:"U∈T""Interior(K,(T{restricted to}H))=H∩U" unfolding RestrictedTo_def by auto
  then have "H∩U⊆K" using topology0.Top_2_L1[of "T{restricted to}H"] unfolding topology0_def using Top_1_L4 by force
  moreover have U2:"U⊆U∪K" by auto
  have ksub:"K⊆H" using tot K(2) unfolding IsCompact_def by auto
  ultimately have int:"H∩(U∪K)=K" by auto
  from U(2) K(3) have "𝟬∈U" by auto
  with U(1) U2 have "𝟬∈int(U ∪ K)" using Top_2_L6 by auto
  then have "U∪K∈𝒩0" unfolding zerohoods_def using U(1) ksub sub by auto
  then obtain V where V:"V⊆U∪K" "V∈𝒩0" "V\<sad>V⊆U∪K""(\<sm> V) = V" using exists_procls_zerohood[of "U∪K"]
    by auto
  {
    fix h assume AS:"h∈cl(H)"
    with clsub have "(\<rm>h)∈cl(H)" using group0.group0_3_T3A group0_valid_in_tgroup by auto moreover
    then have "(\<rm>h)∈G" using subcl by auto
    with V(2) have "(\<rm>h)∈int((\<rm>h)\<ltr>V)" using elem_in_int_trans by auto ultimately
    have "(\<rm>h)∈(cl(H))∩(int((\<rm>h)\<ltr>V))" by auto moreover
    have "int((\<rm>h)\<ltr>V)∈T" using Top_2_L2 by auto moreover
    note sub ultimately
    have "H∩(int((\<rm>h)\<ltr>V))≠0" using cl_inter_neigh by auto moreover
    from `(\<rm>h)∈G` V(2) have "int((\<rm>h)\<ltr>V)=(\<rm>h)\<ltr>int(V)" unfolding zerohoods_def using trans_interior by force
    ultimately have "H∩((\<rm>h)\<ltr>int(V))≠0" by auto
    then obtain y where y:"y∈H" "y∈(\<rm>h)\<ltr>int(V)" by blast
    then obtain v where v:"v∈int(V)" "y=(\<rm>h)\<ra>v" unfolding ltrans_def LeftTranslation_def by auto
    with `(\<rm>h)∈G` V(2) y(1) sub have "v∈G""(\<rm>h)∈G""y∈G" using Top_2_L1[of "V"] unfolding zerohoods_def by auto
    with v(2) have "(\<rm>(\<rm>h))\<ra>y=v" using group0.group0_2_L18(2) group0_valid_in_tgroup
      unfolding grop_def grinv_def by auto moreover
    have "h∈G" using AS subcl by auto
    then have "(\<rm>(\<rm>h))=h" using group0.group_inv_of_inv group0_valid_in_tgroup by auto ultimately
    have "h\<ra>y=v" by auto
    with v(1) have hyV:"h\<ra>y∈int(V)" by auto
    have "y∈cl(H)" using y(1) cl_contains_set sub by auto
    with AS have hycl:"h\<ra> y∈cl(H)" using clsub group0.group0_3_L6 group0_valid_in_tgroup by auto
    {
      fix W assume W:"W∈T""h\<ra>y∈W"
      with hyV have "h\<ra>y∈int(V)∩W" by auto moreover
      from W(1) have "int(V)∩W∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover
      note hycl sub
      ultimately have "(int(V)∩W)∩H≠0" using cl_inter_neigh[of "H""int(V)∩W""h\<ra>y"] by auto
      then have "V∩W∩H≠0" using Top_2_L1 by auto
      with V(1) have "(U∪K)∩W∩H≠0" by auto
      then have "(H∩(U∪K))∩W≠0" by auto
      with int have "K∩W≠0" by auto
    }
    then have "∀W∈T. h\<ra>y∈W ⟶ K∩W≠0" by auto moreover
    have "K⊆G" "h\<ra>y∈G" using ksub sub hycl subcl by auto ultimately
    have "h\<ra>y∈cl(K)" using inter_neigh_cl[of "K""h\<ra>y"] unfolding G_def by force
    then have "h\<ra>y∈K" using Kcl Top_3_L8 `K⊆G` by auto
    with ksub have "h\<ra>y∈H" by auto
    moreover from y(1) have "(\<rm>y)∈H" using group0.group0_3_T3A assms(1) group0_valid_in_tgroup
      by auto
    ultimately have "(h\<ra>y)\<rs>y∈H" unfolding grsub_def using group0.group0_3_L6 group0_valid_in_tgroup
      assms(1) by auto
    moreover 
    have "(\<rm>y)∈G" using `(\<rm>y)∈H` sub by auto
    then have "h\<ra>(y\<rs>y)=(h\<ra>y)\<rs>y" using `y∈G``h∈G` group0.group_oper_assoc
      group0_valid_in_tgroup unfolding grsub_def by auto
    then have "h\<ra>𝟬=(h\<ra>y)\<rs>y" using group0.group0_2_L6 group0_valid_in_tgroup `y∈G`
      unfolding grsub_def grinv_def grop_def gzero_def by auto
    then have "h=(h\<ra>y)\<rs>y" using group0.group0_2_L2 group0_valid_in_tgroup
      `h∈G` unfolding gzero_def by auto
    ultimately have "h∈H" by auto
  }
  then have "cl(H)⊆H" by auto
  then have "H=cl(H)" using cl_contains_set sub by auto
  then show ?thesis using Top_3_L8 sub by auto
qed

text{*We can always consider a factor group which is $T_2$.*}

theorem(in topgroup) factor_haus:
  shows "(T{quotient by}QuotientGroupRel(G,f,cl({𝟬}))){is T2}"
proof-
  let ?r="QuotientGroupRel(G,f,cl({𝟬}))"
  let ?f="QuotientGroupOp(G,f,cl({𝟬}))"
  let ?i="GroupInv(G//?r,?f)"
  have "IsAnormalSubgroup(G,f,{𝟬})" using group0.trivial_normal_subgroup Ggroup unfolding group0_def
    by auto
  then have normal:"IsAnormalSubgroup(G,f,cl({𝟬}))" using normal_subg by auto
  then have eq:"equiv(⋃T,?r)" using group0.Group_ZF_2_4_L3[OF group0_valid_in_tgroup]
    unfolding IsAnormalSubgroup_def by auto
  then have tot:"⋃(T{quotient by}?r)=G//?r" using total_quo_equi by auto
  have neu:"?r``{𝟬}=TheNeutralElement(G//?r,?f)" using Group_ZF_2_4_L5B[OF Ggroup normal] by auto
  then have "?r``{𝟬}∈G//?r" using group0.group0_2_L2 Group_ZF_2_4_T1[OF Ggroup normal] unfolding group0_def by auto
  then have sub1:"{?r``{𝟬}}⊆G//?r" by auto
  then have sub:"{?r``{𝟬}}⊆⋃(T{quotient by}?r)" using tot by auto
  have zG:"𝟬∈⋃T" using group0.group0_2_L2[OF group0_valid_in_tgroup] by auto
  from zG have cla:"?r``{𝟬}∈G//?r" unfolding quotient_def by auto
  let ?x="G//?r-{?r``{𝟬}}"
  {
    fix s assume A:"s∈⋃(G//?r-{?r``{𝟬}})"
    then obtain U where "s∈U" "U∈G//?r-{?r``{𝟬}}" by auto
    then have "U∈G//?r" "U≠?r``{𝟬}" "s∈U" by auto
    then have "U∈G//?r" "s∈U" "s∉?r``{𝟬}" using cla quotient_disj[OF eq] by auto
    then have "s∈⋃(G//?r)-?r``{𝟬}" by auto
  }
  moreover
  {
    fix s assume A:"s∈⋃(G//?r)-?r``{𝟬}"
    then obtain U where "s∈U" "U∈G//?r" "s∉?r``{𝟬}" by auto
    then have "s∈U" "U∈G//?r-{?r``{𝟬}}" by auto
    then have "s∈⋃(G//?r-{?r``{𝟬}})" by auto
  }
  ultimately have "⋃(G//?r-{?r``{𝟬}})=⋃(G//?r)-?r``{𝟬}" by auto
  then have A:"⋃(G//?r-{?r``{𝟬}})=G-?r``{𝟬}" using Union_quotient eq by auto
  {
    fix s assume A:"s∈?r``{𝟬}"
    then have "⟨𝟬,s⟩∈?r" by auto
    then have "⟨s,𝟬⟩∈?r" using eq unfolding equiv_def sym_def by auto
    then have "s∈cl({𝟬})" using group0.Group_ZF_2_4_L5C[OF group0_valid_in_tgroup] unfolding QuotientGroupRel_def by auto
  }
  moreover
  {
    fix s assume A:"s∈cl({𝟬})"
    then have "s∈G" using Top_3_L11(1) zG by auto
    then have "⟨s,𝟬⟩∈?r" using group0.Group_ZF_2_4_L5C[OF group0_valid_in_tgroup] A by auto
    then have "⟨𝟬,s⟩∈?r" using eq unfolding equiv_def sym_def by auto
    then have "s∈?r``{𝟬}" by auto
  }
  ultimately have "?r``{𝟬}=cl({𝟬})" by blast
  with A have "⋃(G//?r-{?r``{𝟬}})=G-cl({𝟬})" by auto
  moreover have "cl({𝟬}){is closed in}T" using cl_is_closed zG by auto
  ultimately have "⋃(G//?r-{?r``{𝟬}})∈T" unfolding IsClosed_def by auto
  then have "(G//?r-{?r``{𝟬}})∈{quotient by}?r" using quotient_equiv_rel eq by auto
  then have "(⋃(T{quotient by}?r)-{?r``{𝟬}})∈{quotient by}?r" using total_quo_equi[OF eq] by auto
  moreover from sub1 have "{?r``{𝟬}}⊆(⋃(T{quotient by}?r))" using total_quo_equi[OF eq] by auto
  ultimately have "{?r``{𝟬}}{is closed in}(T{quotient by}?r)" unfolding IsClosed_def by auto
  then have "{TheNeutralElement(G//?r,?f)}{is closed in}(T{quotient by}?r)" using neu by auto
  then have "(T{quotient by}?r){is T1}" using topgroup.neu_closed_imp_T1[OF topGroupLocale[OF quotient_top_group[OF normal]]]
    total_quo_equi[OF eq] by auto
  then show ?thesis using topgroup.T1_imp_T2[OF topGroupLocale[OF quotient_top_group[OF normal]]] by auto
qed 
      

end