Theory TopologicalGroup_ZF_1

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

theory TopologicalGroup_ZF_1 imports TopologicalGroup_ZF Topology_ZF_properties_2
begin

text‹This theory deals with some topological properties of topological groups.›

subsection‹Separation properties of topological groups›
text‹The topological groups have very specific properties. For instance, $G$ is ‹T⇩0›
iff it is ‹T⇩3›.›

theorem(in topgroup) cl_point:
  assumes "x∈G"
  shows "cl({x}) = (⋂H∈𝒩⇩0. x\<ltr>H)"
proof-
  {
    have c:"cl({x}) = (⋂H∈𝒩⇩0. {x}\<sad>H)" using cl_topgroup assms by auto
    {
      fix H
      assume "H∈𝒩⇩0"
      then have "{x}\<sad>H=x\<ltr> H" using interval_add(3) assms
        by auto
      with ‹H∈𝒩⇩0› have "{x}\<sad>H∈{x\<ltr>H. H∈𝒩⇩0}" by auto
    }
    then have "{{x}\<sad>H. H∈𝒩⇩0}⊆{x\<ltr>H. H∈𝒩⇩0}" by auto
    moreover
    {
      fix H
      assume "H∈𝒩⇩0"
      then have "{x}\<sad>H=x\<ltr> H" using interval_add(3) assms
        by auto
      with ‹H∈𝒩⇩0› have "x\<ltr> H∈{{x}\<sad>H. H∈𝒩⇩0}" by auto
    }
    then have "{x\<ltr>H. H∈𝒩⇩0}⊆{{x}\<sad>H. H∈𝒩⇩0}" by auto
    ultimately have "{{x}\<sad>H. H∈𝒩⇩0}={x\<ltr>H. H∈𝒩⇩0}" by auto
    then have "(⋂H∈𝒩⇩0. {x}\<sad>H) = (⋂H∈𝒩⇩0. x\<ltr>H)" by auto
    with c show "cl({x})=(⋂H∈𝒩⇩0. x\<ltr>H)" by auto
  }
qed

text‹We prove the equivalence between $T_0$ and $T_1$ first.›

theorem (in topgroup) neu_closed_imp_T1:
  assumes "{𝟬}{is closed in}T"
  shows "T{is T⇩1}"
proof-
  {
    fix x z assume xG:"x∈G" and zG:"z∈G" and dis:"x≠z"
    then have clx:"cl({x})=(⋂H∈𝒩⇩0. x\<ltr>H)" using cl_point by auto
    {
      fix y
      assume "y∈cl({x})"
      with clx have "y∈(⋂H∈𝒩⇩0. x\<ltr>H)" by auto
      then have t:"∀H∈𝒩⇩0. y∈x\<ltr>H" by auto
      from ‹y∈cl({x})› xG have yG:"y∈G" using Top_3_L11(1) G_def by auto
      {
        fix H
        assume HNeig:"H∈𝒩⇩0"
        with t have "y∈x\<ltr>H" by auto
        then obtain n where "y=x\<ra>n" and "n∈H" unfolding ltrans_def grop_def LeftTranslation_def by auto
        with HNeig have nG:"n∈G" unfolding zerohoods_def by auto
        from ‹y=x\<ra>n› and ‹n∈H› have "(\<rm>x)\<ra>y∈H" using group0.group0_2_L18(2) group0_valid_in_tgroup xG nG yG unfolding grinv_def grop_def
          by auto
      }
      then have el:"(\<rm>x)\<ra>y∈(⋂𝒩⇩0)" using zneigh_not_empty by auto
      have "cl({𝟬})=(⋂H∈𝒩⇩0. 𝟬\<ltr>H)" using cl_point zero_in_tgroup by auto
      moreover
      {
        fix H  assume "H∈𝒩⇩0"
        then have "H⊆G" unfolding zerohoods_def by auto
        then have "𝟬\<ltr>H=H" using image_id_same  group0.trans_neutral(2) group0_valid_in_tgroup unfolding gzero_def ltrans_def
          by auto
        with ‹H∈𝒩⇩0› have "𝟬\<ltr>H∈𝒩⇩0" "H∈{𝟬\<ltr>H. H∈𝒩⇩0}" by auto
      }
      then have "{𝟬\<ltr>H. H∈𝒩⇩0}=𝒩⇩0" by blast
      ultimately have "cl({𝟬})=(⋂𝒩⇩0)" by auto
      with el have "(\<rm>x)\<ra>y∈cl({𝟬})" by auto
      then have "(\<rm>x)\<ra>y∈{𝟬}" using assms Top_3_L8 G_def zero_in_tgroup by auto
      then have "(\<rm>x)\<ra>y=𝟬" by auto
      then have "y=\<rm>(\<rm>x)" using group0.group0_2_L9(2) group0_valid_in_tgroup neg_in_tgroup xG yG unfolding grop_def grinv_def by auto
      then have "y=x" using group0.group_inv_of_inv group0_valid_in_tgroup xG unfolding grinv_def by auto
    }
    then have "cl({x})⊆{x}" by auto
    then have "cl({x})={x}" using xG cl_contains_set G_def by blast
    then have "{x}{is closed in}T" using Top_3_L8 xG G_def by auto
    then have "(⋃T)-{x}∈T" using IsClosed_def by auto moreover
    from dis zG G_def have "z∈((⋃T)-{x}) ∧ x∉((⋃T)-{x})" by auto
    ultimately have "∃V∈T. z∈V∧x∉V" by(safe,auto)
  }
  then show "T{is T⇩1}" using isT1_def by auto
