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