The Mizar article:

The Definition and Basic Properties of Topological Groups

by
Artur Kornilowicz

Received September 7, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: TOPGRP_1
[ MML identifier index ]


environ

 vocabulary PRE_TOPC, SGRAPH1, FUNCT_1, RELAT_1, SUBSET_1, VECTSP_1, REALSET1,
      GROUP_1, ORDINAL2, TOPS_2, CONNSP_2, TOPS_1, BOOLE, FUNCT_2, BINOP_1,
      UNIALG_1, URYSOHN1, COMPTS_1, SETFAM_1, PCOMPS_1, TARSKI, TOPGRP_1,
      RLVECT_3, SEQ_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, TOPS_2, FUNCT_1,
      PARTFUN1, BINOP_1, SETFAM_1, GRCAT_1, REALSET1, GROUP_1, GROUP_2,
      STRUCT_0, VECTSP_1, PRE_TOPC, TOPS_1, COMPTS_1, PCOMPS_1, URYSOHN1,
      BORSUK_1, T_0TOPSP, CANTOR_1, FUNCT_2, YELLOW_8;
 constructors REALSET1, TOPS_1, TOPS_2, GRCAT_1, T_0TOPSP, GROUP_7, URYSOHN1,
      COMPTS_1, CANTOR_1, YELLOW_8, MEMBERED;
 clusters BORSUK_1, BORSUK_2, STRUCT_0, GROUP_1, PRE_TOPC, WAYBEL10, TEX_1,
      PCOMPS_1, TOPS_1, RELSET_1, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FUNCT_1, PRE_TOPC, GROUP_1, STRUCT_0, TOPS_1, TOPS_2,
      VECTSP_1, REALSET1, CONNSP_2, FUNCT_2, T_0TOPSP, XBOOLE_0;
 theorems PRE_TOPC, VECTSP_1, RELAT_1, TOPS_1, TOPS_2, TMAP_1, BINOP_1,
      FUNCT_2, GROUP_1, GROUP_2, TARSKI, FUNCT_1, GRCAT_1, BORSUK_1, REALSET1,
      TEX_2, PCOMPS_1, ZFMISC_1, CONNSP_2, URYSOHN1, WAYBEL15, T_0TOPSP,
      YELLOW_8, YELLOW_9, TOPS_3, RELSET_1, SETFAM_1, XBOOLE_0, XBOOLE_1;
 schemes BINOP_1, FUNCT_2, XBOOLE_0;

begin  :: Preliminaries

reserve S for 1-sorted,
        R for non empty 1-sorted,
        X for Subset of R,
        T for non empty TopStruct,
        x for set;

definition let X be set;
 cluster one-to-one onto Function of X, X;
existence
  proof
    take id X;
    thus id X is one-to-one;
    thus rng id X = X by RELAT_1:71;
  end;
end;