qed

theorem (in topgroup) T0_imp_neu_closed:
  assumes "T{is T⇩0}"
  shows "{𝟬}{is closed in}T"
proof-
  {
    fix x assume "x∈cl({𝟬})" and "x≠𝟬"
    have "cl({𝟬})=(⋂H∈𝒩⇩0. 𝟬\<ltr>H)" using cl_point zero_in_tgroup by auto
    moreover
    {
      fix H  assume "H∈𝒩⇩0"
      then have "H⊆G" unfolding zerohoods_def by auto
      then have "𝟬\<ltr>H=H" using image_id_same  group0.trans_neutral(2) group0_valid_in_tgroup unfolding gzero_def ltrans_def
        by auto
      with ‹H∈𝒩⇩0› have "𝟬\<ltr>H∈𝒩⇩0" "H∈{𝟬\<ltr>H. H∈𝒩⇩0}" by auto
    }
    then have "{𝟬\<ltr>H. H∈𝒩⇩0}=𝒩⇩0" by blast
    ultimately have "cl({𝟬})=(⋂𝒩⇩0)" by auto
    from ‹x≠𝟬› and ‹x∈cl({𝟬})› obtain U where "U∈T" and "(x∉U∧𝟬∈U)∨(𝟬∉U∧x∈U)" using assms Top_3_L11(1)
      zero_in_tgroup unfolding isT0_def G_def by blast moreover
    {
      assume "𝟬∈U"
      with ‹U∈T› have "U∈𝒩⇩0" using zerohoods_def G_def Top_2_L3 by auto
      with ‹x∈cl({𝟬})› and ‹cl({𝟬})=(⋂𝒩⇩0)› have "x∈U" by auto
    }
    ultimately have "𝟬∉U" and "x∈U" by auto
    with ‹U∈T› ‹x∈cl({𝟬})› have "False" using cl_inter_neigh zero_in_tgroup unfolding G_def by blast
  }
  then have "cl({𝟬})⊆{𝟬}" by auto
  then have "cl({𝟬})={𝟬}" using zero_in_tgroup cl_contains_set G_def by blast
  then show ?thesis using Top_3_L8 zero_in_tgroup unfolding G_def by auto
qed

subsection‹Existence of nice neighbourhoods.›

theorem(in topgroup) exists_sym_zerohood:
  assumes "U∈𝒩⇩0"
  shows "∃V∈𝒩⇩0. (V⊆U∧ (\<sm>V)=V)"
proof
  let ?V="U∩(\<sm>U)"
  have "U⊆G" using assms unfolding zerohoods_def by auto
  then have "?V⊆G" by auto
  have invg:" GroupInv(G, f) ∈ G → G" using group0_2_T2 Ggroup by auto
  have invb:"GroupInv(G, f) ∈bij(G,G)" using group0.group_inv_bij(2) group0_valid_in_tgroup by auto
  have "(\<sm>?V)=GroupInv(G,f)-``?V" unfolding setninv_def using group0.inv_image_vimage group0_valid_in_tgroup by auto
  also have "…=(GroupInv(G,f)-``U)∩(GroupInv(G,f)-``(\<sm>U))" using invim_inter_inter_invim invg by auto
  also have "…=(\<sm>U)∩(GroupInv(G,f)-``(GroupInv(G,f)``U))" unfolding setninv_def using group0.inv_image_vimage group0_valid_in_tgroup by auto
  also with ‹U⊆G› have "…=(\<sm>U)∩U" using inj_vimage_image invb unfolding bij_def
    by auto
  finally have "(\<sm>?V)=?V" by auto
  then show "?V ⊆ U ∧ (\<sm> ?V) = ?V" by auto
  from assms have "(\<sm>U)∈𝒩⇩0" using neg_neigh_neigh by auto
  with assms have "𝟬∈int(U)∩int(\<sm>U)" unfolding zerohoods_def by auto
  moreover 
  have "int(U)∩int(\<sm>U)∈T" using Top_2_L3 IsATopology_def topSpaceAssum Top_2_L4 by auto
  then have int:"int(int(U)∩int(\<sm>U))=int(U)∩int(\<sm>U)" using Top_2_L3 by auto
  have "int(U)∩int(\<sm>U)⊆?V" using Top_2_L1 by auto
  from interior_mono[OF this] int have "int(U)∩int(\<sm>U)⊆int(?V)" by auto
  ultimately have "𝟬∈int(?V)" by auto
  with ‹?V⊆G› show "?V∈𝒩⇩0" using zerohoods_def by auto
