Theory TopologicalGroup_ZF_3
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_fun 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 P:"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 P 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 P:"(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 P 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 T⇩0}"
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 T⇩2}" using T1_imp_T2 neu_closed_imp_T1 T0_imp_neu_closed by auto
then have "(T{restricted to}H){is T⇩2}" 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 T⇩2}› 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_ltrans 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 ltrans_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 T⇩2}"
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 T⇩1}" 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