theorem Th1:
 rng id S = [#]S
  proof
    thus rng id S = rng id the carrier of S by GRCAT_1:def 11
                 .= the carrier of S by RELAT_1:71
                 .= [#]S by PRE_TOPC:12;
  end;

definition let R be non empty 1-sorted;
 cluster (id R)/" -> one-to-one;
coherence
  proof
      dom (id R) = [#]R & rng (id R) = [#]R by Th1,TOPS_2:51;
    hence thesis by TOPS_2:63;
  end;
end;

theorem Th2:
 (id R)/" = id R
  proof
      dom (id R) = [#]R & rng (id R) = [#]R by Th1,TOPS_2:51;
    hence (id R)/" = (id R qua Function)" by TOPS_2:def 4
      .= (id the carrier of R)" by GRCAT_1:def 11
      .= id the carrier of R by FUNCT_1:67
      .= id R by GRCAT_1:def 11;
  end;

theorem
   (id R)"X = X
  proof
A1: (id R)/" = id R by Th2;
      dom id R = [#]R & rng id R = [#]R by Th1,TOPS_2:51;
    then (id R).:X = ((id R)/")"X by TOPS_2:67;
    hence thesis by A1,WAYBEL15:3;
  end;

definition let S be 1-sorted;
 cluster one-to-one onto map of S, S;
existence
  proof
    take id S;
    thus id S is one-to-one;
    thus rng id S = rng id the carrier of S by GRCAT_1:def 11
        .= the carrier of S by RELAT_1:71;
  end;
end;

begin  :: On the groups

reserve H for non empty HGrStr,
        P, Q, P1, Q1 for Subset of H,
        h for Element of H;

theorem Th4:
 P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1
  proof
    assume
A1:   P c= P1 & Q c= Q1;
    let x be set;
    assume x in P * Q;
    then consider g, t being Element of H such that
A2:   x = g * t & g in P & t in Q by GROUP_2:12;
    thus x in P1 * Q1 by A1,A2,GROUP_2:12;
  end;

theorem Th5:
 P c= Q implies P * h c= Q * h
  proof
    assume
A1:   P c= Q;
    let x be set;
    assume x in P * h;
    then consider g being Element of H such that
A2:   x = g * h & g in P by GROUP_2:34;
    thus x in Q * h by A1,A2,GROUP_2:34;
  end;

theorem
   P c= Q implies h * P c= h * Q
  proof
    assume
A1:   P c= Q;
    let x be set;
    assume x in h * P;
    then consider g being Element of H such that
A2:   x = h * g & g in P by GROUP_2:33;
    thus x in h * Q by A1,A2,GROUP_2:33;
  end;

reserve G for Group,
        A, B for Subset of G,
        a for Element of G;

theorem Th7:
  a in A" iff a" in A
  proof
A1: A" = {g" where g is Element of G: g in A} by GROUP_2:def 1;
    hereby
      assume a in A";
      then consider g being Element of G such that
A2:     a = g" & g in A by A1;
      thus a" in A by A2,GROUP_1:19;
    end;
    assume
A3:   a" in A;
      a"" = a by GROUP_1:19;
    hence a in A" by A1,A3;
  end;

theorem Th8:
 A"" = A
  proof
A1: A"" = {g" where g is Element of G: g in A"}
      by GROUP_2:def 1;
A2: A" = {g" where g is Element of G: g in A} by GROUP_2:def 1;
    hereby
      let x be set;
      assume x in A"";
      then consider g being Element of G such that
A3:     x = g" & g in A" by A1;
      consider h being Element of G such that
A4:     g = h" & h in A by A2,A3;
      thus x in A by A3,A4,GROUP_1:19;
    end;
    let x be set; assume
A5:   x in A;
    then reconsider g = x as Element of G;
      g" in A" by A2,A5;
    then g"" in A"" by A1;
    hence x in A"" by GROUP_1:19;
  end;

theorem Th9:
 A c= B iff A" c= B"
  proof
A1: A" = {g" where g is Element of G: g in A} by GROUP_2:def 1;
A2: B" = {g" where g is Element of G: g in B} by GROUP_2:def 1;
    thus A c= B implies A" c= B"
    proof
      assume
A3:     A c= B;
      let a be set;
      assume a in A";
      then consider g being Element of G such that
A4:     a = g" & g in A by A1;
      thus a in B" by A2,A3,A4;
    end;
    assume
A5:  A" c= B";
A6: A = A"" & B = B"" by Th8;
A7: A"" = {g" where g is Element of G: g in
 A"} by GROUP_2:def 1;
A8: B"" = {g" where g is Element of G: g in
 B"} by GROUP_2:def 1;
    let a be set;
    assume a in A;
    then consider g being Element of G such that
A9:     a = g" & g in A" by A6,A7;
    thus a in B by A5,A6,A8,A9;
  end;

theorem Th10:
 (inverse_op G).:A = A"
  proof
    set f = inverse_op G;
A1: A" = {g" where g is Element of G: g in A}
      by GROUP_2:def 1;
    hereby
      let y be set;
      assume y in f.:A;
      then consider x being set such that
A2:     x in the carrier of G & x in A & y = f.x by FUNCT_2:115;
      reconsider x as Element of G by A2;
        y = x" by A2,GROUP_1:def 6;
      hence y in A" by A1,A2;
    end;
    let y be set;
    assume y in A";
    then consider g being Element of G such that
A3:   y = g" & g in A by A1;
      f.g = g" by GROUP_1:def 6;
    hence y in f.:A by A3,FUNCT_2:43;
  end;

theorem Th11:
 (inverse_op G)"A = A"
  proof
    set f = inverse_op G;
A1: dom f = the carrier of G by FUNCT_2:def 1;
    hereby
      let x be set; assume
A2:     x in f"A;
      then reconsider g = x as Element of G;
        x in dom f & f.x in A by A2,FUNCT_1:def 13;
      then (f.g)" in A" by GROUP_2:5;
      then g"" in A" by GROUP_1:def 6;
      hence x in A" by GROUP_1:19;
    end;
    let x be set;
    assume x in A";
    then consider g being Element of G such that
A3:   x = g" & g in A by GROUP_2:5;
      f.(g") = g"" by GROUP_1:def 6
          .= g by GROUP_1:19;
    hence thesis by A1,A3,FUNCT_1:def 13;
  end;

theorem Th12:
 inverse_op G is one-to-one
  proof
    set f = inverse_op G;
    let x1, x2 be set; assume
A1:   x1 in dom f & x2 in dom f & f.x1 = f.x2;
    then reconsider a = x1, b = x2 as Element of G
      by FUNCT_2:def 1;
      f.a = a" & f.b = b" by GROUP_1:def 6;
    hence x1 = x2 by A1,GROUP_1:17;
  end;

theorem Th13:
 rng inverse_op G = the carrier of G
  proof
    set f = inverse_op G;
    thus rng f c= the carrier of G by RELSET_1:12;
    let x be set;
    assume x in the carrier of G;
    then reconsider a = x as Element of G;
A1: f.(a") = a"" by GROUP_1:def 6
          .= a by GROUP_1:19;
      dom f = the carrier of G by FUNCT_2:def 1;
    hence x in rng f by A1,FUNCT_1:def 5;
  end;

definition let G be Group;
  cluster inverse_op G -> one-to-one onto;
coherence
  proof
    thus inverse_op G is one-to-one by Th12;
    thus rng inverse_op G = the carrier of G by Th13;
  end;
end;

theorem Th14:
 (inverse_op G)" = inverse_op G
  proof
    set f = inverse_op G;
A1: dom f = the carrier of G & dom (f") = the carrier of G by FUNCT_2:def 1;
      now
      let x be set;
      assume x in dom f;
      then reconsider g = x as Element of G by FUNCT_2:def 1;
A2:   f.(g") = g"" by GROUP_1:def 6
            .= g by GROUP_1:19;
      thus f.x = g" by GROUP_1:def 6
              .= f".x by A1,A2,FUNCT_1:54;
    end;
    hence (inverse_op G)" = inverse_op G by A1,FUNCT_1:9;
  end;

theorem Th15:
 (the mult of H).:[:P,Q:] = P*Q
  proof
    set f = the mult of H;
A1: P*Q = {g * h where g, h is Element of H: g in P & h in Q}
      by GROUP_2:def 2;
    hereby
      let y be set;
      assume y in f.:[:P,Q:];
      then consider x being set such that
A2:     x in [:the carrier of H,the carrier of H:] & x in [:P,Q:] & y = f.x
          by FUNCT_2:115;
      consider a, b being set such that
A3:     a in P & b in Q & x = [a,b] by A2,ZFMISC_1:def 2;
      reconsider a, b as Element of H by A3;
        y = f.(a,b) by A2,A3,BINOP_1:def 1
       .= a*b by VECTSP_1:def 10;
      hence y in P*Q by A1,A3;
    end;
    let y be set;
    assume y in P*Q;
    then consider g, h being Element of H such that
A4:   y = g*h & g in P & h in Q by A1;
A5: [g,h] in [:the carrier of H, the carrier of H:] &
     [g,h] in [:P,Q:] by A4,ZFMISC_1:106;
      y = f.(g,h) by A4,VECTSP_1:def 10
     .= f. [g,h] by BINOP_1:def 1;
    hence y in f.:[:P,Q:] by A5,FUNCT_2:43;
  end;

definition let G be non empty HGrStr, a be Element of G;
 func a* -> map of G, G means :Def1:
  for x being Element of G holds it.x = a * x;
existence
  proof deffunc U(Element of G) = a * $1;
    consider f being Function of the carrier of G, the carrier of G such that
A1:   for x being Element of G holds f.x = U(x) from LambdaD;
    reconsider f as map of G, G;
    take f;
    thus thesis by A1;
  end;
uniqueness
  proof
    let f, g be map of G, G such that
A2:   for x being Element of G holds f.x = a * x and
A3:   for x being Element of G holds g.x = a * x;
      now
      let x be set;
      assume x in the carrier of G;
      then reconsider y = x as Element of G;
      thus f.x = a * y by A2
              .= g.x by A3;
    end;
    hence thesis by FUNCT_2:18;
  end;
 func *a -> map of G, G means :Def2:
  for x being Element of G holds it.x = x * a;
existence
  proof deffunc U(Element of G) = $1 *a;
    consider f being Function of the carrier of G, the carrier of G such that
A4:   for x being Element of G holds f.x = U(x) from LambdaD;
    reconsider f as map of G, G;
    take f;
    thus thesis by A4;
  end;
uniqueness
  proof
    let f, g be map of G, G such that
A5:   for x being Element of G holds f.x = x * a and
A6:   for x being Element of G holds g.x = x * a;
      now
      let x be set;
      assume x in the carrier of G;
      then reconsider y = x as Element of G;
      thus f.x = y * a by A5
              .= g.x by A6;
    end;
    hence thesis by FUNCT_2:18;
  end;
end;

definition let G be Group, a be Element of G;
 cluster a* -> one-to-one onto;
coherence
  proof
    set f = a*;
A1: dom f = the carrier of G by FUNCT_2:def 1;
    hereby
      let x1, x2 be set; assume
A2:     x1 in dom f & x2 in dom f & f.x1 = f.x2;
      then reconsider y1 = x1, y2 = x2 as Element of G
        by FUNCT_2:def 1;
A3:   f.y1 = a * y1 & f.y2 = a * y2 by Def1;
      thus x1 = 1.G * y1 by GROUP_1:def 4
             .= a" * a * y1 by GROUP_1:def 5
             .= a" * (a * y1) by VECTSP_1:def 16
             .= a" * a * y2 by A2,A3,VECTSP_1:def 16
             .= 1.G * y2 by GROUP_1:def 5
             .= x2 by GROUP_1:def 4;
    end;
    thus rng f c= the carrier of G by RELSET_1:12;
    let y be set;
    assume y in the carrier of G;
    then reconsider y1 = y as Element of G;
      f.(a"*y1) = a * (a" * y1) by Def1
             .= a * (a") * y1 by VECTSP_1:def 16
             .= 1.G * y1 by GROUP_1:def 5
             .= y by GROUP_1:def 4;
    hence y in rng f by A1,FUNCT_1:def 5;
  end;
 cluster *a -> one-to-one onto;
coherence
  proof
    set f = *a;
A4: dom f = the carrier of G by FUNCT_2:def 1;
    hereby
      let x1, x2 be set; assume
A5:     x1 in dom f & x2 in dom f & f.x1 = f.x2;
      then reconsider y1 = x1, y2 = x2 as Element of G
        by FUNCT_2:def 1;
A6:   f.y1 = y1 * a & f.y2 = y2 * a by Def2;
      thus x1 = y1 * 1.G by GROUP_1:def 4
             .= y1 * (a * a") by GROUP_1:def 5
             .= y1 * a * a" by VECTSP_1:def 16
             .= y2 * (a * a") by A5,A6,VECTSP_1:def 16
             .= y2 * 1.G by GROUP_1:def 5
             .= x2 by GROUP_1:def 4;
    end;
    thus rng f c= the carrier of G by RELSET_1:12;
    let y be set;
    assume y in the carrier of G;
    then reconsider y1 = y as Element of G;
      f.(y1*a") = y1 * a" * a by Def2
             .= y1 * (a" * a) by VECTSP_1:def 16
             .= y1 * 1.G by GROUP_1:def 5
             .= y by GROUP_1:def 4;
    hence y in rng f by A4,FUNCT_1:def 5;
  end;
end;

theorem Th16:
 h*.:P = h * P
  proof
    set f = h*;
A1: dom f = the carrier of H by FUNCT_2:def 1;
    hereby
      let y be set;
      assume y in f.:P;
      then consider x being set such that
A2:     x in dom f & x in P & y = f.x by FUNCT_1:def 12;
      reconsider x as Element of H by A2;
        f.x = h * x by Def1;
      hence y in h * P by A2,GROUP_2:33;
    end;
    let y be set;
    assume y in h * P;
    then consider s being Element of H such that
A3:   y = h * s & s in P by GROUP_2:33;
      f.s = h * s by Def1;
    hence y in f.:P by A1,A3,FUNCT_1:def 12;
  end;

theorem Th17:
 (*h).:P = P * h
  proof
    set f = *h;
A1: dom f = the carrier of H by FUNCT_2:def 1;
    hereby
      let y be set;
      assume y in f.:P;
      then consider x being set such that
A2:     x in dom f & x in P & y = f.x by FUNCT_1:def 12;
      reconsider x as Element of H by A2;
        f.x = x * h by Def2;
      hence y in P * h by A2,GROUP_2:34;
    end;
    let y be set;
    assume y in P * h;
    then consider s being Element of H such that
A3:   y = s * h & s in P by GROUP_2:34;
      f.s = s * h by Def2;
    hence y in f.:P by A1,A3,FUNCT_1:def 12;
  end;

theorem Th18:
 a*/" = a"*
  proof
    set f = a*,
        g = a"*;
A1: dom (f/") = the carrier of G & dom g = the carrier of G by FUNCT_2:def 1;
      now
      let y be set;
      assume y in the carrier of G;
      then reconsider y1 = y as Element of G;
      reconsider h = f as Function;
A2:   rng f = the carrier of G by FUNCT_2:def 3;
then A3:   y1 in rng f;
        dom f = the carrier of G by FUNCT_2:def 1;
then A4:   g.y1 in dom f & f/".y1 in dom f;
A5:   rng f = [#]G by A2,PRE_TOPC:12;
        f.(g.y) = a*(g.y1) by Def1
             .= a*(a"*y1) by Def1
             .= a*a"*y1 by VECTSP_1:def 16
             .= 1.G*y1 by GROUP_1:def 5
             .= y by GROUP_1:def 4
             .= h.(h".y) by A3,FUNCT_1:57
             .= f.(f/".y) by A5,TOPS_2:def 4;
      hence f/".y = g.y by A4,FUNCT_1:def 8;
    end;
    hence thesis by A1,FUNCT_1:9;
  end;

theorem Th19:
 (*a)/" = *(a")
  proof
    set f = *a,
        g = *(a");
A1: dom (f/") = the carrier of G & dom g = the carrier of G by FUNCT_2:def 1;
      now
      let y be set;
      assume y in the carrier of G;
      then reconsider y1 = y as Element of G;
      reconsider h = f as Function;
A2:   rng f = the carrier of G by FUNCT_2:def 3;
then A3:   y1 in rng f;
        dom f = the carrier of G by FUNCT_2:def 1;
then A4:   g.y1 in dom f & f/".y1 in dom f;
A5:   rng f = [#]G by A2,PRE_TOPC:12;
        f.(g.y) = (g.y1)*a by Def2
             .= y1*a"*a by Def2
             .= y1*(a"*a) by VECTSP_1:def 16
             .= y1*(1.G) by GROUP_1:def 5
             .= y by GROUP_1:def 4
             .= h.(h".y) by A3,FUNCT_1:57
             .= f.(f/".y) by A5,TOPS_2:def 4;
      hence f/".y = g.y by A4,FUNCT_1:def 8;
    end;
    hence thesis by A1,FUNCT_1:9;
  end;

begin  :: On the topological spaces

definition let T be non empty TopStruct;
 cluster (id T)/" -> continuous;
coherence by Th2;
end;

theorem Th20:
 id T is_homeomorphism
  proof
    thus dom id T = [#]T & rng id T = [#]T by Th1,TOPS_2:51;
    thus thesis;
  end;

definition let T be non empty TopSpace, p be Point of T;
 cluster -> non empty a_neighborhood of p;
coherence
  proof
    let N be a_neighborhood of p;
A1: p in Int N by CONNSP_2:def 1;
      Int N c= N by TOPS_1:44;
    hence thesis by A1;
  end;
end;

theorem Th21:
 for T being non empty TopSpace, p being Point of T holds
  [#]T is a_neighborhood of p
  proof
    let T be non empty TopSpace,
        p be Point of T;
      Int [#]T = [#]T by TOPS_1:43
          .= the carrier of T by PRE_TOPC:12;
    hence p in Int [#]T;
  end;

definition let T be non empty TopSpace, p be Point of T;
 cluster non empty open a_neighborhood of p;
existence
  proof
    reconsider B = [#]T as a_neighborhood of p by Th21;
    take B;
    thus thesis;
  end;
end;

theorem
   for S, T being non empty TopSpace, f being map of S, T st f is open holds
  for p being Point of S, P being a_neighborhood of p
   ex R being open a_neighborhood of f.p st R c= f.:P
  proof
    let S, T be non empty TopSpace, f be map of S, T such that
A1:     for A being Subset of S st A is open holds f.:A is open;
    let p be Point of S,
        P be a_neighborhood of p;
A2: f.:Int P is open by A1;
      p in Int P by CONNSP_2:def 1;
    then f.p in f.:Int P by FUNCT_2:43;
    then reconsider R = f.:Int P as open a_neighborhood of f.p by A2,CONNSP_2:5
;
    take R;
      Int P c= P by TOPS_1:44;
    hence R c= f.:P by RELAT_1:156;
  end;

theorem
   for S, T being non empty TopSpace, f being map of S, T st
   for p being Point of S, P being open a_neighborhood of p
    ex R being a_neighborhood of f.p st R c= f.:P
  holds f is open
  proof
    let S, T be non empty TopSpace, f be map of S, T such that
A1:   for p being Point of S, P being open a_neighborhood of p
       ex R being a_neighborhood of f.p st R c= f.:P;
    let A be Subset of S such that
A2:   A is open;
      for x being set holds x in f.:A iff ex Q being Subset of T
     st Q is open & Q c= f.:A & x in Q
    proof
      let x be set;
      hereby
        assume x in f.:A;
        then consider a being set such that
A3:        a in dom f & a in A & x = f.a by FUNCT_1:def 12;
        reconsider p = a as Point of S by A3;
        consider V being Subset of S such that
A4:       V is open & V c= A & a in V by A2,A3;
          V is a_neighborhood of p by A4,CONNSP_2:5;
        then consider R being a_neighborhood of f.p such that
A5:       R c= f.:V by A1,A4;
        take K = Int R;
        thus K is open;
A6:     f.:V c= f.:A by A4,RELAT_1:156;
          Int R c= R by TOPS_1:44;
        then K c= f.:V by A5,XBOOLE_1:1;
        hence K c= f.:A by A6,XBOOLE_1:1;
        thus x in K by A3,CONNSP_2:def 1;
      end;
      thus thesis;
    end;
    hence f.:A is open by TOPS_1:57;
  end;

theorem
   for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of T holds P is closed iff f"P is closed
  proof
    let S, T be non empty TopStruct,
        f be map of S, T;
    hereby
      assume
A1:     f is_homeomorphism;
      hence
A2:     dom f = [#]S & rng f = [#]T & f is one-to-one by TOPS_2:def 5;
      let P be Subset of T;
      hereby assume
A3:       P is closed;
          f is continuous by A1,TOPS_2:def 5;
        hence f"P is closed by A3,PRE_TOPC:def 12;
      end;
      assume f"P is closed;
then A4:   f.:(f"P) is closed by A1,TOPS_2:72;
        [#]T = the carrier of T by PRE_TOPC:12;
      hence P is closed by A2,A4,FUNCT_1:147;
    end;
    assume that
A5:   dom f = [#]S & rng f = [#]T & f is one-to-one and
A6:   for P being Subset of T holds
          P is closed iff f"P is closed;
    thus dom f = [#]S & rng f = [#]T & f is one-to-one by A5;
    thus f is continuous
    proof
      let P be Subset of T;
      thus P is closed implies f"P is closed by A6;
    end;
    let R be Subset of S such that
A7:   R is closed;
A8: (f/")"R = f.:R by A5,TOPS_2:67;
      for x1, x2 being Element of S st x1 in R & f.x1 = f.x2
     holds x2 in R
    proof
      let x1, x2 be Element of S such that
A9:     x1 in R & f.x1 = f.x2;
        dom f = the carrier of S by A5,PRE_TOPC:12;
      hence x2 in R by A5,A9,FUNCT_1:def 8;
    end;
    then f"(f.:R) = R by T_0TOPSP:2;
    hence (f/")"R is closed by A6,A7,A8;
  end;

theorem Th25:
 for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of S holds P is open iff f.:P is open
  proof
    let S, T be non empty TopStruct,
        f be map of S, T;
    hereby assume
A1:    f is_homeomorphism;
then A2:   f is continuous by TOPS_2:def 5;
A3:   f/" is continuous by A1,TOPS_2:def 5;
      thus
A4:     dom f = [#]S & rng f = [#]T & f is one-to-one by A1,TOPS_2:def 5;
      let P be Subset of S;
      hereby assume
A5:      P is open;
          (f/")"P = ((f qua Function)")"P by A4,TOPS_2:def 4
              .= f.:P by A4,FUNCT_1:154;
        hence f.:P is open by A3,A5,TOPS_2:55;
      end;
      assume f.:P is open;
then A6:   f"(f.:P) is open by A2,TOPS_2:55;
A7:   f"(f.:P) c= P by A4,FUNCT_1:152;
        P c= dom f by A4,PRE_TOPC:14;
      then P c= f"(f.:P) by FUNCT_1:146;
      hence P is open by A6,A7,XBOOLE_0:def 10;
    end;
    assume that
A8:  dom f = [#]S & rng f = [#]T and
A9:  f is one-to-one and
A10:  for P being Subset of S holds P is open iff f.:P is open;
      now
      let B be Subset of T such that
A11:     B is open;
        B c= rng f by A8,PRE_TOPC:14;
      then B = f.:f"B by FUNCT_1:147;
      hence f"B is open by A10,A11;
    end;
then A12: f is continuous by TOPS_2:55;
      now
      let B be Subset of S such that
A13:     B is open;
        (f/")"B = ((f qua Function)")"B by A8,A9,TOPS_2:def 4
            .= f.:B by A9,FUNCT_1:154;
      hence f/""B is open by A10,A13;
    end;
    then f/" is continuous by TOPS_2:55;
    hence thesis by A8,A9,A12,TOPS_2:def 5;
  end;

theorem
   for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of T holds P is open iff f"P is open
  proof
    let S, T be non empty TopStruct,
        f be map of S, T;
    hereby
      assume
A1:     f is_homeomorphism;
      hence
A2:     dom f = [#]S & rng f = [#]T & f is one-to-one by TOPS_2:def 5;
      let P be Subset of T;
      hereby assume
A3:       P is open;
          f is continuous by A1,TOPS_2:def 5;
        hence f"P is open by A3,TOPS_2:55;
      end;
      assume f"P is open;
then A4:   f.:(f"P) is open by A1,Th25;
        [#]T = the carrier of T by PRE_TOPC:12;
      hence P is open by A2,A4,FUNCT_1:147;
    end;
    assume that
A5:   dom f = [#]S & rng f = [#]T & f is one-to-one and
A6:   for P being Subset of T holds P is open iff f"P is open;
    thus dom f = [#]S & rng f = [#]T & f is one-to-one by A5;
    thus f is continuous by A6,TOPS_2:55;
      now
      let R be Subset of S such that
A7:     R is open;
A8:   (f/")"R = f.:R by A5,TOPS_2:67;
        for x1, x2 being Element of S st x1 in R & f.x1 = f.x2
       holds x2 in R
      proof
        let x1, x2 be Element of S such that
A9:       x1 in R & f.x1 = f.x2;
          dom f = the carrier of S by A5,PRE_TOPC:12;
        hence x2 in R by A5,A9,FUNCT_1:def 8;
      end;
      then f"(f.:R) = R by T_0TOPSP:2;
      hence (f/")"R is open by A6,A7,A8;
    end;
    hence thesis by TOPS_2:55;
  end;

theorem
   for S being TopSpace, T being non empty TopSpace, f being map of S, T holds
  f is continuous iff
  for P being Subset of T holds f"(Int P) c= Int(f"P)
  proof
    let S be TopSpace, T be non empty TopSpace, f be map of S, T;
    hereby assume
A1:    f is continuous;
      let P be Subset of T;
        Int P c= P by TOPS_1:44;
      then f"Int P c= f"P by RELAT_1:178;
then A2:   Int(f"Int P) c= Int(f"P) by TOPS_1:48;
      f"(Int P) is open by A1,TOPS_2:55;
      hence f"(Int P) c= Int(f"P) by A2,TOPS_1:55;
    end;
    assume
A3:  for P being Subset of T holds f"(Int P) c= Int(f"P);
      now
      let P be Subset of T such that
A4:     P is open;
        f"P = Int (f"P)
      proof
          Int P = P by A4,TOPS_1:55;
        hence f"P c= Int (f"P) by A3;
        thus thesis by TOPS_1:44;
      end;
      hence f"P is open;
    end;
    hence thesis by TOPS_2:55;
  end;

definition let T be non empty TopSpace;
 cluster non empty dense Subset of T;
existence
  proof
    take [#]T;
    thus thesis by TOPS_3:16;
  end;
end;

theorem Th28:
 for S, T being non empty TopSpace, f being map of S, T,
     A being dense Subset of S st f is_homeomorphism
  holds f.:A is dense
  proof
    let S, T be non empty TopSpace,
        f be map of S, T,
        A be dense Subset of S such that
A1:   f is_homeomorphism;
A2: Cl A = [#]S by TOPS_1:def 3;
A3: rng f = [#]T by A1,TOPS_2:def 5;
    thus Cl (f.:A) = f.:(Cl A) by A1,TOPS_2:74
                 .= f.:the carrier of S by A2,PRE_TOPC:12
                 .= [#]T by A3,FUNCT_2:45;
  end;

theorem Th29:
 for S, T being non empty TopSpace, f being map of S, T,
     A being dense Subset of T st f is_homeomorphism
  holds f"A is dense
  proof
    let S, T be non empty TopSpace,
        f be map of S, T,
        A be dense Subset of T such that
A1:   f is_homeomorphism;
A2: Cl A = [#]T by TOPS_1:def 3;
    thus Cl (f"A) = f"(Cl A) by A1,TOPS_2:73
                 .= [#]S by A2,TOPS_2:52;
  end;

definition let S, T be non empty TopStruct;
 cluster being_homeomorphism -> onto one-to-one continuous open map of S, T;
coherence
  proof
    let f be map of S, T; assume
A1:   f is_homeomorphism;
    then rng f = [#]T & dom f = [#]S by TOPS_2:def 5;
    hence rng f = the carrier of T by PRE_TOPC:12;
    thus f is one-to-one continuous by A1,TOPS_2:def 5;
    let A be Subset of S;
    thus thesis by A1,Th25;
  end;
end;

definition let T be non empty TopStruct;
 cluster being_homeomorphism map of T, T;
existence
  proof
    take id T;
    thus thesis by Th20;
  end;
end;

definition let T be non empty TopStruct,
               f be being_homeomorphism map of T, T;
 cluster f/" -> being_homeomorphism;
coherence by TOPS_2:70;
end;

begin  :: The group of homoemorphisms

definition let T be non empty TopStruct;
 mode Homeomorphism of T -> map of T, T means :Def3:
  it is_homeomorphism;
existence
  proof
    take id T;
    thus thesis by Th20;
  end;
end;

definition let T be non empty TopStruct;
 redefine func id T -> Homeomorphism of T;
coherence
  proof
    thus id T is_homeomorphism by Th20;
  end;
end;

definition let T be non empty TopStruct;
 cluster -> being_homeomorphism Homeomorphism of T;
coherence by Def3;
end;

theorem Th30:
 for f being Homeomorphism of T holds f/" is Homeomorphism of T
  proof
    let f be Homeomorphism of T;
    thus f/" is_homeomorphism;
  end;

theorem Th31:
 for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
  proof
    let f, g be Homeomorphism of T;
    thus f * g is_homeomorphism by TOPS_2:71;
  end;

definition let T be non empty TopStruct;
 func HomeoGroup T -> strict HGrStr means :Def4:
  (x in the carrier of it iff x is Homeomorphism of T) &
  for f, g being Homeomorphism of T holds (the mult of it).(f,g) = g * f;
existence
  proof defpred X[set] means $1 is Homeomorphism of T;
    consider A being set such that
A1:   for q being set holds q in A iff
       q in Funcs(the carrier of T,the carrier of T) & X[q] from Separation;
A2: now
      let f be Homeomorphism of T;
        f in Funcs(the carrier of T, the carrier of T) by FUNCT_2:12;
      hence f in A by A1;
    end;
    then reconsider A as non empty set;

defpred P[Element of A, Element of A, Element of A] means
 ex f, g being Homeomorphism of T st $1 = f & $2 = g & $3 = g * f;

A3: for x, y being Element of A ex z being Element of A st P[x,y,z]
    proof
      let x, y be Element of A;
      reconsider x1 = x, y1 = y as Homeomorphism of T by A1;
        y1 * x1 is Homeomorphism of T by Th31;
      then reconsider z = y1 * x1 as Element of A by A2;
      take z, x1, y1;
      thus thesis;
    end;
    consider o being BinOp of A such that
A4:  for a, b being Element of A holds P[a,b,o.(a,b)] from BinOpEx(A3);

    take G = HGrStr (#A, o#);
    let x;
    thus x in the carrier of G iff x is Homeomorphism of T by A1,A2;
    let f, g be Homeomorphism of T;
    reconsider f1 = f, g1 = g as Element of A by A2;
      ex m, n being Homeomorphism of T st f1 = m & g1 = n & o.(f1,g1) = n * m
     by A4;
    hence (the mult of G).(f,g) = g * f;
  end;
uniqueness
  proof
    let A, B be strict HGrStr;
    assume that
A5:  (x in the carrier of A iff x is Homeomorphism of T) &
     for f, g being Homeomorphism of T holds (the mult of A).(f,g) = g * f and
A6:  (x in the carrier of B iff x is Homeomorphism of T) &
     for f, g being Homeomorphism of T holds (the mult of B).(f,g) = g * f;
    defpred X[set] means $1 is Homeomorphism of T;
A7: for x being set holds x in the carrier of A iff X[x] by A5;
A8: for x being set holds x in the carrier of B iff X[x] by A6;
A9: the carrier of A = the carrier of B from Extensionality(A7,A8);
      for c, d being set st c in the carrier of A & d in the carrier of A
      holds (the mult of A). [c,d] = (the mult of B). [c,d]
    proof
      let c, d be set;
      assume c in the carrier of A & d in the carrier of A;
      then reconsider f = c, g = d as Homeomorphism of T by A5;
      thus (the mult of A). [c,d]
         = (the mult of A).(c,d) by BINOP_1:def 1
        .= g * f by A5
        .= (the mult of B).(c,d) by A6
        .= (the mult of B). [c,d] by BINOP_1:def 1;
    end;
    hence A = B by A9,FUNCT_2:118;
  end;
end;

definition let T be non empty TopStruct;
 cluster HomeoGroup T -> non empty;
coherence
  proof
      id T is Homeomorphism of T;
    hence the carrier of HomeoGroup T is non empty by Def4;
  end;
end;

theorem
   for f, g being Homeomorphism of T
  for a, b being Element of HomeoGroup T st f = a & g = b holds
   a * b = g * f
  proof
    let f, g be Homeomorphism of T,
        a, b be Element of HomeoGroup T such that
A1:   f = a & g = b;
    thus a * b = (the mult of HomeoGroup T).(a,b) by VECTSP_1:def 10
              .= g * f by A1,Def4;
  end;

definition let T be non empty TopStruct;
 cluster HomeoGroup T -> Group-like associative;
coherence
  proof
    set G = HomeoGroup T,
        o = the mult of G;
    thus G is Group-like
    proof
      reconsider e = id T as Element of G by Def4;
      take e;
      let h be Element of G;
      reconsider h1 = h, e1 = e as Homeomorphism of T by Def4;
      thus h * e = o.(h,e) by VECTSP_1:def 10
                .= e1 * h1 by Def4
                .= h by TMAP_1:93;
      thus e * h = o.(e,h) by VECTSP_1:def 10
                .= h1 * e1 by Def4
                .= h by TMAP_1:93;
      reconsider h1 = h as Homeomorphism of T by Def4;
        h1/" is Homeomorphism of T by Th30;
      then reconsider g = h1/" as Element of G by Def4;
      take g;
      reconsider g1 = g as Homeomorphism of T by Def4;
A1:   dom h1 = [#]T & rng h1 = [#]T by TOPS_2:def 5;
      thus h * g = o.(h,g) by VECTSP_1:def 10
                .= g1 * h1 by Def4
                .= id [#]T by A1,TOPS_2:65
                .= id the carrier of T by PRE_TOPC:12
                .= e by GRCAT_1:def 11;
      thus g * h = o.(g,h) by VECTSP_1:def 10
                .= h1 * g1 by Def4
                .= id [#]T by A1,TOPS_2:65
                .= id the carrier of T by PRE_TOPC:12
                .= e by GRCAT_1:def 11;
    end;
    let x, y, z be Element of G;
    reconsider f = x, g = y as Homeomorphism of T by Def4;
    reconsider p = g*f, r = z as Homeomorphism of T by Def4,Th31;
    reconsider a = r*g as Homeomorphism of T by Th31;
    thus (x*y)*z = o.(x*y,z) by VECTSP_1:def 10
                .= o.(o.(x,y),z) by VECTSP_1:def 10
                .= o.(g*f,z) by Def4
                .= r * p by Def4
                .= (r * g) * f by RELAT_1:55
                .= o.(f,a) by Def4
                .= o.(x,o.(y,z)) by Def4
                .= o.(x,y*z) by VECTSP_1:def 10
                .= x*(y*z) by VECTSP_1:def 10;
  end;
end;

theorem Th33:
 id T = 1.HomeoGroup T
  proof
    set G = HomeoGroup T;
    reconsider e = id T as Element of G by Def4;
      now
      let h be Element of G;
      reconsider h1 = h as Homeomorphism of T by Def4;
      thus h * e = (the mult of G).(h,e) by VECTSP_1:def 10
                .= id T * h1 by Def4
                .= h by TMAP_1:93;
      thus e * h = (the mult of G).(e,h) by VECTSP_1:def 10
                .= h1 * id T by Def4
                .= h by TMAP_1:93;
    end;
    hence id T = 1.HomeoGroup T by GROUP_1:10;
  end;

theorem
   for f being Homeomorphism of T
  for a being Element of HomeoGroup T st f = a holds a" = f/"
  proof
    let f be Homeomorphism of T,
        a be Element of HomeoGroup T such that
A1:   f = a;
    set G = HomeoGroup T;
A2: f/" is Homeomorphism of T
    proof
      thus f/" is_homeomorphism;
    end;
    then reconsider g = f/" as Element of G by Def4;
      now
A3:   dom f = [#]T & rng f = [#]T by TOPS_2:def 5;
      thus a * g = (the mult of G).(a,g) by VECTSP_1:def 10
                .= f/" * f by A1,A2,Def4
                .= id [#]T by A3,TOPS_2:65
                .= id the carrier of T by PRE_TOPC:12
                .= id T by GRCAT_1:def 11
                .= 1.G by Th33;
      thus g * a = (the mult of G).(g,a) by VECTSP_1:def 10
                .= f * (f/") by A1,A2,Def4
                .= id [#]T by A3,TOPS_2:65
                .= id the carrier of T by PRE_TOPC:12
                .= id T by GRCAT_1:def 11
                .= 1.G by Th33;
    end;
    hence a" = f/" by GROUP_1:12;
  end;

definition let T be non empty TopStruct;
 attr T is homogeneous means :Def5:
  for p, q being Point of T ex f being Homeomorphism of T st f.p = q;
end;

definition
 cluster trivial -> homogeneous (non empty TopStruct);
coherence
  proof
    let T be non empty TopStruct such that
A1:   T is trivial;
    let p, q be Point of T;
    take id T;
    thus (id T).p = q by A1,REALSET1:def 20;
  end;
end;

definition
 cluster strict trivial non empty TopSpace;
existence
  proof
    consider T being strict trivial non empty TopSpace;
    take T;
    thus thesis;
  end;
end;

theorem
   for T being homogeneous (non empty TopSpace) st
  ex p being Point of T st {p} is closed holds T is_T1
  proof
    let T be homogeneous (non empty TopSpace);
    given p being Point of T such that
A1:   {p} is closed;
      now
      let q be Point of T;
      consider f being Homeomorphism of T such that
A2:     f.p = q by Def5;
        dom f = the carrier of T by FUNCT_2:def 1;
      then f.:{p} = {f.p} by FUNCT_1:117;
      hence {q} is closed by A1,A2,TOPS_2:72;
    end;
    hence T is_T1 by URYSOHN1:27;
  end;

theorem Th36:
 for T being homogeneous (non empty TopSpace) st
  ex p being Point of T st for A being Subset of T st A is open & p in A holds
   ex B being Subset of T st p in B & B is open & Cl B c= A
  holds T is_T3
  proof
    let T be homogeneous (non empty TopSpace);
    given p being Point of T such that
A1:   for A being Subset of T st A is open & p in A holds
       ex B being Subset of T st p in B & B is open & Cl B c= A;
      now
      let A be open Subset of T,
          q be Point of T such that
A2:     q in A;
      consider f being Homeomorphism of T such that
A3:     f.p = q by Def5;
      reconsider g = f as Function;
A4:   dom f = the carrier of T by FUNCT_2:def 1;
      rng f = [#]T by TOPS_2:def 5;
then A6:   rng f = the carrier of T by PRE_TOPC:12;
A7:   p = g".q by A3,A4,FUNCT_1:54;
A8:   g".q = f".q;
        g.(g".q) in A by A2,A6,FUNCT_1:54;
then A9:   g".q in g"A by A4,A8,FUNCT_1:def 13;
        f"A is open by TOPS_2:55;
      then consider B being Subset of T such that
A10:     p in B & B is open & Cl B c= f"A by A1,A7,A9;
      reconsider fB = f.:B as open Subset of T by A10,Th25;
      take fB;
      thus q in fB by A3,A4,A10,FUNCT_1:def 12;
A11:   f.:Cl B c= f.:(f"A) by A10,RELAT_1:156;
        f.:Cl B = Cl fB by TOPS_2:74;
      hence Cl fB c= A by A6,A11,FUNCT_1:147;
    end;
    hence T is_T3 by URYSOHN1:29;
  end;

begin  :: On the topological groups

definition
  struct (HGrStr, TopStruct) TopGrStr
     (# carrier -> set,
           mult -> BinOp of the carrier,
       topology -> Subset-Family of the carrier #);
end;

definition let A be non empty set,
               R be BinOp of A,
               T be Subset-Family of A;
 cluster TopGrStr (#A, R, T#) -> non empty;
coherence
  proof
    thus the carrier of TopGrStr (#A,R,T#) is non empty;
  end;
end;

definition let x be set,
               R be BinOp of {x},
               T be Subset-Family of {x};
 cluster TopGrStr (#{x}, R, T#) -> trivial;
coherence
  proof
    let a, b be Element of TopGrStr (#{x},R,T#);
      a = x & b = x by TARSKI:def 1;
    hence thesis;
  end;
end;

definition
 cluster trivial -> Group-like associative commutative (non empty HGrStr);
coherence
  proof
    let H be non empty HGrStr such that
A1:   H is trivial;
    hereby
      consider e being Element of H;
      take e;
      let h be Element of H;
      thus h * e = h & e * h = h by A1,REALSET1:def 20;
      take g = e;
      thus h * g = e & g * h = e by A1,REALSET1:def 20;
    end;
    thus for x, y, z being Element of H holds
      x*y*z = x*(y*z) by A1,REALSET1:def 20;
    let x, y be Element of H;
    thus thesis by A1,REALSET1:def 20;
  end;
end;

definition let a be set;
 cluster 1TopSp {a} -> trivial;
coherence
  proof
    let x, y be Element of 1TopSp {a};
      1TopSp {a} = TopStruct (#{a},bool {a}#) by PCOMPS_1:def 1;
    then a = x & a = y by TARSKI:def 1;
    hence thesis;
  end;
end;

definition
 cluster strict non empty TopGrStr;
existence
  proof
    consider R being BinOp of {0}, T being Subset-Family of {0};
    take TopGrStr (#{0},R,T#);
    thus thesis;
  end;
end;

definition
 cluster strict TopSpace-like trivial (non empty TopGrStr);
existence
  proof
    consider R being BinOp of {0};
    take TopGrStr (#{0}, R, bool {0}#);
      1TopSp {0} = TopStruct (#{0},bool {0}#) by PCOMPS_1:def 1;
    hence thesis by TEX_2:12;
  end;
end;

definition let G be Group-like associative (non empty TopGrStr);
 redefine func inverse_op G -> map of G, G;
coherence;
end;

definition let G be Group-like associative (non empty TopGrStr);
 attr G is UnContinuous means :Def6:
  inverse_op G is continuous;
end;

definition let G be TopSpace-like TopGrStr;
 attr G is BinContinuous means :Def7:
  for f being map of [:G,G:], G st f = the mult of G holds f is continuous;
end;

definition
 cluster strict commutative trivial UnContinuous BinContinuous
         (TopSpace-like Group-like associative (non empty TopGrStr));
existence
  proof
    consider R being BinOp of {0};
      1TopSp {0} = TopStruct (#{0},bool {0}#) by PCOMPS_1:def 1;
    then reconsider T = TopGrStr (#{0}, R, bool {0}#)
     as strict TopSpace-like Group-like associative
     (non empty TopGrStr) by TEX_2:12;
    take T;
    thus T is strict commutative trivial;
    hereby
      set f = inverse_op T;
      thus f is continuous
      proof
        let P1 be Subset of T such that P1 is closed;
        per cases by ZFMISC_1:39;
        suppose f"P1 = {};
        then f"P1 = {}T;
        hence f"P1 is closed;
        suppose f"P1 = {0};
        then f"P1 = [#]T by PRE_TOPC:12;
        hence f"P1 is closed;
      end;
    end;
    let f be map of [:T,T:], T such that
        f = the mult of T;
A1: the carrier of [:T,T:] = [:{0},{0}:] by BORSUK_1:def 5
      .= {[0,0]} by ZFMISC_1:35;
    let P1 be Subset of T such that P1 is closed;
    per cases by A1,ZFMISC_1:39;
    suppose f"P1 = {};
    then f"P1 = {}[:T,T:];
    hence f"P1 is closed;
    suppose f"P1 = {[0,0]};
    then f"P1 = [#][:T,T:] by A1,PRE_TOPC:12;
    hence f"P1 is closed;
  end;
end;

definition
 mode TopGroup is TopSpace-like Group-like associative (non empty TopGrStr);
end;

definition
 mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;

theorem Th37:
 for T being BinContinuous non empty (TopSpace-like TopGrStr),
     a, b being Element of T,
     W being a_neighborhood of a*b
  ex A being open a_neighborhood of a, B being open a_neighborhood of b st
   A*B c= W
  proof
    let T be BinContinuous non empty (TopSpace-like TopGrStr),
        a, b be Element of T,
        W be a_neighborhood of a*b;
      the carrier of [:T,T:] = [:the carrier of T,the carrier of T:]
      by BORSUK_1:def 5;
    then reconsider f = the mult of T as map of [:T,T:], T;
A1: f. [a,b] = f.(a,b) by BINOP_1:def 1
            .= a*b by VECTSP_1:def 10;
      f is continuous by Def7;
    then consider H being a_neighborhood of [a,b] such that
A2:   f.:H c= W by A1,BORSUK_1:def 2;
A3: [a,b] in Int H by CONNSP_2:def 1;
    consider F being Subset-Family of [:T,T:] such that
A4:   Int H = union F and
A5:   for e being set st e in F ex X1, Y1 being Subset of T st
      e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:45;
    consider M being set such that
A6:   [a,b] in M & M in F by A3,A4,TARSKI:def 4;
    consider A, B being Subset of T such that
A7:   M = [:A,B:] & A is open & B is open by A5,A6;
      a in A & b in B by A6,A7,ZFMISC_1:106;
then A8: a in Int A & b in Int B by A7,TOPS_1:55;
    then reconsider A as open a_neighborhood of a by A7,CONNSP_2:def 1;
    reconsider B as open a_neighborhood of b by A7,A8,CONNSP_2:def 1;
A9: A*B = {g * h where g, h is Element of T: g in A & h in B}
      by GROUP_2:def 2;
    take A, B;
    let x be set;
    assume x in A*B;
    then consider g, h being Element of T such that
A10:   x = g*h & g in A & h in B by A9;
      [g,h] in M by A7,A10,ZFMISC_1:106;
then A11:[g,h] in Int H by A4,A6,TARSKI:def 4;
A12:Int H c= H by TOPS_1:44;
      f. [g,h] = f.(g,h) by BINOP_1:def 1
            .= g*h by VECTSP_1:def 10;
    then x in f.:H by A10,A11,A12,FUNCT_2:43;
    hence x in W by A2;
  end;

theorem Th38:
 for T being TopSpace-like non empty TopGrStr st
  (for a, b being Element of T,
       W being a_neighborhood of a*b
   ex A being a_neighborhood of a, B being a_neighborhood of b st A*B c= W)
  holds T is BinContinuous
  proof
    let T be TopSpace-like non empty TopGrStr such that
A1:   for a, b being Element of T,
          W being a_neighborhood of a*b
      ex A being a_neighborhood of a, B being a_neighborhood of b st A*B c= W;
    let f be map of [:T,T:], T such that
A2:   f = the mult of T;
      for W being Point of [:T,T:], G being a_neighborhood of f.W
      ex H being a_neighborhood of W st f.:H c= G
    proof
      let W be Point of [:T,T:],
          G be a_neighborhood of f.W;
      consider a, b being Point of T such that
A3:     W = [a,b] by BORSUK_1:50;
        f.W = f.(a,b) by A3,BINOP_1:def 1
         .= a*b by A2,VECTSP_1:def 10;
      then consider A being a_neighborhood of a,
               B being a_neighborhood of b such that
A4:     A*B c= G by A1;
      reconsider H = [:A,B:] as a_neighborhood of W by A3;
      take H;
      thus f.:H c= G by A2,A4,Th15;
    end;
    hence f is continuous by BORSUK_1:def 2;
  end;

theorem Th39:
 for T being UnContinuous TopGroup,
     a being Element of T,
     W being a_neighborhood of a"
  ex A being open a_neighborhood of a st A" c= W
  proof
    let T be UnContinuous TopGroup,
        a be Element of T,
        W be a_neighborhood of a";
    reconsider f = inverse_op T as map of T, T;
A1: f.a = a" by GROUP_1:def 6;
      f is continuous by Def6;
    then consider H being a_neighborhood of a such that
A2:   f.:H c= W by A1,BORSUK_1:def 2;
      a in Int H by CONNSP_2:def 1;
    then a in Int Int H by TOPS_1:45;
    then reconsider A = Int H as open a_neighborhood of a by CONNSP_2:def 1;
    take A;
A3: A" = {g" where g is Element of T: g in A} by GROUP_2:def 1;
    let x be set;
    assume x in A";
    then consider g being Element of T such that
A4:   x = g" & g in A by A3;
A5: Int H c= H by TOPS_1:44;
      f.g = g" by GROUP_1:def 6;
    then g" in f.:H by A4,A5,FUNCT_2:43;
    hence x in W by A2,A4;
  end;

theorem Th40:
 for T being TopGroup st
   for a being Element of T,
        W being a_neighborhood of a"
     ex A being a_neighborhood of a st A" c= W holds
  T is UnContinuous
  proof
    let T be TopGroup such that
A1:   for a being Element of T, W being a_neighborhood of a"
       ex A being a_neighborhood of a st A" c= W;
    set f = inverse_op T;
      for W being Point of T, G being a_neighborhood of f.W
      ex H being a_neighborhood of W st f.:H c= G
    proof
      let a be Point of T,
          G be a_neighborhood of f.a;
        f.a = a" by GROUP_1:def 6;
      then consider A being a_neighborhood of a such that
A2:     A" c= G by A1;
      take A;
      thus f.:A c= G by A2,Th10;
    end;
    hence f is continuous by BORSUK_1:def 2;
  end;

theorem Th41:
 for T being TopologicalGroup, a, b being Element of T
  for W being a_neighborhood of a*(b")
   ex A being open a_neighborhood of a, B being open a_neighborhood of b st
    A*(B") c= W
  proof
    let T be TopologicalGroup,
        a, b be Element of T,
        W be a_neighborhood of a*(b");
    consider A being open a_neighborhood of a,
             B being open a_neighborhood of b" such that
A1:   A*B c= W by Th37;
    consider C being open a_neighborhood of b such that
A2:   C" c= B by Th39;
    take A, C;
A3: A*B = {g*h where g, h is Element of T: g in A & h in B}
      by GROUP_2:def 2;
A4: A*(C") = {g*h where g, h is Element of T: g in A & h in C"}
      by GROUP_2:def 2;
A5: C" = {g" where g is Element of T: g in C} by GROUP_2:def 1;
    let x be set;
    assume x in A*(C");
    then consider g, h being Element of T such that
A6:   x = g*h & g in A & h in C" by A4;
    consider k being Element of T such that
A7:   h = k" & k in C by A5,A6;
      g*(k") in A*B by A2,A3,A6,A7;
    hence x in W by A1,A6,A7;
  end;

theorem
   for T being TopGroup st
   for a, b being Element of T,
        W being a_neighborhood of a*(b")
    ex A being a_neighborhood of a, B being a_neighborhood of b st
     A*(B") c= W holds
  T is TopologicalGroup
  proof
    let T be TopGroup such that
A1:   for a, b being Element of T,
          W being a_neighborhood of a*(b")
       ex A being a_neighborhood of a, B being a_neighborhood of b st
        A*(B") c= W;
A2: for a being Element of T,
        W being a_neighborhood of a"
     ex A being a_neighborhood of a st A" c= W
    proof
      let a be Element of T,
          W be a_neighborhood of a";
        W is a_neighborhood of 1.T*(a") by GROUP_1:def 4;
      then consider A being a_neighborhood of 1.T,
               B being a_neighborhood of a such that
A3:     A*(B") c= W by A1;
      take B;
      let x be set; assume
A4:     x in B";
      then consider g being Element of T such that
A5:     x = g" & g in B by GROUP_2:5;
        1.T in A by CONNSP_2:6;
      then 1.T * (g") in A*(B") by A4,A5,GROUP_2:12;
      then g" in A*(B") by GROUP_1:def 4;
      hence x in W by A3,A5;
    end;
      for a, b being Element of T,
        W being a_neighborhood of a*b
     ex A being a_neighborhood of a, B being a_neighborhood of b st A*B c= W
    proof
      let a, b be Element of T,
          W be a_neighborhood of a*b;
        W is a_neighborhood of a*(b"") by GROUP_1:19;
      then consider A being a_neighborhood of a,
               B being a_neighborhood of b" such that
A6:     A*(B") c= W by A1;
      consider B1 being a_neighborhood of b such that
A7:     B1" c= B by A2;
      take A, B1;
      let x be set; assume
       x in A * B1;
      then consider g, h being Element of T such that
A8:     x = g * h & g in A & h in B1 by GROUP_2:12;
        h" in B1" by A8,GROUP_2:5;
      then h in B" by A7,Th7;
      then x in A*(B") by A8,GROUP_2:12;
      hence x in W by A6;
    end;
    hence thesis by A2,Th38,Th40;
  end;

definition let G be BinContinuous non empty (TopSpace-like TopGrStr),
               a be Element of G;
 cluster a* -> continuous;
coherence
  proof
    set f = a*;
      for w being Point of G, A being a_neighborhood of f.w
     ex W being a_neighborhood of w st f.:W c= A
    proof
      let w be Point of G,
          A be a_neighborhood of f.w;
        f.w = a * w by Def1;
      then consider B being open a_neighborhood of a,
               W being open a_neighborhood of w such that
A1:     B*W c= A by Th37;
      take W;
      let k be set;
      assume k in f.:W;
      then k in a * W by Th16;
      then consider h being Element of G such that
A2:     k = a * h & h in W by GROUP_2:33;
        a in B by CONNSP_2:6;
      then k in B * W by A2,GROUP_2:12;
      hence k in A by A1;
    end;
    hence f is continuous by BORSUK_1:def 2;
  end;
 cluster *a -> continuous;
coherence
  proof
    set f = *a;
      for w being Point of G, A being a_neighborhood of f.w
     ex W being a_neighborhood of w st f.:W c= A
    proof
      let w be Point of G,
          A be a_neighborhood of f.w;
        f.w = w * a by Def2;
      then consider W being open a_neighborhood of w,
               B being open a_neighborhood of a such that
A3:     W*B c= A by Th37;
      take W;
      let k be set;
      assume k in f.:W;
      then k in W * a by Th17;
      then consider h being Element of G such that
A4:     k = h * a & h in W by GROUP_2:34;
        a in B by CONNSP_2:6;
      then k in W * B by A4,GROUP_2:12;
      hence k in A by A3;
    end;
    hence f is continuous by BORSUK_1:def 2;
  end;
end;

theorem Th43:
 for G being BinContinuous TopGroup,
     a being Element of G holds
   a* is Homeomorphism of G
  proof
    let G be BinContinuous TopGroup,
        a be Element of G;
    set f = a*;
      dom f = the carrier of G & rng f = the carrier of G by FUNCT_2:def 1,def
3
;
    hence dom f = [#]G & rng f = [#]G & f is one-to-one by PRE_TOPC:12;
    thus f is continuous;
      f/" = (a"*) by Th18;
    hence f/" is continuous;
  end;

theorem Th44:
 for G being BinContinuous TopGroup,
     a being Element of G holds
  *a is Homeomorphism of G
  proof
    let G be BinContinuous TopGroup,
        a be Element of G;
    set f = *a;
      dom f = the carrier of G & rng f = the carrier of G by FUNCT_2:def 1,def
3
;
    hence dom f = [#]G & rng f = [#]G & f is one-to-one by PRE_TOPC:12;
    thus f is continuous;
      f/" = *(a") by Th19;
    hence f/" is continuous;
  end;

definition let G be BinContinuous TopGroup,
               a be Element of G;
 redefine func a* -> Homeomorphism of G;
coherence by Th43;
 redefine func *a -> Homeomorphism of G;
coherence by Th44;
end;

theorem Th45:
 for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G
  proof
    let G be UnContinuous TopGroup;
    set f = inverse_op G;
      dom f = the carrier of G & rng f = the carrier of G by FUNCT_2:def 1,def
3
;
    hence
A1:   dom f = [#]G & rng f = [#]G & f is one-to-one by PRE_TOPC:12;
    thus f is continuous by Def6;
      f = (f qua Function)" by Th14
     .= f/" by A1,TOPS_2:def 4;
    hence f/" is continuous by Def6;
  end;

definition let G be UnContinuous TopGroup;
 redefine func inverse_op G -> Homeomorphism of G;
coherence by Th45;
end;

definition
 cluster BinContinuous -> homogeneous TopGroup;
coherence
  proof
    let T be TopGroup;
    assume T is BinContinuous;
    then reconsider G = T as BinContinuous TopGroup;
      G is homogeneous
    proof
      let p, q be Point of G;
      take *(p"*q);
      thus (*(p"*q)).p = p*(p"*q) by Def2
                      .= p*p"*q by VECTSP_1:def 16
                      .= 1.G*q by GROUP_1:def 5
                      .= q by GROUP_1:def 4;
    end;
    hence thesis;
  end;
end;

theorem Th46:
 for G being BinContinuous TopGroup, F being closed Subset of G,
     a being Element of G holds F * a is closed
  proof
    let G be BinContinuous TopGroup,
        F be closed Subset of G,
        a be Element of G;
      F * a = (*a).:F by Th17;
    hence F * a is closed by TOPS_2:72;
  end;

theorem Th47:
 for G being BinContinuous TopGroup, F being closed Subset of G,
     a being Element of G holds a * F is closed
  proof
    let G be BinContinuous TopGroup,
        F be closed Subset of G,
        a be Element of G;
      a * F = (a*).:F by Th16;
    hence a * F is closed by TOPS_2:72;
  end;

definition let G be BinContinuous TopGroup,
               F be closed Subset of G,
               a be Element of G;
 cluster F * a -> closed;
coherence by Th46;
 cluster a * F -> closed;
coherence by Th47;
end;

theorem Th48:
 for G being UnContinuous TopGroup, F being closed Subset of G
  holds F" is closed
  proof
    let G be UnContinuous TopGroup,
        F be closed Subset of G;
      F" = (inverse_op G).:F by Th10;
    hence F" is closed by TOPS_2:72;
  end;

definition let G be UnContinuous TopGroup,
               F be closed Subset of G;
 cluster F" -> closed;
coherence by Th48;
end;

theorem Th49:
 for G being BinContinuous TopGroup, O being open Subset of G,
     a being Element of G holds O * a is open
  proof
    let G be BinContinuous TopGroup,
        O be open Subset of G,
        a be Element of G;
      O * a = (*a).:O by Th17;
    hence O * a is open by Th25;
  end;

theorem Th50:
 for G being BinContinuous TopGroup, O being open Subset of G,
     a being Element of G holds a * O is open
  proof
    let G be BinContinuous TopGroup,
        O be open Subset of G,
        a be Element of G;
      a * O = (a*).:O by Th16;
    hence a * O is open by Th25;
  end;

definition let G be BinContinuous TopGroup,
               A be open Subset of G,
               a be Element of G;
 cluster A * a -> open;
coherence by Th49;
 cluster a * A -> open;
coherence by Th50;
end;

theorem Th51:
 for G being UnContinuous TopGroup, O being open Subset of G holds O" is open
  proof
    let G be UnContinuous TopGroup,
        O be open Subset of G;
      O" = (inverse_op G).:O by Th10;
    hence O" is open by Th25;
  end;

definition let G be UnContinuous TopGroup,
               A be open Subset of G;
 cluster A" -> open;
coherence by Th51;
end;

theorem Th52:
 for G being BinContinuous TopGroup, A, O being Subset of G st O is open
  holds O * A is open
  proof
    let G be BinContinuous TopGroup,
        A, O be Subset of G such that
A1:   O is open;
      Int (O * A) = O * A
    proof
      thus Int (O * A) c= O * A by TOPS_1:44;
      let x be set;
      assume x in O * A;
      then consider o, a being Element of G such that
A2:     x = o * a & o in O & a in A by GROUP_2:12;
      set Q = O * a;
A3:   Q is open by A1,Th49;
A4:   Q c= O * A
      proof
        let q be set;
        assume q in Q;
        then consider h being Element of G such that
A5:       q = h * a & h in O by GROUP_2:34;
        thus thesis by A2,A5,GROUP_2:12;
      end;
        x in Q by A2,GROUP_2:34;
      hence x in Int (O * A) by A3,A4,TOPS_1:54;
    end;
    hence O * A is open;
  end;

theorem Th53:
 for G being BinContinuous TopGroup, A, O being Subset of G st O is open
  holds A * O is open
  proof
    let G be BinContinuous TopGroup,
        A, O be Subset of G such that
A1:   O is open;
      Int (A * O) = A * O
    proof
      thus Int (A * O) c= A * O by TOPS_1:44;
      let x be set;
      assume x in A * O;
      then consider a, o being Element of G such that
A2:     x = a * o & a in A & o in O by GROUP_2:12;
      set Q = a * O;
A3:   Q is open by A1,Th50;
A4:   Q c= A * O
      proof
        let q be set;
        assume q in Q;
        then consider h being Element of G such that
A5:       q = a * h & h in O by GROUP_2:33;
        thus thesis by A2,A5,GROUP_2:12;
      end;
        x in Q by A2,GROUP_2:33;
      hence x in Int (A * O) by A3,A4,TOPS_1:54;
    end;
    hence A * O is open;
  end;

definition let G be BinContinuous TopGroup,
               A be open Subset of G,
               B be Subset of G;
 cluster A * B -> open;
coherence by Th52;
 cluster B * A -> open;
coherence by Th53;
end;

theorem Th54:
 for G being UnContinuous TopGroup,
     a being Point of G, A being a_neighborhood of a
  holds A" is a_neighborhood of a"
  proof
    let G be UnContinuous TopGroup,
        a be Point of G,
        A be a_neighborhood of a;
      a in Int A by CONNSP_2:def 1;
    then consider Q being Subset of G such that
A1:   Q is open & Q c= A & a in Q by TOPS_1:54;
      Q" is open & Q" c= A" & a" in Q" by A1,Th9,Th51,GROUP_2:5;
    hence a" in Int (A") by TOPS_1:54;
  end;

theorem Th55:
 for G being TopologicalGroup, a being Point of G,
     A being a_neighborhood of a*a"
  ex B being open a_neighborhood of a st B*B" c= A
  proof
    let G be TopologicalGroup,
        a be Point of G,
        A be a_neighborhood of a*a";
    consider X, Y being open a_neighborhood of a such that
A1:   X*Y" c= A by Th41;
    reconsider B = X /\ Y as open a_neighborhood of a by CONNSP_2:4,TOPS_1:38;
    take B;
    let x be set;
    assume x in B*B";
    then consider g, h being Point of G such that
A2:   x = g*h & g in B & h in B" by GROUP_2:12;
      h" in B by A2,Th7;
    then h" in Y by XBOOLE_0:def 3;
    then g in X & h in Y" by A2,Th7,XBOOLE_0:def 3;
    then x in X*Y" by A2,GROUP_2:12;
    hence x in A by A1;
  end;

theorem Th56:
 for G being UnContinuous TopGroup, A being dense Subset of G holds
  A" is dense
  proof
    let G be UnContinuous TopGroup,
        A be dense Subset of G;
      (inverse_op G)"A = A" by Th11;
    hence A" is dense by Th29;
  end;

definition let G be UnContinuous TopGroup,
               A be dense Subset of G;
 cluster A" -> dense;
coherence by Th56;
end;

theorem Th57:
 for G being BinContinuous TopGroup, A being dense Subset of G,
     a being Point of G holds a*A is dense
  proof
    let G be BinContinuous TopGroup,
        A be dense Subset of G,
        a be Point of G;
      (a*).:A = a*A by Th16;
    hence a*A is dense by Th28;
  end;

theorem Th58:
 for G being BinContinuous TopGroup, A being dense Subset of G,
     a being Point of G holds A*a is dense
  proof
    let G be BinContinuous TopGroup,
        A be dense Subset of G,
        a be Point of G;
      (*a).:A = A*a by Th17;
    hence A*a is dense by Th28;
  end;

definition let G be BinContinuous TopGroup,
               A be dense Subset of G,
               a be Point of G;
 cluster A * a -> dense;
coherence by Th58;
 cluster a * A -> dense;
coherence by Th57;
end;

theorem
   for G being TopologicalGroup, B being Basis of 1.G, M being dense Subset of
G
  holds
{ V * x where V is Subset of G, x is Point of G: V in B & x in
 M }
  is Basis of G
  proof
    let G be TopologicalGroup,
        B be Basis of 1.G,
        M be dense Subset of G;
    set Z = { V * x where V is Subset of G,
              x is Point of G: V in B & x in M };
   Z c= bool the carrier of G
    proof
      let a be set;
      assume a in Z;
      then consider V being Subset of G,
               x being Point of G such that
A1:     a = V*x and V in B & x in M;
      thus thesis by A1;
    end;
    then Z is Subset-Family of G by SETFAM_1:def 7;
then A2:  Z is Subset-Family of G;
A3: Z c= the topology of G
    proof
      let a be set;
      assume a in Z;
      then consider V being Subset of G,
               x being Point of G such that
A4:     a = V*x & V in B & x in M;
      reconsider V as Subset of G;
        V is open by A4,YELLOW_8:21;
      then V*x is open by Th49;
      hence thesis by A4,PRE_TOPC:def 5;
    end;
      for W being Subset of G st W is open
     for a being Point of G st a in W
      ex V being Subset of G st V in Z & a in V & V c= W
    proof
      let W be Subset of G such that
A5:     W is open;
      let a be Point of G such that
A6:     a in W;
A7:   W*a" is open by A5,Th49;
A8:   1.G*(1.G)" = 1.G*1.G by GROUP_1:16
                .= 1.G by GROUP_1:def 4;
        1.G = a*a" by GROUP_1:def 5;
      then 1.G in W*a" by A6,GROUP_2:34;
      then W*a" is a_neighborhood of 1.G*(1.G)" by A7,A8,CONNSP_2:5;
      then consider V being open a_neighborhood of 1.G such that
A9:     V*V" c= W*a" by Th55;
        1.G in V by CONNSP_2:6;
      then consider E being Subset of G such that
A10:     E in B & E c= V by YELLOW_8:22;
     E is open & E <> {} by A10,YELLOW_8:21;
      then (a*M") meets E by TOPS_1:80;
      then consider d being set such that
A11:     d in (a*M") /\ E by XBOOLE_0:4;
      reconsider d as Point of G by A11;
      take I = E*(d"*a);
A12:   d in E & d in a*M" by A11,XBOOLE_0:def 3;
      then consider m being Point of G such that
A13:     d = a*m & m in M" by GROUP_2:33;
        d"*a = d"*a*1.G by GROUP_1:def 4
          .= d"*a*(m*m") by GROUP_1:def 5
          .= d"*a*m*m" by VECTSP_1:def 16
          .= d"*d*m" by A13,VECTSP_1:def 16
          .= 1.G*m" by GROUP_1:def 5
          .= m" by GROUP_1:def 4;
      then d"*a in M by A13,Th7;
      hence I in Z by A10;
        d*d" = 1.G by GROUP_1:def 5;
then A14:   1.G in E*d" by A12,GROUP_2:34;
        1.G*a = a by GROUP_1:def 4;
      then a in E*d"*a by A14,GROUP_2:34;
      hence a in I by GROUP_2:40;
        E*d" c= V*V"
      proof
        let q be set;
        assume q in E*d";
        then consider v being Point of G such that
A15:       q = v*d" & v in E by GROUP_2:34;
          d" in V" by A10,A12,GROUP_2:5;
        hence q in V*V" by A10,A15,GROUP_2:12;
      end;
      then E*d" c= W*a" by A9,XBOOLE_1:1;
then A16:   E*d"*a c= W*a"*a by Th5;
        W*a"*a = W*(a"*a) by GROUP_2:40
            .= W*1.G by GROUP_1:def 5
            .= W by GROUP_2:43;
      hence I c= W by A16,GROUP_2:40;
    end;
    hence thesis by A2,A3,YELLOW_9:32;
  end;

theorem Th60:
 for G being TopologicalGroup holds G is_T3
  proof
    let G be TopologicalGroup;
      ex p being Point of G st for A being Subset of G
     st A is open & p in A holds ex B being Subset of G
      st p in B & B is open & Cl B c= A
    proof
      set e = 1.G;
      take e;
      let A be Subset of G; assume
       A is open & e in A;
      then e in Int A by TOPS_1:55;
then A1:   A is a_neighborhood of e by CONNSP_2:def 1;
        e = e*e" by GROUP_1:def 5;
      then consider C being open a_neighborhood of e,
               B being open a_neighborhood of e" such that
A2:     C*B c= A by A1,Th37;
        e"" = e by GROUP_1:19;
      then B" is a_neighborhood of e by Th54;
      then reconsider W = C /\ (B") as a_neighborhood of e by CONNSP_2:4;
      take W;
A3:   W is open by TOPS_1:38;
      then Int W = W by TOPS_1:55;
      hence
A4:     e in W & W is open by CONNSP_2:def 1;
      let p be set; assume
A5:     p in Cl W;
      then reconsider r = p as Point of G;
A6:   r*W is open by A3,Th50;
        r = r*e by GROUP_1:def 4;
      then p in r*W by A4,GROUP_2:33;
      then (r*W) meets W by A5,A6,PRE_TOPC:def 13;
      then consider a being set such that
A7:     a in (r*W) /\ W by XBOOLE_0:4;
A8:   a in r*W & a in W by A7,XBOOLE_0:def 3;
      reconsider a as Point of G by A7;
      consider b being Element of G such that
A9:     a = r * b & b in W by A8,GROUP_2:33;
        W c= B" by XBOOLE_1:17;
      then W" c= B"" by Th9;
      then W" c= B by Th8;
      then C*W" c= C*B by Th4;
then A10:   C*W" c= A by A2,XBOOLE_1:1;
A11:   r = r * e by GROUP_1:def 4
       .= r * (b * b") by GROUP_1:def 5
       .= a * (b") by A9,VECTSP_1:def 16;
A12:   W c= C by XBOOLE_1:17;
        b" in W" by A9,GROUP_2:5;
      then p in C * W" by A8,A11,A12,GROUP_2:12;
      hence p in A by A10;
    end;
    hence thesis by Th36;
  end;

definition
 cluster -> being_T3 TopologicalGroup;
coherence by Th60;
end;


Back to top