qed 

theorem(in topgroup) exists_procls_zerohood:
  assumes "U∈𝒩⇩0"
  shows "∃V∈𝒩⇩0. (V⊆U∧ (V\<sad>V)⊆U ∧ (\<sm>V)=V)"
proof-
  have "int(U)∈T" using Top_2_L2 by auto
  then have "f-``(int(U))∈τ" using fcon IsContinuous_def by auto
  moreover 
  have fne:"f ` ⟨𝟬, 𝟬⟩ = 𝟬" using group0.group0_2_L2 group0_valid_in_tgroup by auto
  have "𝟬∈int(U)" using assms unfolding zerohoods_def by auto
  then have "f -`` {𝟬}⊆f-``(int(U))" using func1_1_L8 vimage_def by auto
  then have "GroupInv(G,f)⊆f-``(int(U))" using group0.group0_2_T3 group0_valid_in_tgroup by auto
  then have "⟨𝟬,𝟬⟩∈f-``(int(U))" using fne zero_in_tgroup unfolding GroupInv_def
    by auto
  ultimately obtain W V where wop:"W∈T" and vop:"V∈T" and cartsub:"W×V⊆f-``(int(U))" and zerhood:"⟨𝟬,𝟬⟩∈W×V" using prod_top_point_neighb topSpaceAssum
    unfolding prodtop_def by force
  then have "𝟬∈W" and "𝟬∈V" by auto
  then have "𝟬∈W∩V" by auto
  have sub:"W∩V⊆G" using wop vop G_def by auto
  have assoc:"f∈G×G→G" using group0.group_oper_assocA group0_valid_in_tgroup by auto
  {
    fix t s assume "t∈W∩V" and "s∈W∩V"
    then have "t∈W" and "s∈V" by auto
    then have "⟨t,s⟩∈W×V" by auto
    then have "⟨t,s⟩∈f-``(int(U))" using cartsub by auto
    then have "f`⟨t,s⟩∈int(U)" using func1_1_L15 assoc by auto
  }
  then have "{f`⟨t,s⟩. ⟨t,s⟩∈(W∩V)×(W∩V)}⊆int(U)" by auto
  then have "(W∩V)\<sad>(W∩V)⊆int(U)" unfolding setadd_def using lift_subsets_explained(4) assoc sub
    by auto
  then have "(W∩V)\<sad>(W∩V)⊆U" using Top_2_L1 by auto
  from topSpaceAssum have "W∩V∈T" using vop wop unfolding IsATopology_def by auto
  then have "int(W∩V)=W∩V" using Top_2_L3 by auto
  with sub ‹𝟬∈W∩V› have "W∩V∈𝒩⇩0" unfolding zerohoods_def by auto
  then obtain Q where "Q∈𝒩⇩0" and "Q⊆W∩V" and "(\<sm>Q)=Q" using exists_sym_zerohood by blast
  then have "Q×Q⊆(W∩V)×(W∩V)" by auto 
  moreover from ‹Q⊆W∩V› have "W∩V⊆G" and "Q⊆G" using vop wop unfolding G_def by auto
  ultimately have "Q\<sad>Q⊆(W∩V)\<sad>(W∩V)" using interval_add(2) func1_1_L8 by auto
  with ‹(W∩V)\<sad>(W∩V)⊆U› have "Q\<sad>Q⊆U" by auto
  from ‹Q∈𝒩⇩0› have "𝟬∈Q" unfolding zerohoods_def using Top_2_L1 by auto
  with ‹Q\<sad>Q⊆U› ‹Q⊆G› have "𝟬\<ltr>Q⊆U" using interval_add(3) by auto
  with ‹Q⊆G› have "Q⊆U" unfolding ltrans_def using group0.trans_neutral(2) group0_valid_in_tgroup
    unfolding gzero_def using image_id_same by auto
  with ‹Q∈𝒩⇩0› ‹Q\<sad>Q⊆U› ‹(\<sm>Q)=Q› show ?thesis by auto
qed


lemma (in topgroup) exist_basehoods_closed:
  assumes "U∈𝒩⇩0"
  shows "∃V∈𝒩⇩0. cl(V)⊆U"
proof-
  from assms obtain V where "V∈𝒩⇩0" "V⊆U" "(V\<sad>V)⊆U" "(\<sm>V)=V" using exists_procls_zerohood by blast
  have inv_fun:"GroupInv(G,f)∈G→G" using group0_2_T2 Ggroup by auto
  have f_fun:"f∈G×G→G" using group0.group_oper_assocA group0_valid_in_tgroup by auto
  {
    fix x assume "x∈cl(V)"
    with ‹V∈𝒩⇩0› have "x∈⋃T" "V⊆⋃T" using Top_3_L11(1) unfolding zerohoods_def G_def by blast+
    with ‹V∈𝒩⇩0› have "x∈int(x\<ltr>V)" using elem_in_int_trans G_def by auto
    with ‹V⊆⋃T›‹x∈cl(V)› have "int(x\<ltr>V)∩V≠0" using cl_inter_neigh Top_2_L2 by blast
    then have "(x\<ltr>V)∩V≠0" using Top_2_L1 by blast
    then obtain q where "q∈(x\<ltr>V)" and "q∈V" by blast
    with ‹V⊆⋃T›‹x∈⋃T› obtain v where "q=x\<ra>v" "v∈V" unfolding ltrans_def grop_def using group0.ltrans_image
      group0_valid_in_tgroup unfolding G_def by auto
    from ‹V⊆⋃T› ‹v∈V›‹q∈V› have "v∈⋃T" "q∈⋃T" by auto
    with ‹q=x\<ra>v›‹x∈⋃T› have "q\<rs>v=x" using group0.group0_2_L18(1) group0_valid_in_tgroup unfolding G_def
        unfolding grsub_def grinv_def grop_def by auto moreover
    from ‹v∈V› have "(\<rm>v)∈(\<sm>V)" unfolding setninv_def grinv_def using func_imagedef inv_fun ‹V⊆⋃T› G_def by auto
    then have "(\<rm>v)∈V" using ‹(\<sm>V)=V› by auto
    with ‹q∈V› have "⟨q,\<rm>v⟩∈V×V" by auto
    then have "f`⟨q,\<rm>v⟩∈V\<sad>V" using lift_subset_suff f_fun ‹V⊆⋃T› unfolding setadd_def by auto
    with ‹V\<sad>V⊆U› have "q\<rs>v∈U" unfolding grsub_def grop_def by auto
    with ‹q\<rs>v=x› have "x∈U" by auto
  }
  then have "cl(V)⊆U" by auto
  with ‹V∈𝒩⇩0› show ?thesis by auto
qed

subsection‹Rest of separation axioms›

theorem(in topgroup) T1_imp_T2:
  assumes "T{is T⇩1}"
  shows "T{is T⇩2}"
proof-
  {
    fix x y assume ass:"x∈⋃T" "y∈⋃T" "x≠y"
    {
      assume "(\<rm>y)\<ra>x=𝟬"
      with ass(1,2) have "y=x" using group0.group0_2_L11[where a="y" and b="x"] group0_valid_in_tgroup by auto (*cannot be erased.*)
      with ass(3) have "False" by auto
    }
    then have "(\<rm>y)\<ra>x≠𝟬" by auto
    then have "𝟬≠(\<rm>y)\<ra>x" by auto
    from ‹y∈⋃T› have "(\<rm>y)∈⋃T" using neg_in_tgroup G_def by auto
    with ‹x∈⋃T› have "(\<rm>y)\<ra>x∈⋃T" using group0.group_op_closed[where a="\<rm>y" and b="x"] group0_valid_in_tgroup unfolding (*cannot be erased.*)
      G_def by auto
    with assms ‹𝟬≠(\<rm>y)\<ra>x› obtain U where "U∈T" and "(\<rm>y)\<ra>x∉U" and "𝟬∈U" unfolding isT1_def using zero_in_tgroup
      by auto
    then have "U∈𝒩⇩0" unfolding zerohoods_def G_def using Top_2_L3 by auto
    then obtain Q where "Q∈𝒩⇩0" "Q⊆U" "(Q\<sad>Q)⊆U" "(\<sm>Q)=Q" using exists_procls_zerohood by blast
    with ‹(\<rm>y)\<ra>x∉U› have "(\<rm>y)\<ra>x∉Q" by auto
    from ‹Q∈𝒩⇩0› have "Q⊆G" unfolding zerohoods_def by auto
    {
      assume "x∈y\<ltr>Q"
      with ‹Q⊆G› ‹y∈⋃T› obtain u where "u∈Q" and "x=y\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image group0_valid_in_tgroup
        unfolding G_def by auto
      with ‹Q⊆G› have "u∈⋃T" unfolding G_def by auto
      with ‹x=y\<ra>u› ‹y∈⋃T› ‹x∈⋃T› ‹Q⊆G› have "(\<rm>y)\<ra>x=u" using group0.group0_2_L18(2) group0_valid_in_tgroup unfolding G_def
        unfolding grsub_def grinv_def grop_def by auto
      with ‹u∈Q› have "(\<rm>y)\<ra>x∈Q" by auto
      then have "False" using ‹(\<rm>y)\<ra>x∉Q› by auto
    }
    then have "x∉y\<ltr>Q" by auto moreover
    {
      assume "y∈x\<ltr>Q"
      with ‹Q⊆G› ‹x∈⋃T› obtain u where "u∈Q" and "y=x\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image group0_valid_in_tgroup
        unfolding G_def by auto
      with ‹Q⊆G› have "u∈⋃T" unfolding G_def by auto
      with ‹y=x\<ra>u› ‹y∈⋃T› ‹x∈⋃T› ‹Q⊆G› have "(\<rm>x)\<ra>y=u" using group0.group0_2_L18(2) group0_valid_in_tgroup unfolding G_def
        unfolding grsub_def grinv_def grop_def by auto
      with ‹u∈Q› have "(\<rm>y)\<ra>x=\<rm>u" using group0.group_inv_of_two[OF group0_valid_in_tgroup group0.inverse_in_group[OF group0_valid_in_tgroup,of x],of y] (*From here no checked*)
        using ‹x∈⋃T› ‹y∈⋃T› using group0.group_inv_of_inv[OF group0_valid_in_tgroup] unfolding G_def grinv_def grop_def by auto
      moreover from ‹u∈Q› have "(\<rm>u)∈(\<sm>Q)" unfolding setninv_def grinv_def using func_imagedef[OF group0_2_T2[OF Ggroup] ‹Q⊆G›] by auto
      ultimately have "(\<rm>y)\<ra>x∈Q" using ‹(\<rm>y)\<ra>x∉Q› ‹(\<sm>Q)=Q› unfolding setninv_def grinv_def by auto
      then have "False" using ‹(\<rm>y)\<ra>x∉Q› by auto
    }
    then have "y∉x\<ltr>Q" by auto moreover
    {
      fix t
      assume "t∈(x\<ltr>Q)∩(y\<ltr>Q)"
      then have "t∈(x\<ltr>Q)" "t∈(y\<ltr>Q)" by auto
      with ‹Q⊆G› ‹x∈⋃T› ‹y∈⋃T› obtain u v where "u∈Q" "v∈Q" and "t=x\<ra>u" "t=y\<ra>v" unfolding ltrans_def grop_def using group0.ltrans_image[OF group0_valid_in_tgroup]
        unfolding G_def by auto
      then have "x\<ra>u=y\<ra>v" by auto
      moreover from ‹u∈Q› ‹v∈Q› ‹Q⊆G› have "u∈⋃T" "v∈⋃T" unfolding G_def by auto
      moreover note ‹x∈⋃T› ‹y∈⋃T›
      ultimately have "(\<rm>y)\<ra>(x\<ra>u)=v" using group0.group0_2_L18(2)[OF group0_valid_in_tgroup, of y v "x\<ra>u"] group0.group_op_closed[OF group0_valid_in_tgroup, of x u] unfolding G_def
        unfolding grsub_def grinv_def grop_def by auto
      then have "((\<rm>y)\<ra>x)\<ra>u=v" using group0.group_oper_assoc[OF group0_valid_in_tgroup]
        unfolding grop_def using ‹x∈⋃T› ‹y∈⋃T› ‹u∈⋃T› using group0.inverse_in_group[OF group0_valid_in_tgroup] unfolding G_def
        by auto
      then have "((\<rm>y)\<ra>x)=v\<rs>u" using group0.group0_2_L18(1)[OF group0_valid_in_tgroup,of "(\<rm>y)\<ra>x" u v]
        using ‹(\<rm>y)\<ra>x∈⋃T› ‹u∈⋃T› ‹v∈⋃T› unfolding G_def grsub_def grinv_def grop_def by force
      moreover 
      from ‹u∈Q› have "(\<rm>u)∈(\<sm>Q)" unfolding setninv_def grinv_def using func_imagedef[OF group0_2_T2[OF Ggroup] ‹Q⊆G›] by auto
      then have "(\<rm>u)∈Q" using ‹(\<sm>Q)=Q› by auto
      with ‹v∈Q› have "⟨v,\<rm>u⟩∈Q×Q" by auto
      then have "f`⟨v,\<rm>u⟩∈Q\<sad>Q" using lift_subset_suff[OF group0.group_oper_assocA[OF group0_valid_in_tgroup] ‹Q⊆G› ‹Q⊆G›]
        unfolding setadd_def by auto
      with ‹Q\<sad>Q⊆U› have "v\<rs>u∈U" unfolding grsub_def grop_def by auto
      ultimately have "(\<rm>y)\<ra>x∈U" by auto
      with ‹(\<rm>y)\<ra>x∉U› have "False" by auto
    }
    then have "(x\<ltr>Q)∩(y\<ltr>Q)=0" by auto
    moreover have "x∈int(x\<ltr>Q)""y∈int(y\<ltr>Q)" using elem_in_int_trans ‹Q∈𝒩⇩0›
      ‹x∈⋃T› ‹y∈⋃T› unfolding G_def by auto moreover
    have "int(x\<ltr>Q)⊆(x\<ltr>Q)""int(y\<ltr>Q)⊆(y\<ltr>Q)" using Top_2_L1 by auto
    moreover have "int(x\<ltr>Q)∈T" "int(y\<ltr>Q)∈T" using Top_2_L2 by auto
    ultimately have "int(x\<ltr>Q)∈T ∧ int(y\<ltr>Q)∈T ∧ x ∈ int(x\<ltr>Q) ∧ y ∈ int(y\<ltr>Q) ∧ int(x\<ltr>Q) ∩ int(y\<ltr>Q) = 0"
      by blast
    then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" by auto
  }
  then show ?thesis using isT2_def by auto
qed

text‹Here follow some auxiliary lemmas.›

lemma (in topgroup) trans_closure:
  assumes "x∈G" "A⊆G"
  shows "cl(x\<ltr>A)=x\<ltr>cl(A)"
proof-
  have "⋃T-(⋃T-(x\<ltr>A))=(x\<ltr>A)" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup assms(1)]
    unfolding image_def range_def domain_def converse_def Pi_def by auto
  then have "cl(x\<ltr>A)=⋃T-int(⋃T-(x\<ltr>A))" using Top_3_L11(2)[of "⋃T-(x\<ltr>A)"] by auto moreover
  have "x\<ltr>G=G" using surj_image_eq group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] bij_def by auto
  then have "⋃T-(x\<ltr>A)=x\<ltr>(⋃T-A)" using inj_image_dif[of "LeftTranslation(G, f, x)""G""G", OF _ assms(2)]
    unfolding ltrans_def G_def using group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] bij_def by auto
  then have "int(⋃T-(x\<ltr>A))=int(x\<ltr>(⋃T-A))" by auto
  then have "int(⋃T-(x\<ltr>A))=x\<ltr>int(⋃T-A)" using trans_interior[OF assms(1),of "⋃T-A"] unfolding G_def by force
  have "⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))" using Top_3_L11(2)[of "⋃T-A"] by force
  have "⋃T-(⋃T-A)=A" using assms(2) G_def by auto
  with ‹⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))› have "⋃T-int(⋃T-A)=cl(A)" by auto
  have "⋃T-(⋃T-int(⋃T-A))=int(⋃T-A)" using Top_2_L2 by auto
  with ‹⋃T-int(⋃T-A)=cl(A)› have "int(⋃T-A)=⋃T-cl(A)" by auto
  with ‹int(⋃T-(x\<ltr>A))=x\<ltr>int(⋃T-A)› have "int(⋃T-(x\<ltr>A))=x\<ltr>(⋃T-cl(A))" by auto
  with ‹x\<ltr>G=G› have "int(⋃T-(x\<ltr>A))=⋃T-(x\<ltr>cl(A))" using inj_image_dif[of "LeftTranslation(G, f, x)""G""G""cl(A)"]
    unfolding ltrans_def using group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] Top_3_L11(1) assms(2) unfolding bij_def G_def
    by auto
  then have "⋃T-int(⋃T-(x\<ltr>A))=⋃T-(⋃T-(x\<ltr>cl(A)))" by auto
  then have "⋃T-int(⋃T-(x\<ltr>A))=x\<ltr>cl(A)" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup assms(1)]
    unfolding image_def range_def domain_def converse_def Pi_def by auto
  with ‹cl(x\<ltr>A)=⋃T-int(⋃T-(x\<ltr>A))› show ?thesis by auto
qed

lemma (in topgroup) trans_interior2: assumes A1: "g∈G" and A2: "A⊆G" 
  shows "int(A)\<rtr>g = int(A\<rtr>g)"
proof -
  from assms have "A ⊆ ⋃T" and "IsAhomeomorphism(T,T,RightTranslation(G,f,g))"
    using tr_homeo by auto
  then show ?thesis using int_top_invariant by simp
qed

lemma (in topgroup) trans_closure2:
  assumes "x∈G" "A⊆G"
  shows "cl(A\<rtr>x)=cl(A)\<rtr>x"
proof-
  have "⋃T-(⋃T-(A\<rtr>x))=(A\<rtr>x)" unfolding ltrans_def using group0.group0_5_L1(1)[OF group0_valid_in_tgroup assms(1)]
    unfolding image_def range_def domain_def converse_def Pi_def by auto
  then have "cl(A\<rtr>x)=⋃T-int(⋃T-(A\<rtr>x))" using Top_3_L11(2)[of "⋃T-(A\<rtr>x)"] by auto moreover
  have "G\<rtr>x=G" using surj_image_eq group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] bij_def by auto
  then have "⋃T-(A\<rtr>x)=(⋃T-A)\<rtr>x" using inj_image_dif[of "RightTranslation(G, f, x)""G""G", OF _ assms(2)]
    unfolding rtrans_def G_def using group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] bij_def by auto
  then have "int(⋃T-(A\<rtr>x))=int((⋃T-A)\<rtr>x)" by auto
  then have "int(⋃T-(A\<rtr>x))=int(⋃T-A)\<rtr>x" using trans_interior2[OF assms(1),of "⋃T-A"] unfolding G_def by force
  have "⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))" using Top_3_L11(2)[of "⋃T-A"] by force
  have "⋃T-(⋃T-A)=A" using assms(2) G_def by auto
  with ‹⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))› have "⋃T-int(⋃T-A)=cl(A)" by auto
  have "⋃T-(⋃T-int(⋃T-A))=int(⋃T-A)" using Top_2_L2 by auto
  with ‹⋃T-int(⋃T-A)=cl(A)› have "int(⋃T-A)=⋃T-cl(A)" by auto
  with ‹int(⋃T-(A\<rtr>x))=int(⋃T-A)\<rtr>x› have "int(⋃T-(A\<rtr>x))=(⋃T-cl(A))\<rtr>x" by auto
  with ‹G\<rtr>x=G› have "int(⋃T-(A\<rtr>x))=⋃T-(cl(A)\<rtr>x)" using inj_image_dif[of "RightTranslation(G, f, x)""G""G""cl(A)"]
    unfolding rtrans_def using group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] Top_3_L11(1) assms(2) unfolding bij_def G_def
    by auto
  then have "⋃T-int(⋃T-(A\<rtr>x))=⋃T-(⋃T-(cl(A)\<rtr>x))" by auto
  then have "⋃T-int(⋃T-(A\<rtr>x))=cl(A)\<rtr>x" unfolding ltrans_def using group0.group0_5_L1(1)[OF group0_valid_in_tgroup assms(1)]
    unfolding image_def range_def domain_def converse_def Pi_def by auto
  with ‹cl(A\<rtr>x)=⋃T-int(⋃T-(A\<rtr>x))› show ?thesis by auto
qed

lemma (in topgroup) trans_subset:
  assumes "A⊆((\<rm>x)\<ltr>B)""x∈G""A⊆G""B⊆G"
  shows "x\<ltr>A⊆B"
proof-
  {
   fix t assume "t∈x\<ltr>A"
    with ‹x∈G› ‹A⊆G› obtain u where "u∈A" "t=x\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image[OF group0_valid_in_tgroup]
      unfolding G_def by auto
    with ‹x∈G› ‹A⊆G› ‹u∈A› have "(\<rm>x)\<ra>t=u" using group0.group0_2_L18(2)[OF group0_valid_in_tgroup, of "x""u""t"]
      group0.group_op_closed[OF group0_valid_in_tgroup,of x u] unfolding grop_def grinv_def by auto
    with ‹u∈A› have "(\<rm>x)\<ra>t∈A" by auto
    with ‹A⊆(\<rm>x)\<ltr>B› have "(\<rm>x)\<ra>t∈(\<rm>x)\<ltr>B" by auto
    with ‹B⊆G› obtain v where "(\<rm>x)\<ra>t=(\<rm>x)\<ra>v" "v∈B" unfolding ltrans_def grop_def using neg_in_tgroup[OF ‹x∈G›] group0.ltrans_image[OF group0_valid_in_tgroup]
      unfolding G_def by auto
    have "LeftTranslation(G,f,\<rm>x)∈inj(G,G)" using group0.trans_bij(2)[OF group0_valid_in_tgroup neg_in_tgroup[OF ‹x∈G›]] bij_def by auto
    then have eq:"∀A∈G. ∀B∈G. LeftTranslation(G,f,\<rm>x)`A=LeftTranslation(G,f,\<rm>x)`B ⟶ A=B" unfolding inj_def by auto
    {
      fix A B assume "A∈G""B∈G"
      assume "f`⟨\<rm>x,A⟩=f`⟨\<rm>x,B⟩"
      then have "LeftTranslation(G,f,\<rm>x)`A=LeftTranslation(G,f,\<rm>x)`B" using group0.group0_5_L2(2)[OF group0_valid_in_tgroup neg_in_tgroup[OF ‹x∈G›]]
        ‹A∈G›‹B∈G› by auto
      with eq ‹A∈G›‹B∈G› have "A=B" by auto
    }
    then have eq1:"∀A∈G. ∀B∈G. f`⟨\<rm>x,A⟩=f`⟨\<rm>x,B⟩ ⟶ A=B" by auto
    from ‹A⊆G› ‹u∈A› have "u∈G" by auto
    with ‹v∈B› ‹B⊆G› ‹t=x\<ra>u› have "t∈G" "v∈G" using group0.group_op_closed[OF group0_valid_in_tgroup ‹x∈G›,of u] unfolding grop_def
      by auto
    with eq1 ‹(\<rm>x)\<ra>t=(\<rm>x)\<ra>v› have "t=v" unfolding grop_def by auto
    with ‹v∈B› have "t∈B" by auto
  }
  then show ?thesis by auto
qed

text‹Every topological group is regular, and hence $T_3$. The proof is in the next
section, since it uses local properties.›

subsection‹Local properties›

text‹In a topological group, all local properties depend only on the neighbourhoods
of the neutral element; when considering topological properties. The next result
of regularity, will use this idea, since translations preserve closed sets.›

lemma (in topgroup) local_iff_neutral:
  assumes "∀U∈T∩𝒩⇩0. ∃N∈𝒩⇩0. N⊆U∧ P(N,T)" "∀N∈Pow(G). ∀x∈G. P(N,T) ⟶ P(x\<ltr>N,T)"
  shows "T{is locally}P"
proof-
  {
    fix x U assume "x∈⋃T""U∈T""x∈U"
    then have "(\<rm>x)\<ltr>U∈T∩𝒩⇩0" using open_tr_open(1) open_trans_neigh neg_in_tgroup unfolding G_def
      by auto
    with assms(1) obtain N where "N⊆((\<rm>x)\<ltr>U)""P(N,T)""N∈𝒩⇩0" by auto
    note ‹x∈⋃T›‹N⊆((\<rm>x)\<ltr>U)› moreover
    from ‹U∈T› have "U⊆⋃T" by auto moreover
    from ‹N∈𝒩⇩0› have "N⊆G" unfolding zerohoods_def by auto
    ultimately have "(x\<ltr>N)⊆U" using trans_subset unfolding G_def by auto moreover
    from ‹N⊆G›‹x∈⋃T› assms(2) ‹P(N,T)› have "P((x\<ltr>N),T)" unfolding G_def by auto moreover
    from ‹N∈𝒩⇩0›‹x∈⋃T› have "x∈int(x\<ltr>N)" using elem_in_int_trans unfolding G_def by auto
    ultimately have "∃N∈Pow(U). x∈int(N)∧P(N,T)" by auto
  }
  then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] by auto
qed

lemma (in topgroup) trans_closed:
  assumes "A{is closed in}T""x∈G"
  shows "(x\<ltr>A){is closed in}T"
proof-
  from assms(1) have "cl(A)=A" using Top_3_L8 unfolding IsClosed_def by auto
  then have "x\<ltr>cl(A)=x\<ltr>A" by auto
  then have "cl(x\<ltr>A)=x\<ltr>A" using trans_closure assms unfolding IsClosed_def by auto
  moreover have "x\<ltr>A⊆G" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup ‹x∈G›]
      unfolding image_def range_def domain_def converse_def Pi_def by auto
  ultimately show ?thesis using Top_3_L8 unfolding G_def by auto
qed

text‹As it is written in the previous section, every topological group is regular.›

theorem (in topgroup) topgroup_reg:
  shows "T{is regular}"
proof-
  {
    fix U assume "U∈T∩𝒩⇩0"
    then obtain V where "cl(V)⊆U""V∈𝒩⇩0" using exist_basehoods_closed by blast
    then have "V⊆cl(V)" using cl_contains_set unfolding zerohoods_def G_def by auto
    then have "int(V)⊆int(cl(V))" using interior_mono by auto
    with ‹V∈𝒩⇩0› have "cl(V)∈𝒩⇩0" unfolding zerohoods_def G_def using Top_3_L11(1) by auto
    from ‹V∈𝒩⇩0› have "cl(V){is closed in}T" using cl_is_closed unfolding zerohoods_def G_def by auto
    with ‹cl(V)∈𝒩⇩0›‹cl(V)⊆U› have "∃N∈𝒩⇩0. N⊆U∧N{is closed in}T" by auto
  }
  then have "∀U∈T∩𝒩⇩0. ∃N∈𝒩⇩0. N⊆U∧N{is closed in}T" by auto moreover
  have "∀N∈Pow(G).( ∀x∈G. (N{is closed in}T⟶(x\<ltr>N){is closed in}T))" using trans_closed by auto
  ultimately have "T{is locally-closed}" using local_iff_neutral unfolding IsLocallyClosed_def by auto
  then show "T{is regular}" using regular_locally_closed by auto
qed

text‹The promised corollary follows:›
    
corollary (in topgroup) T2_imp_T3:
  assumes "T{is T⇩2}"
  shows "T{is T⇩3}" using T2_is_T1 topgroup_reg isT3_def assms by auto

end