:: TOPGRP_1 semantic presentation begin registration let X be set ; cluster Relation-like X -defined X -valued Function-like one-to-one V14(X) quasi_total onto for Element of bool [:X,X:]; existence ex b1 being Function of X,X st ( b1 is one-to-one & b1 is onto ) proof take id X ; ::_thesis: ( id X is one-to-one & id X is onto ) thus id X is one-to-one ; ::_thesis: id X is onto thus rng (id X) = X by RELAT_1:45; :: according to FUNCT_2:def_3 ::_thesis: verum end; end; theorem :: TOPGRP_1:1 for S being 1-sorted holds rng (id S) = [#] S by RELAT_1:45; registration let R be 1-sorted ; cluster(id R) /" -> one-to-one ; coherence (id R) /" is one-to-one proof rng (id R) = [#] R by RELAT_1:45; hence (id R) /" is one-to-one by TOPS_2:50; ::_thesis: verum end; end; theorem Th2: :: TOPGRP_1:2 for R being 1-sorted holds (id R) /" = id R proof let R be 1-sorted ; ::_thesis: (id R) /" = id R rng (id R) = [#] R by RELAT_1:45; then id R is onto by FUNCT_2:def_3; hence (id R) /" = (id the carrier of R) " by TOPS_2:def_4 .= id R by FUNCT_1:45 ; ::_thesis: verum end; theorem :: TOPGRP_1:3 for R being 1-sorted for X being Subset of R holds (id R) " X = X proof let R be 1-sorted ; ::_thesis: for X being Subset of R holds (id R) " X = X let X be Subset of R; ::_thesis: (id R) " X = X rng (id R) = [#] R by RELAT_1:45; then A1: (id R) .: X = ((id R) /") " X by TOPS_2:54; (id R) /" = id R by Th2; hence (id R) " X = X by A1, FUNCT_1:92; ::_thesis: verum end; begin theorem Th4: :: TOPGRP_1:4 for H being non empty multMagma for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds P * Q c= P1 * Q1 proof let H be non empty multMagma ; ::_thesis: for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds P * Q c= P1 * Q1 let P, P1, Q, Q1 be Subset of H; ::_thesis: ( P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1 ) assume A1: ( P c= P1 & Q c= Q1 ) ; ::_thesis: P * Q c= P1 * Q1 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * Q or x in P1 * Q1 ) assume x in P * Q ; ::_thesis: x in P1 * Q1 then ex g, t being Element of H st ( x = g * t & g in P & t in Q ) ; hence x in P1 * Q1 by A1; ::_thesis: verum end; theorem Th5: :: TOPGRP_1:5 for H being non empty multMagma for P, Q being Subset of H for h being Element of H st P c= Q holds P * h c= Q * h proof let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H for h being Element of H st P c= Q holds P * h c= Q * h let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds P * h c= Q * h let h be Element of H; ::_thesis: ( P c= Q implies P * h c= Q * h ) assume A1: P c= Q ; ::_thesis: P * h c= Q * h let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * h or x in Q * h ) assume x in P * h ; ::_thesis: x in Q * h then ex g being Element of H st ( x = g * h & g in P ) by GROUP_2:28; hence x in Q * h by A1, GROUP_2:28; ::_thesis: verum end; theorem :: TOPGRP_1:6 for H being non empty multMagma for P, Q being Subset of H for h being Element of H st P c= Q holds h * P c= h * Q proof let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H for h being Element of H st P c= Q holds h * P c= h * Q let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds h * P c= h * Q let h be Element of H; ::_thesis: ( P c= Q implies h * P c= h * Q ) assume A1: P c= Q ; ::_thesis: h * P c= h * Q let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h * P or x in h * Q ) assume x in h * P ; ::_thesis: x in h * Q then ex g being Element of H st ( x = h * g & g in P ) by GROUP_2:27; hence x in h * Q by A1, GROUP_2:27; ::_thesis: verum end; theorem Th7: :: TOPGRP_1:7 for G being Group for A being Subset of G for a being Element of G holds ( a in A " iff a " in A ) proof let G be Group; ::_thesis: for A being Subset of G for a being Element of G holds ( a in A " iff a " in A ) let A be Subset of G; ::_thesis: for a being Element of G holds ( a in A " iff a " in A ) let a be Element of G; ::_thesis: ( a in A " iff a " in A ) ( (a ") " = a & (A ") " = A ) ; hence ( a in A " iff a " in A ) ; ::_thesis: verum end; Lm1: for G being Group for A, B being Subset of G st A c= B holds A " c= B " proof let G be Group; ::_thesis: for A, B being Subset of G st A c= B holds A " c= B " let A, B be Subset of G; ::_thesis: ( A c= B implies A " c= B " ) assume A1: A c= B ; ::_thesis: A " c= B " let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A " or a in B " ) assume a in A " ; ::_thesis: a in B " then ex g being Element of G st ( a = g " & g in A ) ; hence a in B " by A1; ::_thesis: verum end; theorem :: TOPGRP_1:8 canceled; theorem Th9: :: TOPGRP_1:9 for G being Group for A, B being Subset of G holds ( A c= B iff A " c= B " ) proof let G be Group; ::_thesis: for A, B being Subset of G holds ( A c= B iff A " c= B " ) let A, B be Subset of G; ::_thesis: ( A c= B iff A " c= B " ) ( (A ") " = A & (B ") " = B ) ; hence ( A c= B iff A " c= B " ) by Lm1; ::_thesis: verum end; theorem Th10: :: TOPGRP_1:10 for G being Group for A being Subset of G holds (inverse_op G) .: A = A " proof let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) .: A = A " let A be Subset of G; ::_thesis: (inverse_op G) .: A = A " set f = inverse_op G; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) .: A let y be set ; ::_thesis: ( y in (inverse_op G) .: A implies y in A " ) assume y in (inverse_op G) .: A ; ::_thesis: y in A " then consider x being set such that A1: x in the carrier of G and A2: x in A and A3: y = (inverse_op G) . x by FUNCT_2:64; reconsider x = x as Element of G by A1; y = x " by A3, GROUP_1:def_6; hence y in A " by A2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A " or y in (inverse_op G) .: A ) assume y in A " ; ::_thesis: y in (inverse_op G) .: A then consider g being Element of G such that A4: ( y = g " & g in A ) ; (inverse_op G) . g = g " by GROUP_1:def_6; hence y in (inverse_op G) .: A by A4, FUNCT_2:35; ::_thesis: verum end; theorem Th11: :: TOPGRP_1:11 for G being Group for A being Subset of G holds (inverse_op G) " A = A " proof let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) " A = A " let A be Subset of G; ::_thesis: (inverse_op G) " A = A " set f = inverse_op G; A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) " A let x be set ; ::_thesis: ( x in (inverse_op G) " A implies x in A " ) assume A2: x in (inverse_op G) " A ; ::_thesis: x in A " then reconsider g = x as Element of G ; (inverse_op G) . x in A by A2, FUNCT_1:def_7; then ((inverse_op G) . g) " in A " ; then (g ") " in A " by GROUP_1:def_6; hence x in A " ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in (inverse_op G) " A ) assume x in A " ; ::_thesis: x in (inverse_op G) " A then consider g being Element of G such that A3: ( x = g " & g in A ) ; (inverse_op G) . (g ") = (g ") " by GROUP_1:def_6 .= g ; hence x in (inverse_op G) " A by A1, A3, FUNCT_1:def_7; ::_thesis: verum end; theorem Th12: :: TOPGRP_1:12 for G being Group holds inverse_op G is one-to-one proof let G be Group; ::_thesis: inverse_op G is one-to-one set f = inverse_op G; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (inverse_op G) or not x2 in dom (inverse_op G) or not (inverse_op G) . x1 = (inverse_op G) . x2 or x1 = x2 ) assume that A1: ( x1 in dom (inverse_op G) & x2 in dom (inverse_op G) ) and A2: (inverse_op G) . x1 = (inverse_op G) . x2 ; ::_thesis: x1 = x2 reconsider a = x1, b = x2 as Element of G by A1; ( (inverse_op G) . a = a " & (inverse_op G) . b = b " ) by GROUP_1:def_6; hence x1 = x2 by A2, GROUP_1:9; ::_thesis: verum end; theorem Th13: :: TOPGRP_1:13 for G being Group holds rng (inverse_op G) = the carrier of G proof let G be Group; ::_thesis: rng (inverse_op G) = the carrier of G set f = inverse_op G; thus rng (inverse_op G) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (inverse_op G) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in rng (inverse_op G) ) A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1; assume x in the carrier of G ; ::_thesis: x in rng (inverse_op G) then reconsider a = x as Element of G ; (inverse_op G) . (a ") = (a ") " by GROUP_1:def_6 .= a ; hence x in rng (inverse_op G) by A1, FUNCT_1:def_3; ::_thesis: verum end; registration let G be Group; cluster inverse_op G -> one-to-one onto ; coherence ( inverse_op G is one-to-one & inverse_op G is onto ) proof thus inverse_op G is one-to-one by Th12; ::_thesis: inverse_op G is onto thus rng (inverse_op G) = the carrier of G by Th13; :: according to FUNCT_2:def_3 ::_thesis: verum end; end; theorem Th14: :: TOPGRP_1:14 for G being Group holds (inverse_op G) " = inverse_op G proof let G be Group; ::_thesis: (inverse_op G) " = inverse_op G set f = inverse_op G; A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(inverse_op_G)_holds_ (inverse_op_G)_._x_=_((inverse_op_G)_")_._x let x be set ; ::_thesis: ( x in dom (inverse_op G) implies (inverse_op G) . x = ((inverse_op G) ") . x ) assume x in dom (inverse_op G) ; ::_thesis: (inverse_op G) . x = ((inverse_op G) ") . x then reconsider g = x as Element of G ; A3: (inverse_op G) . (g ") = (g ") " by GROUP_1:def_6 .= g ; thus (inverse_op G) . x = g " by GROUP_1:def_6 .= ((inverse_op G) ") . x by A1, A3, FUNCT_1:32 ; ::_thesis: verum end; dom ((inverse_op G) ") = the carrier of G by FUNCT_2:def_1; hence (inverse_op G) " = inverse_op G by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem Th15: :: TOPGRP_1:15 for H being non empty multMagma for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q proof let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q let P, Q be Subset of H; ::_thesis: the multF of H .: [:P,Q:] = P * Q set f = the multF of H; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * Q c= the multF of H .: [:P,Q:] let y be set ; ::_thesis: ( y in the multF of H .: [:P,Q:] implies y in P * Q ) assume y in the multF of H .: [:P,Q:] ; ::_thesis: y in P * Q then consider x being set such that x in [: the carrier of H, the carrier of H:] and A1: x in [:P,Q:] and A2: y = the multF of H . x by FUNCT_2:64; consider a, b being set such that A3: ( a in P & b in Q ) and A4: x = [a,b] by A1, ZFMISC_1:def_2; reconsider a = a, b = b as Element of H by A3; y = a * b by A2, A4; hence y in P * Q by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * Q or y in the multF of H .: [:P,Q:] ) assume y in P * Q ; ::_thesis: y in the multF of H .: [:P,Q:] then consider g, h being Element of H such that A5: y = g * h and A6: ( g in P & h in Q ) ; [g,h] in [:P,Q:] by A6, ZFMISC_1:87; hence y in the multF of H .: [:P,Q:] by A5, FUNCT_2:35; ::_thesis: verum end; definition let G be non empty multMagma ; let a be Element of G; funca * -> Function of G,G means :Def1: :: TOPGRP_1:def 1 for x being Element of G holds it . x = a * x; existence ex b1 being Function of G,G st for x being Element of G holds b1 . x = a * x proof deffunc H1( Element of G) -> Element of the carrier 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 = H1(x) from FUNCT_2:sch_4(); reconsider f = f as Function of G,G ; take f ; ::_thesis: for x being Element of G holds f . x = a * x thus for x being Element of G holds f . x = a * x by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = a * x ) & ( for x being Element of G holds b2 . x = a * x ) holds b1 = b2 proof let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = a * x ) & ( for x being Element of G holds g . x = a * x ) implies f = g ) assume 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 ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x ) assume x in the carrier of G ; ::_thesis: f . x = g . x then reconsider y = x as Element of G ; thus f . x = a * y by A2 .= g . x by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:12; ::_thesis: verum end; func * a -> Function of G,G means :Def2: :: TOPGRP_1:def 2 for x being Element of G holds it . x = x * a; existence ex b1 being Function of G,G st for x being Element of G holds b1 . x = x * a proof deffunc H1( Element of G) -> Element of the carrier 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 = H1(x) from FUNCT_2:sch_4(); reconsider f = f as Function of G,G ; take f ; ::_thesis: for x being Element of G holds f . x = x * a thus for x being Element of G holds f . x = x * a by A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = x * a ) & ( for x being Element of G holds b2 . x = x * a ) holds b1 = b2 proof let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = x * a ) & ( for x being Element of G holds g . x = x * a ) implies f = g ) assume 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 ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x ) assume x in the carrier of G ; ::_thesis: f . x = g . x then reconsider y = x as Element of G ; thus f . x = y * a by A5 .= g . x by A6 ; ::_thesis: verum end; hence f = g by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines * TOPGRP_1:def_1_:_ for G being non empty multMagma for a being Element of G for b3 being Function of G,G holds ( b3 = a * iff for x being Element of G holds b3 . x = a * x ); :: deftheorem Def2 defines * TOPGRP_1:def_2_:_ for G being non empty multMagma for a being Element of G for b3 being Function of G,G holds ( b3 = * a iff for x being Element of G holds b3 . x = x * a ); registration let G be Group; let a be Element of G; clustera * -> one-to-one onto ; coherence ( a * is one-to-one & a * is onto ) proof set f = a * ; A1: dom (a *) = the carrier of G by FUNCT_2:def_1; hereby :: according to FUNCT_1:def_4 ::_thesis: a * is onto let x1, x2 be set ; ::_thesis: ( x1 in dom (a *) & x2 in dom (a *) & (a *) . x1 = (a *) . x2 implies x1 = x2 ) assume that A2: ( x1 in dom (a *) & x2 in dom (a *) ) and A3: (a *) . x1 = (a *) . x2 ; ::_thesis: x1 = x2 reconsider y1 = x1, y2 = x2 as Element of G by A2; A4: ( (a *) . y1 = a * y1 & (a *) . 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 GROUP_1:def_3 .= ((a ") * a) * y2 by A3, A4, GROUP_1:def_3 .= (1_ G) * y2 by GROUP_1:def_5 .= x2 by GROUP_1:def_4 ; ::_thesis: verum end; thus rng (a *) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (a *) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (a *) ) assume y in the carrier of G ; ::_thesis: y in rng (a *) then reconsider y1 = y as Element of G ; (a *) . ((a ") * y1) = a * ((a ") * y1) by Def1 .= (a * (a ")) * y1 by GROUP_1:def_3 .= (1_ G) * y1 by GROUP_1:def_5 .= y by GROUP_1:def_4 ; hence y in rng (a *) by A1, FUNCT_1:def_3; ::_thesis: verum end; cluster * a -> one-to-one onto ; coherence ( * a is one-to-one & * a is onto ) proof set f = * a; A5: dom (* a) = the carrier of G by FUNCT_2:def_1; hereby :: according to FUNCT_1:def_4 ::_thesis: * a is onto let x1, x2 be set ; ::_thesis: ( x1 in dom (* a) & x2 in dom (* a) & (* a) . x1 = (* a) . x2 implies x1 = x2 ) assume that A6: ( x1 in dom (* a) & x2 in dom (* a) ) and A7: (* a) . x1 = (* a) . x2 ; ::_thesis: x1 = x2 reconsider y1 = x1, y2 = x2 as Element of G by A6; A8: ( (* a) . y1 = y1 * a & (* a) . 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 GROUP_1:def_3 .= y2 * (a * (a ")) by A7, A8, GROUP_1:def_3 .= y2 * (1_ G) by GROUP_1:def_5 .= x2 by GROUP_1:def_4 ; ::_thesis: verum end; thus rng (* a) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (* a) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (* a) ) assume y in the carrier of G ; ::_thesis: y in rng (* a) then reconsider y1 = y as Element of G ; (* a) . (y1 * (a ")) = (y1 * (a ")) * a by Def2 .= y1 * ((a ") * a) by GROUP_1:def_3 .= y1 * (1_ G) by GROUP_1:def_5 .= y by GROUP_1:def_4 ; hence y in rng (* a) by A5, FUNCT_1:def_3; ::_thesis: verum end; end; theorem Th16: :: TOPGRP_1:16 for H being non empty multMagma for P being Subset of H for h being Element of H holds (h *) .: P = h * P proof let H be non empty multMagma ; ::_thesis: for P being Subset of H for h being Element of H holds (h *) .: P = h * P let P be Subset of H; ::_thesis: for h being Element of H holds (h *) .: P = h * P let h be Element of H; ::_thesis: (h *) .: P = h * P set f = h * ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: h * P c= (h *) .: P let y be set ; ::_thesis: ( y in (h *) .: P implies y in h * P ) assume y in (h *) .: P ; ::_thesis: y in h * P then consider x being set such that A1: x in dom (h *) and A2: ( x in P & y = (h *) . x ) by FUNCT_1:def_6; reconsider x = x as Element of H by A1; (h *) . x = h * x by Def1; hence y in h * P by A2, GROUP_2:27; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in h * P or y in (h *) .: P ) assume y in h * P ; ::_thesis: y in (h *) .: P then consider s being Element of H such that A3: ( y = h * s & s in P ) by GROUP_2:27; ( dom (h *) = the carrier of H & (h *) . s = h * s ) by Def1, FUNCT_2:def_1; hence y in (h *) .: P by A3, FUNCT_1:def_6; ::_thesis: verum end; theorem Th17: :: TOPGRP_1:17 for H being non empty multMagma for P being Subset of H for h being Element of H holds (* h) .: P = P * h proof let H be non empty multMagma ; ::_thesis: for P being Subset of H for h being Element of H holds (* h) .: P = P * h let P be Subset of H; ::_thesis: for h being Element of H holds (* h) .: P = P * h let h be Element of H; ::_thesis: (* h) .: P = P * h set f = * h; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * h c= (* h) .: P let y be set ; ::_thesis: ( y in (* h) .: P implies y in P * h ) assume y in (* h) .: P ; ::_thesis: y in P * h then consider x being set such that A1: x in dom (* h) and A2: ( x in P & y = (* h) . x ) by FUNCT_1:def_6; reconsider x = x as Element of H by A1; (* h) . x = x * h by Def2; hence y in P * h by A2, GROUP_2:28; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * h or y in (* h) .: P ) assume y in P * h ; ::_thesis: y in (* h) .: P then consider s being Element of H such that A3: ( y = s * h & s in P ) by GROUP_2:28; ( dom (* h) = the carrier of H & (* h) . s = s * h ) by Def2, FUNCT_2:def_1; hence y in (* h) .: P by A3, FUNCT_1:def_6; ::_thesis: verum end; theorem Th18: :: TOPGRP_1:18 for G being Group for a being Element of G holds (a *) /" = (a ") * proof let G be Group; ::_thesis: for a being Element of G holds (a *) /" = (a ") * let a be Element of G; ::_thesis: (a *) /" = (a ") * set f = a * ; set g = (a ") * ; A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_ ((a_*)_/")_._y_=_((a_")_*)_._y reconsider h = a * as Function ; let y be set ; ::_thesis: ( y in the carrier of G implies ((a *) /") . y = ((a ") *) . y ) assume y in the carrier of G ; ::_thesis: ((a *) /") . y = ((a ") *) . y then reconsider y1 = y as Element of G ; rng (a *) = the carrier of G by FUNCT_2:def_3; then A2: y1 in rng (a *) ; dom (a *) = the carrier of G by FUNCT_2:def_1; then A3: ( ((a ") *) . y1 in dom (a *) & ((a *) /") . y1 in dom (a *) ) ; (a *) . (((a ") *) . y) = a * (((a ") *) . y1) by Def1 .= a * ((a ") * y1) by Def1 .= (a * (a ")) * y1 by GROUP_1:def_3 .= (1_ G) * y1 by GROUP_1:def_5 .= y by GROUP_1:def_4 .= h . ((h ") . y) by A2, FUNCT_1:35 .= (a *) . (((a *) /") . y) by TOPS_2:def_4 ; hence ((a *) /") . y = ((a ") *) . y by A3, FUNCT_1:def_4; ::_thesis: verum end; ( dom ((a *) /") = the carrier of G & dom ((a ") *) = the carrier of G ) by FUNCT_2:def_1; hence (a *) /" = (a ") * by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th19: :: TOPGRP_1:19 for G being Group for a being Element of G holds (* a) /" = * (a ") proof let G be Group; ::_thesis: for a being Element of G holds (* a) /" = * (a ") let a be Element of G; ::_thesis: (* a) /" = * (a ") set f = * a; set g = * (a "); A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_ ((*_a)_/")_._y_=_(*_(a_"))_._y reconsider h = * a as Function ; let y be set ; ::_thesis: ( y in the carrier of G implies ((* a) /") . y = (* (a ")) . y ) assume y in the carrier of G ; ::_thesis: ((* a) /") . y = (* (a ")) . y then reconsider y1 = y as Element of G ; rng (* a) = the carrier of G by FUNCT_2:def_3; then A2: y1 in rng (* a) ; dom (* a) = the carrier of G by FUNCT_2:def_1; then A3: ( (* (a ")) . y1 in dom (* a) & ((* a) /") . y1 in dom (* a) ) ; (* a) . ((* (a ")) . y) = ((* (a ")) . y1) * a by Def2 .= (y1 * (a ")) * a by Def2 .= y1 * ((a ") * a) by GROUP_1:def_3 .= y1 * (1_ G) by GROUP_1:def_5 .= y by GROUP_1:def_4 .= h . ((h ") . y) by A2, FUNCT_1:35 .= (* a) . (((* a) /") . y) by TOPS_2:def_4 ; hence ((* a) /") . y = (* (a ")) . y by A3, FUNCT_1:def_4; ::_thesis: verum end; ( dom ((* a) /") = the carrier of G & dom (* (a ")) = the carrier of G ) by FUNCT_2:def_1; hence (* a) /" = * (a ") by A1, FUNCT_1:2; ::_thesis: verum end; begin registration let T be TopStruct ; cluster(id T) /" -> continuous ; coherence (id T) /" is continuous by Th2; end; theorem Th20: :: TOPGRP_1:20 for T being TopStruct holds id T is being_homeomorphism proof let T be TopStruct ; ::_thesis: id T is being_homeomorphism thus ( dom (id T) = [#] T & rng (id T) = [#] T ) by RELAT_1:45; :: according to TOPS_2:def_5 ::_thesis: ( id T is one-to-one & id T is continuous & (id T) /" is continuous ) thus ( id T is one-to-one & id T is continuous & (id T) /" is continuous ) ; ::_thesis: verum end; registration let T be non empty TopSpace; let p be Point of T; cluster -> non empty for a_neighborhood of p; coherence for b1 being a_neighborhood of p holds not b1 is empty proof let N be a_neighborhood of p; ::_thesis: not N is empty p in Int N by CONNSP_2:def_1; hence not N is empty ; ::_thesis: verum end; end; theorem Th21: :: TOPGRP_1:21 for T being non empty TopSpace for p being Point of T holds [#] T is a_neighborhood of p proof let T be non empty TopSpace; ::_thesis: for p being Point of T holds [#] T is a_neighborhood of p let p be Point of T; ::_thesis: [#] T is a_neighborhood of p Int ([#] T) = the carrier of T by TOPS_1:15; hence p in Int ([#] T) ; :: according to CONNSP_2:def_1 ::_thesis: verum end; registration let T be non empty TopSpace; let p be Point of T; cluster non empty open for a_neighborhood of p; existence ex b1 being a_neighborhood of p st ( not b1 is empty & b1 is open ) proof reconsider B = [#] T as a_neighborhood of p by Th21; take B ; ::_thesis: ( not B is empty & B is open ) thus ( not B is empty & B is open ) ; ::_thesis: verum end; end; theorem :: TOPGRP_1:22 for S, T being non empty TopSpace for f being Function of S,T st f is open holds for p being Point of S for 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; ::_thesis: for f being Function of S,T st f is open holds for p being Point of S for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P let f be Function of S,T; ::_thesis: ( f is open implies for p being Point of S for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P ) assume A1: for A being Subset of S st A is open holds f .: A is open ; :: according to T_0TOPSP:def_2 ::_thesis: for p being Point of S for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P let p be Point of S; ::_thesis: for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P let P be a_neighborhood of p; ::_thesis: ex R being open a_neighborhood of f . p st R c= f .: P A2: p in Int P by CONNSP_2:def_1; f .: (Int P) is open by A1; then reconsider R = f .: (Int P) as open a_neighborhood of f . p by A2, CONNSP_2:3, FUNCT_2:35; take R ; ::_thesis: R c= f .: P thus R c= f .: P by RELAT_1:123, TOPS_1:16; ::_thesis: verum end; theorem :: TOPGRP_1:23 for S, T being non empty TopSpace for f being Function of S,T st ( for p being Point of S for 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; ::_thesis: for f being Function of S,T st ( for p being Point of S for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) holds f is open let f be Function of S,T; ::_thesis: ( ( for p being Point of S for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) implies f is open ) assume A1: for p being Point of S for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ; ::_thesis: f is open let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open ) assume A2: A is open ; ::_thesis: f .: 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 ; ::_thesis: ( x in f .: A iff ex Q being Subset of T st ( Q is open & Q c= f .: A & x in Q ) ) hereby ::_thesis: ( ex Q being Subset of T st ( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) assume x in f .: A ; ::_thesis: ex K being Element of bool the carrier of T st ( K is open & K c= f .: A & x in K ) then consider a being set such that A3: a in dom f and A4: a in A and A5: x = f . a by FUNCT_1:def_6; reconsider p = a as Point of S by A3; consider V being Subset of S such that A6: V is open and A7: V c= A and A8: a in V by A2, A4; V is a_neighborhood of p by A6, A8, CONNSP_2:3; then consider R being a_neighborhood of f . p such that A9: R c= f .: V by A1, A6; take K = Int R; ::_thesis: ( K is open & K c= f .: A & x in K ) Int R c= R by TOPS_1:16; then A10: K c= f .: V by A9, XBOOLE_1:1; thus K is open ; ::_thesis: ( K c= f .: A & x in K ) f .: V c= f .: A by A7, RELAT_1:123; hence K c= f .: A by A10, XBOOLE_1:1; ::_thesis: x in K thus x in K by A5, CONNSP_2:def_1; ::_thesis: verum end; thus ( ex Q being Subset of T st ( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; ::_thesis: verum end; hence f .: A is open by TOPS_1:25; ::_thesis: verum end; theorem :: TOPGRP_1:24 for S, T being non empty TopStruct for f being Function of S,T holds ( f is being_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 ; ::_thesis: for f being Function of S,T holds ( f is being_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 ) ) ) ) let f be Function of S,T; ::_thesis: ( f is being_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 ) ) ) ) hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds ( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) ) ) ) hence A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds ( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) ) let P be Subset of T; ::_thesis: ( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) ) hereby ::_thesis: ( f " P is closed implies P is closed ) assume A3: P is closed ; ::_thesis: f " P is closed f is continuous by A1, TOPS_2:def_5; hence f " P is closed by A3, PRE_TOPC:def_6; ::_thesis: verum end; assume f " P is closed ; ::_thesis: P is closed then f .: (f " P) is closed by A1, TOPS_2:58; hence P is closed by A2, FUNCT_1:77; ::_thesis: verum end; assume that A4: dom f = [#] S and A5: rng f = [#] T and A6: f is one-to-one and A7: for P being Subset of T holds ( P is closed iff f " P is closed ) ; ::_thesis: f is being_homeomorphism thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A4, A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous ) thus f is continuous ::_thesis: f /" is continuous proof let P be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or f " P is closed ) thus ( not P is closed or f " P is closed ) by A7; ::_thesis: verum end; let R be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not R is closed or (f /") " R is closed ) assume A8: R is closed ; ::_thesis: (f /") " R is closed for x1, x2 being Element of S st x1 in R & f . x1 = f . x2 holds x2 in R by A4, A6, FUNCT_1:def_4; then A9: f " (f .: R) = R by T_0TOPSP:1; (f /") " R = f .: R by A5, A6, TOPS_2:54; hence (f /") " R is closed by A7, A8, A9; ::_thesis: verum end; theorem Th25: :: TOPGRP_1:25 for S, T being non empty TopStruct for f being Function of S,T holds ( f is being_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 ; ::_thesis: for f being Function of S,T holds ( f is being_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 ) ) ) ) let f be Function of S,T; ::_thesis: ( f is being_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 ) ) ) ) A1: [#] T <> {} ; A2: [#] S <> {} ; hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism ) assume A3: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of S holds ( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) ) ) ) hence A4: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of S holds ( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) ) let P be Subset of S; ::_thesis: ( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) ) A5: ( f " (f .: P) c= P & P c= f " (f .: P) ) by A4, FUNCT_1:76, FUNCT_1:82; A6: f /" is continuous by A3, TOPS_2:def_5; hereby ::_thesis: ( f .: P is open implies P is open ) assume A7: P is open ; ::_thesis: f .: P is open f is onto by A4, FUNCT_2:def_3; then (f /") " P = (f ") " P by A4, TOPS_2:def_4 .= f .: P by A4, FUNCT_1:84 ; hence f .: P is open by A2, A6, A7, TOPS_2:43; ::_thesis: verum end; assume A8: f .: P is open ; ::_thesis: P is open f is continuous by A3, TOPS_2:def_5; then f " (f .: P) is open by A1, A8, TOPS_2:43; hence P is open by A5, XBOOLE_0:def_10; ::_thesis: verum end; assume that A9: dom f = [#] S and A10: rng f = [#] T and A11: f is one-to-one and A12: for P being Subset of S holds ( P is open iff f .: P is open ) ; ::_thesis: f is being_homeomorphism now__::_thesis:_for_B_being_Subset_of_T_st_B_is_open_holds_ f_"_B_is_open let B be Subset of T; ::_thesis: ( B is open implies f " B is open ) assume A13: B is open ; ::_thesis: f " B is open B = f .: (f " B) by A10, FUNCT_1:77; hence f " B is open by A12, A13; ::_thesis: verum end; then A14: f is continuous by A1, TOPS_2:43; now__::_thesis:_for_B_being_Subset_of_S_st_B_is_open_holds_ (f_/")_"_B_is_open let B be Subset of S; ::_thesis: ( B is open implies (f /") " B is open ) assume A15: B is open ; ::_thesis: (f /") " B is open f is onto by A10, FUNCT_2:def_3; then (f /") " B = (f ") " B by A11, TOPS_2:def_4 .= f .: B by A11, FUNCT_1:84 ; hence (f /") " B is open by A12, A15; ::_thesis: verum end; then f /" is continuous by A2, TOPS_2:43; hence f is being_homeomorphism by A9, A10, A11, A14, TOPS_2:def_5; ::_thesis: verum end; theorem :: TOPGRP_1:26 for S, T being non empty TopStruct for f being Function of S,T holds ( f is being_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 ; ::_thesis: for f being Function of S,T holds ( f is being_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 ) ) ) ) let f be Function of S,T; ::_thesis: ( f is being_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 ) ) ) ) A1: [#] T <> {} ; hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism ) assume A2: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds ( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) ) ) ) hence A3: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds ( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) ) let P be Subset of T; ::_thesis: ( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) ) hereby ::_thesis: ( f " P is open implies P is open ) assume A4: P is open ; ::_thesis: f " P is open f is continuous by A2, TOPS_2:def_5; hence f " P is open by A1, A4, TOPS_2:43; ::_thesis: verum end; assume f " P is open ; ::_thesis: P is open then f .: (f " P) is open by A2, Th25; hence P is open by A3, FUNCT_1:77; ::_thesis: verum end; assume that A5: dom f = [#] S and A6: rng f = [#] T and A7: f is one-to-one and A8: for P being Subset of T holds ( P is open iff f " P is open ) ; ::_thesis: f is being_homeomorphism A9: now__::_thesis:_for_R_being_Subset_of_S_st_R_is_open_holds_ (f_/")_"_R_is_open let R be Subset of S; ::_thesis: ( R is open implies (f /") " R is open ) assume A10: R is open ; ::_thesis: (f /") " R is open for x1, x2 being Element of S st x1 in R & f . x1 = f . x2 holds x2 in R by A5, A7, FUNCT_1:def_4; then A11: f " (f .: R) = R by T_0TOPSP:1; (f /") " R = f .: R by A6, A7, TOPS_2:54; hence (f /") " R is open by A8, A10, A11; ::_thesis: verum end; thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A5, A6, A7; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous ) thus f is continuous by A1, A8, TOPS_2:43; ::_thesis: f /" is continuous [#] S <> {} ; hence f /" is continuous by A9, TOPS_2:43; ::_thesis: verum end; theorem :: TOPGRP_1:27 for S being TopSpace for T being non empty TopSpace for f being Function 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; ::_thesis: for T being non empty TopSpace for f being Function of S,T holds ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) ) let T be non empty TopSpace; ::_thesis: for f being Function of S,T holds ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) ) let f be Function of S,T; ::_thesis: ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) ) A1: [#] T <> {} ; hereby ::_thesis: ( ( for P being Subset of T holds f " (Int P) c= Int (f " P) ) implies f is continuous ) assume A2: f is continuous ; ::_thesis: for P being Subset of T holds f " (Int P) c= Int (f " P) let P be Subset of T; ::_thesis: f " (Int P) c= Int (f " P) f " (Int P) c= f " P by RELAT_1:143, TOPS_1:16; then A3: Int (f " (Int P)) c= Int (f " P) by TOPS_1:19; f " (Int P) is open by A1, A2, TOPS_2:43; hence f " (Int P) c= Int (f " P) by A3, TOPS_1:23; ::_thesis: verum end; assume A4: for P being Subset of T holds f " (Int P) c= Int (f " P) ; ::_thesis: f is continuous now__::_thesis:_for_P_being_Subset_of_T_st_P_is_open_holds_ f_"_P_is_open let P be Subset of T; ::_thesis: ( P is open implies f " P is open ) assume P is open ; ::_thesis: f " P is open then Int P = P by TOPS_1:23; then A5: f " P c= Int (f " P) by A4; Int (f " P) c= f " P by TOPS_1:16; hence f " P is open by A5, XBOOLE_0:def_10; ::_thesis: verum end; hence f is continuous by A1, TOPS_2:43; ::_thesis: verum end; registration let T be non empty TopSpace; cluster non empty dense for Element of bool the carrier of T; existence ex b1 being Subset of T st ( not b1 is empty & b1 is dense ) proof take [#] T ; ::_thesis: ( not [#] T is empty & [#] T is dense ) thus ( not [#] T is empty & [#] T is dense ) ; ::_thesis: verum end; end; theorem Th28: :: TOPGRP_1:28 for S, T being non empty TopSpace for f being Function of S,T for A being dense Subset of S st f is being_homeomorphism holds f .: A is dense proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T for A being dense Subset of S st f is being_homeomorphism holds f .: A is dense let f be Function of S,T; ::_thesis: for A being dense Subset of S st f is being_homeomorphism holds f .: A is dense let A be dense Subset of S; ::_thesis: ( f is being_homeomorphism implies f .: A is dense ) assume A1: f is being_homeomorphism ; ::_thesis: f .: A is dense A2: rng f = [#] T by A1, TOPS_2:def_5; Cl A = [#] S by TOPS_1:def_3; hence Cl (f .: A) = f .: the carrier of S by A1, TOPS_2:60 .= [#] T by A2, RELSET_1:22 ; :: according to TOPS_1:def_3 ::_thesis: verum end; theorem Th29: :: TOPGRP_1:29 for S, T being non empty TopSpace for f being Function of S,T for A being dense Subset of T st f is being_homeomorphism holds f " A is dense proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T for A being dense Subset of T st f is being_homeomorphism holds f " A is dense let f be Function of S,T; ::_thesis: for A being dense Subset of T st f is being_homeomorphism holds f " A is dense let A be dense Subset of T; ::_thesis: ( f is being_homeomorphism implies f " A is dense ) assume A1: f is being_homeomorphism ; ::_thesis: f " A is dense A2: Cl A = [#] T by TOPS_1:def_3; thus Cl (f " A) = f " (Cl A) by A1, TOPS_2:59 .= [#] S by A2, TOPS_2:41 ; :: according to TOPS_1:def_3 ::_thesis: verum end; registration let S, T be TopStruct ; cluster Function-like quasi_total being_homeomorphism -> one-to-one onto continuous for Element of bool [: the carrier of S, the carrier of T:]; coherence for b1 being Function of S,T st b1 is being_homeomorphism holds ( b1 is onto & b1 is one-to-one & b1 is continuous ) proof let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies ( f is onto & f is one-to-one & f is continuous ) ) assume A1: f is being_homeomorphism ; ::_thesis: ( f is onto & f is one-to-one & f is continuous ) then rng f = [#] T by TOPS_2:def_5; hence rng f = the carrier of T ; :: according to FUNCT_2:def_3 ::_thesis: ( f is one-to-one & f is continuous ) thus ( f is one-to-one & f is continuous ) by A1, TOPS_2:def_5; ::_thesis: verum end; end; registration let S, T be non empty TopStruct ; cluster Function-like quasi_total being_homeomorphism -> open for Element of bool [: the carrier of S, the carrier of T:]; coherence for b1 being Function of S,T st b1 is being_homeomorphism holds b1 is open proof let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f is open ) assume A1: f is being_homeomorphism ; ::_thesis: f is open let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open ) thus ( not A is open or f .: A is open ) by A1, Th25; ::_thesis: verum end; end; registration let T be TopStruct ; cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like V14( the carrier of T) quasi_total being_homeomorphism for Element of bool [: the carrier of T, the carrier of T:]; existence ex b1 being Function of T,T st b1 is being_homeomorphism proof take id T ; ::_thesis: id T is being_homeomorphism thus id T is being_homeomorphism by Th20; ::_thesis: verum end; end; registration let T be TopStruct ; let f be being_homeomorphism Function of T,T; clusterf /" -> being_homeomorphism ; coherence f /" is being_homeomorphism proof percases ( not T is empty or T is empty ) ; suppose not T is empty ; ::_thesis: f /" is being_homeomorphism hence f /" is being_homeomorphism by TOPS_2:56; ::_thesis: verum end; suppose T is empty ; ::_thesis: f /" is being_homeomorphism then A1: the carrier of T is empty ; f /" = f " by TOPS_2:def_4 .= id T by A1, RELAT_1:55 ; hence f /" is being_homeomorphism by Th20; ::_thesis: verum end; end; end; end; begin definition let S, T be TopStruct ; assume A1: S,T are_homeomorphic ; mode Homeomorphism of S,T -> Function of S,T means :Def3: :: TOPGRP_1:def 3 it is being_homeomorphism ; existence ex b1 being Function of S,T st b1 is being_homeomorphism by A1, T_0TOPSP:def_1; end; :: deftheorem Def3 defines Homeomorphism TOPGRP_1:def_3_:_ for S, T being TopStruct st S,T are_homeomorphic holds for b3 being Function of S,T holds ( b3 is Homeomorphism of S,T iff b3 is being_homeomorphism ); definition let T be TopStruct ; mode Homeomorphism of T -> Function of T,T means :Def4: :: TOPGRP_1:def 4 it is being_homeomorphism ; existence ex b1 being Function of T,T st b1 is being_homeomorphism proof A1: id T is being_homeomorphism by Th20; then T,T are_homeomorphic by T_0TOPSP:def_1; then reconsider f = id T as Homeomorphism of T,T by A1, Def3; f is being_homeomorphism by Th20; hence ex b1 being Function of T,T st b1 is being_homeomorphism ; ::_thesis: verum end; end; :: deftheorem Def4 defines Homeomorphism TOPGRP_1:def_4_:_ for T being TopStruct for b2 being Function of T,T holds ( b2 is Homeomorphism of T iff b2 is being_homeomorphism ); definition let T be TopStruct ; :: original: Homeomorphism redefine mode Homeomorphism of T -> Homeomorphism of T,T; coherence for b1 being Homeomorphism of T holds b1 is Homeomorphism of T,T proof let f be Homeomorphism of T; ::_thesis: f is Homeomorphism of T,T A1: f is being_homeomorphism by Def4; then T,T are_homeomorphic by T_0TOPSP:def_1; hence f is Homeomorphism of T,T by A1, Def3; ::_thesis: verum end; end; definition let T be TopStruct ; :: original: id redefine func id T -> Homeomorphism of T,T; coherence id T is Homeomorphism of T,T proof id T is being_homeomorphism by Th20; hence T,T are_homeomorphic by T_0TOPSP:def_1; :: according to TOPGRP_1:def_3 ::_thesis: id T is being_homeomorphism thus id T is being_homeomorphism by Th20; ::_thesis: verum end; end; definition let T be TopStruct ; :: original: id redefine func id T -> Homeomorphism of T; coherence id T is Homeomorphism of T proof thus id T is being_homeomorphism by Th20; :: according to TOPGRP_1:def_4 ::_thesis: verum end; end; registration let T be TopStruct ; cluster -> being_homeomorphism for Homeomorphism of T; coherence for b1 being Homeomorphism of T holds b1 is being_homeomorphism by Def4; end; theorem Th30: :: TOPGRP_1:30 for T being TopStruct for f being Homeomorphism of T holds f /" is Homeomorphism of T proof let T be TopStruct ; ::_thesis: for f being Homeomorphism of T holds f /" is Homeomorphism of T let f be Homeomorphism of T; ::_thesis: f /" is Homeomorphism of T thus f /" is being_homeomorphism ; :: according to TOPGRP_1:def_4 ::_thesis: verum end; Lm2: for T being TopStruct for f being Function of T,T st T is empty holds f is being_homeomorphism proof let T be TopStruct ; ::_thesis: for f being Function of T,T st T is empty holds f is being_homeomorphism let f be Function of T,T; ::_thesis: ( T is empty implies f is being_homeomorphism ) assume A1: T is empty ; ::_thesis: f is being_homeomorphism then f = {} .= id T by A1 ; hence f is being_homeomorphism ; ::_thesis: verum end; theorem Th31: :: TOPGRP_1:31 for T being TopStruct for f, g being Homeomorphism of T holds f * g is Homeomorphism of T proof let T be TopStruct ; ::_thesis: for f, g being Homeomorphism of T holds f * g is Homeomorphism of T let f, g be Homeomorphism of T; ::_thesis: f * g is Homeomorphism of T ( not T is empty or T is empty ) ; hence f * g is being_homeomorphism by TOPS_2:57; :: according to TOPGRP_1:def_4 ::_thesis: verum end; definition let T be TopStruct ; func HomeoGroup T -> strict multMagma means :Def5: :: TOPGRP_1:def 5 for x being set holds ( ( x in the carrier of it implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of it ) & ( for f, g being Homeomorphism of T holds the multF of it . (f,g) = g * f ) ); existence ex b1 being strict multMagma st for x being set holds ( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) ) proof defpred S1[ 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) & S1[q] ) ) from XBOOLE_0:sch_1(); A2: now__::_thesis:_for_f_being_Homeomorphism_of_T_holds_f_in_A let f be Homeomorphism of T; ::_thesis: f in A f in Funcs ( the carrier of T, the carrier of T) by FUNCT_2:9; hence f in A by A1; ::_thesis: verum end; then reconsider A = A as non empty set ; defpred S2[ 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 S2[x,y,z] proof let x, y be Element of A; ::_thesis: ex z being Element of A st S2[x,y,z] 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 ; ::_thesis: S2[x,y,z] take x1 ; ::_thesis: ex g being Homeomorphism of T st ( x = x1 & y = g & z = g * x1 ) take y1 ; ::_thesis: ( x = x1 & y = y1 & z = y1 * x1 ) thus ( x = x1 & y = y1 & z = y1 * x1 ) ; ::_thesis: verum end; consider o being BinOp of A such that A4: for a, b being Element of A holds S2[a,b,o . (a,b)] from BINOP_1:sch_3(A3); take G = multMagma(# A,o #); ::_thesis: for x being set holds ( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) ) let x be set ; ::_thesis: ( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) ) thus ( x in the carrier of G iff x is Homeomorphism of T ) by A1, A2; ::_thesis: for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f let f, g be Homeomorphism of T; ::_thesis: the multF of G . (f,g) = g * f 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 multF of G . (f,g) = g * f ; ::_thesis: verum end; uniqueness for b1, b2 being strict multMagma st ( for x being set holds ( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) ) ) & ( for x being set holds ( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) ) holds b1 = b2 proof defpred S1[ set ] means \$1 is Homeomorphism of T; let A, B be strict multMagma ; ::_thesis: ( ( for x being set holds ( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) ) & ( for x being set holds ( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ) implies A = B ) assume that A5: for x being set holds ( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) and A6: for x being set holds ( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ; ::_thesis: A = B A7: for x being set holds ( x in the carrier of B iff S1[x] ) by A6; A8: for c, d being set st c in the carrier of A & d in the carrier of A holds the multF of A . (c,d) = the multF of B . (c,d) proof let c, d be set ; ::_thesis: ( c in the carrier of A & d in the carrier of A implies the multF of A . (c,d) = the multF of B . (c,d) ) assume ( c in the carrier of A & d in the carrier of A ) ; ::_thesis: the multF of A . (c,d) = the multF of B . (c,d) then reconsider f = c, g = d as Homeomorphism of T by A5; thus the multF of A . (c,d) = g * f by A5 .= the multF of B . (c,d) by A6 ; ::_thesis: verum end; A9: for x being set holds ( x in the carrier of A iff S1[x] ) by A5; the carrier of A = the carrier of B from XBOOLE_0:sch_2(A9, A7); hence A = B by A8, BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def5 defines HomeoGroup TOPGRP_1:def_5_:_ for T being TopStruct for b2 being strict multMagma holds ( b2 = HomeoGroup T iff for x being set holds ( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) ); registration let T be TopStruct ; cluster HomeoGroup T -> non empty strict ; coherence not HomeoGroup T is empty proof id T is Homeomorphism of T ; hence not the carrier of (HomeoGroup T) is empty by Def5; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem :: TOPGRP_1:32 for T being TopStruct 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 by Def5; registration let T be TopStruct ; cluster HomeoGroup T -> strict Group-like associative ; coherence ( HomeoGroup T is Group-like & HomeoGroup T is associative ) proof set G = HomeoGroup T; set o = the multF of (HomeoGroup T); thus HomeoGroup T is Group-like ::_thesis: HomeoGroup T is associative proof reconsider e = id T as Element of (HomeoGroup T) by Def5; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (HomeoGroup T) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (HomeoGroup T) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st ( h * b1 = e & b1 * h = e ) ) reconsider h1 = h, e1 = e as Homeomorphism of T by Def5; thus h * e = e1 * h1 by Def5 .= h by FUNCT_2:17 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st ( h * b1 = e & b1 * h = e ) ) thus e * h = h1 * e1 by Def5 .= h by FUNCT_2:17 ; ::_thesis: ex b1 being Element of the carrier of (HomeoGroup T) st ( h * b1 = e & b1 * h = e ) reconsider h1 = h as Homeomorphism of T by Def5; A1: dom h1 = [#] T by TOPS_2:def_5; h1 /" is Homeomorphism of T by Th30; then reconsider g = h1 /" as Element of (HomeoGroup T) by Def5; reconsider g1 = g as Homeomorphism of T by Def5; take g ; ::_thesis: ( h * g = e & g * h = e ) A2: rng h1 = [#] T by TOPS_2:def_5; thus h * g = g1 * h1 by Def5 .= e by A1, A2, TOPS_2:52 ; ::_thesis: g * h = e thus g * h = h1 * g1 by Def5 .= e by A2, TOPS_2:52 ; ::_thesis: verum end; let x, y, z be Element of (HomeoGroup T); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) reconsider f = x, g = y as Homeomorphism of T by Def5; reconsider p = g * f, r = z as Homeomorphism of T by Def5, Th31; reconsider a = r * g as Homeomorphism of T by Th31; thus (x * y) * z = the multF of (HomeoGroup T) . ((g * f),z) by Def5 .= r * p by Def5 .= (r * g) * f by RELAT_1:36 .= the multF of (HomeoGroup T) . (f,a) by Def5 .= x * (y * z) by Def5 ; ::_thesis: verum end; end; theorem Th33: :: TOPGRP_1:33 for T being TopStruct holds id T = 1_ (HomeoGroup T) proof let T be TopStruct ; ::_thesis: id T = 1_ (HomeoGroup T) set G = HomeoGroup T; reconsider e = id T as Element of (HomeoGroup T) by Def5; now__::_thesis:_for_h_being_Element_of_(HomeoGroup_T)_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h ) reconsider h1 = h as Homeomorphism of T by Def5; thus h * e = (id T) * h1 by Def5 .= h by FUNCT_2:17 ; ::_thesis: e * h = h thus e * h = h1 * (id T) by Def5 .= h by FUNCT_2:17 ; ::_thesis: verum end; hence id T = 1_ (HomeoGroup T) by GROUP_1:4; ::_thesis: verum end; theorem :: TOPGRP_1:34 for T being TopStruct for f being Homeomorphism of T for a being Element of (HomeoGroup T) st f = a holds a " = f /" proof let T be TopStruct ; ::_thesis: for f being Homeomorphism of T for a being Element of (HomeoGroup T) st f = a holds a " = f /" let f be Homeomorphism of T; ::_thesis: for a being Element of (HomeoGroup T) st f = a holds a " = f /" set G = HomeoGroup T; A1: dom f = [#] T by TOPS_2:def_5; A2: f /" is Homeomorphism of T by Def4; then reconsider g = f /" as Element of (HomeoGroup T) by Def5; A3: rng f = [#] T by TOPS_2:def_5; let a be Element of (HomeoGroup T); ::_thesis: ( f = a implies a " = f /" ) assume A4: f = a ; ::_thesis: a " = f /" A5: g * a = f * (f /") by A4, A2, Def5 .= id T by A3, TOPS_2:52 .= 1_ (HomeoGroup T) by Th33 ; a * g = (f /") * f by A4, A2, Def5 .= id T by A1, A3, TOPS_2:52 .= 1_ (HomeoGroup T) by Th33 ; hence a " = f /" by A5, GROUP_1:5; ::_thesis: verum end; definition let T be TopStruct ; attrT is homogeneous means :Def6: :: TOPGRP_1:def 6 for p, q being Point of T ex f being Homeomorphism of T st f . p = q; end; :: deftheorem Def6 defines homogeneous TOPGRP_1:def_6_:_ for T being TopStruct holds ( T is homogeneous iff for p, q being Point of T ex f being Homeomorphism of T st f . p = q ); registration cluster1 -element -> 1 -element homogeneous for TopStruct ; coherence for b1 being 1 -element TopStruct holds b1 is homogeneous proof let T be 1 -element TopStruct ; ::_thesis: T is homogeneous let p, q be Point of T; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of T st f . p = q take id T ; ::_thesis: (id T) . p = q thus (id T) . p = q by STRUCT_0:def_10; ::_thesis: verum end; end; theorem :: TOPGRP_1:35 for T being non empty homogeneous TopSpace st ex p being Point of T st {p} is closed holds T is T_1 proof let T be non empty homogeneous TopSpace; ::_thesis: ( ex p being Point of T st {p} is closed implies T is T_1 ) given p being Point of T such that A1: {p} is closed ; ::_thesis: T is T_1 now__::_thesis:_for_q_being_Point_of_T_holds_{q}_is_closed let q be Point of T; ::_thesis: {q} is closed consider f being Homeomorphism of T such that A2: f . p = q by Def6; dom f = the carrier of T by FUNCT_2:def_1; then Im (f,p) = {(f . p)} by FUNCT_1:59; hence {q} is closed by A1, A2, TOPS_2:58; ::_thesis: verum end; hence T is T_1 by URYSOHN1:19; ::_thesis: verum end; theorem Th36: :: TOPGRP_1:36 for T being non empty homogeneous 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 regular proof let T be non empty homogeneous TopSpace; ::_thesis: ( 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 ) implies T is regular ) 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 ) ; ::_thesis: T is regular A2: [#] T <> {} ; now__::_thesis:_for_A_being_open_Subset_of_T for_q_being_Point_of_T_st_q_in_A_holds_ ex_fB_being_open_Subset_of_T_st_ (_q_in_fB_&_Cl_fB_c=_A_) let A be open Subset of T; ::_thesis: for q being Point of T st q in A holds ex fB being open Subset of T st ( q in fB & Cl fB c= A ) let q be Point of T; ::_thesis: ( q in A implies ex fB being open Subset of T st ( q in fB & Cl fB c= A ) ) assume A3: q in A ; ::_thesis: ex fB being open Subset of T st ( q in fB & Cl fB c= A ) consider f being Homeomorphism of T such that A4: f . p = q by Def6; A5: f " A is open by A2, TOPS_2:43; reconsider g = f as Function ; A6: dom f = the carrier of T by FUNCT_2:def_1; A7: rng f = [#] T by TOPS_2:def_5; then ( (g ") . q = (f ") . q & g . ((g ") . q) in A ) by A3, FUNCT_1:32; then A8: (g ") . q in g " A by A6, FUNCT_1:def_7; p = (g ") . q by A4, A6, FUNCT_1:32; then consider B being Subset of T such that A9: p in B and A10: B is open and A11: Cl B c= f " A by A1, A8, A5; reconsider fB = f .: B as open Subset of T by A10, Th25; take fB = fB; ::_thesis: ( q in fB & Cl fB c= A ) thus q in fB by A4, A6, A9, FUNCT_1:def_6; ::_thesis: Cl fB c= A A12: f .: (Cl B) = Cl fB by TOPS_2:60; f .: (Cl B) c= f .: (f " A) by A11, RELAT_1:123; hence Cl fB c= A by A7, A12, FUNCT_1:77; ::_thesis: verum end; hence T is regular by URYSOHN1:21; ::_thesis: verum end; begin definition attrc1 is strict ; struct TopGrStr -> multMagma , TopStruct ; aggrTopGrStr(# carrier, multF, topology #) -> TopGrStr ; end; registration let A be non empty set ; let R be BinOp of A; let T be Subset-Family of A; cluster TopGrStr(# A,R,T #) -> non empty ; coherence not TopGrStr(# A,R,T #) is empty ; end; registration let x be set ; let R be BinOp of {x}; let T be Subset-Family of {x}; cluster TopGrStr(# {x},R,T #) -> trivial ; coherence TopGrStr(# {x},R,T #) is trivial ; end; registration cluster1 -element -> 1 -element Group-like associative commutative for multMagma ; coherence for b1 being 1 -element multMagma holds ( b1 is Group-like & b1 is associative & b1 is commutative ) proof let H be 1 -element multMagma ; ::_thesis: ( H is Group-like & H is associative & H is commutative ) hereby :: according to GROUP_1:def_2 ::_thesis: ( H is associative & H is commutative ) set e = the Element of H; take e = the Element of H; ::_thesis: for h being Element of H holds ( h * e = h & e * h = h & ex g being Element of H st ( h * g = e & g * h = e ) ) let h be Element of H; ::_thesis: ( h * e = h & e * h = h & ex g being Element of H st ( h * g = e & g * h = e ) ) thus ( h * e = h & e * h = h ) by STRUCT_0:def_10; ::_thesis: ex g being Element of H st ( h * g = e & g * h = e ) take g = e; ::_thesis: ( h * g = e & g * h = e ) thus ( h * g = e & g * h = e ) by STRUCT_0:def_10; ::_thesis: verum end; thus for x, y, z being Element of H holds (x * y) * z = x * (y * z) by STRUCT_0:def_10; :: according to GROUP_1:def_3 ::_thesis: H is commutative let x, y be Element of H; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x thus x * y = y * x by STRUCT_0:def_10; ::_thesis: verum end; end; registration let a be set ; cluster 1TopSp {a} -> trivial ; coherence 1TopSp {a} is trivial ; end; registration cluster non empty strict for TopGrStr ; existence ex b1 being TopGrStr st ( b1 is strict & not b1 is empty ) proof set R = the BinOp of {{}}; set T = the Subset-Family of {{}}; take TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty ) thus ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty ) ; ::_thesis: verum end; end; registration cluster1 -element TopSpace-like strict for TopGrStr ; existence ex b1 being TopGrStr st ( b1 is strict & b1 is TopSpace-like & b1 is 1 -element ) proof set R = the BinOp of {{}}; take TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) the carrier of (1TopSp {{}}) is 1 -element ; hence ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) by TEX_2:7; ::_thesis: verum end; end; definition let G be non empty Group-like associative TopGrStr ; attrG is UnContinuous means :Def7: :: TOPGRP_1:def 7 inverse_op G is continuous ; end; :: deftheorem Def7 defines UnContinuous TOPGRP_1:def_7_:_ for G being non empty Group-like associative TopGrStr holds ( G is UnContinuous iff inverse_op G is continuous ); definition let G be TopSpace-like TopGrStr ; attrG is BinContinuous means :Def8: :: TOPGRP_1:def 8 for f being Function of [:G,G:],G st f = the multF of G holds f is continuous ; end; :: deftheorem Def8 defines BinContinuous TOPGRP_1:def_8_:_ for G being TopSpace-like TopGrStr holds ( G is BinContinuous iff for f being Function of [:G,G:],G st f = the multF of G holds f is continuous ); registration cluster non empty trivial V43() 1 -element TopSpace-like compact unital Group-like associative commutative homogeneous strict UnContinuous BinContinuous for TopGrStr ; existence ex b1 being 1 -element TopSpace-like Group-like associative TopGrStr st ( b1 is strict & b1 is commutative & b1 is UnContinuous & b1 is BinContinuous ) proof set R = the BinOp of {{}}; 1TopSp {{}} is 1 -element ; then reconsider T = TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) as 1 -element TopSpace-like strict TopGrStr by TEX_2:7; take T ; ::_thesis: ( T is strict & T is commutative & T is UnContinuous & T is BinContinuous ) thus ( T is strict & T is commutative ) ; ::_thesis: ( T is UnContinuous & T is BinContinuous ) hereby :: according to TOPGRP_1:def_7 ::_thesis: T is BinContinuous set f = inverse_op T; thus inverse_op T is continuous ::_thesis: verum proof let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or (inverse_op T) " P1 is closed ) assume P1 is closed ; ::_thesis: (inverse_op T) " P1 is closed percases ( (inverse_op T) " P1 = {} or (inverse_op T) " P1 = {{}} ) by ZFMISC_1:33; suppose (inverse_op T) " P1 = {} ; ::_thesis: (inverse_op T) " P1 is closed hence (inverse_op T) " P1 is closed ; ::_thesis: verum end; suppose (inverse_op T) " P1 = {{}} ; ::_thesis: (inverse_op T) " P1 is closed then (inverse_op T) " P1 = [#] T ; hence (inverse_op T) " P1 is closed ; ::_thesis: verum end; end; end; end; let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous ) assume f = the multF of T ; ::_thesis: f is continuous A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def_2 .= {[{},{}]} by ZFMISC_1:29 ; let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed ) assume P1 is closed ; ::_thesis: f " P1 is closed percases ( f " P1 = {} or f " P1 = {[{},{}]} ) by A1, ZFMISC_1:33; suppose f " P1 = {} ; ::_thesis: f " P1 is closed hence f " P1 is closed ; ::_thesis: verum end; suppose f " P1 = {[{},{}]} ; ::_thesis: f " P1 is closed then f " P1 = [#] [:T,T:] by A1; hence f " P1 is closed ; ::_thesis: verum end; end; end; end; definition mode TopGroup is non empty TopSpace-like Group-like associative TopGrStr ; end; definition mode TopologicalGroup is UnContinuous BinContinuous TopGroup; end; theorem Th37: :: TOPGRP_1:37 for T being non empty TopSpace-like BinContinuous TopGrStr for a, b being Element of T for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W proof let T be non empty TopSpace-like BinContinuous TopGrStr ; ::_thesis: for a, b being Element of T for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W let W be a_neighborhood of a * b; ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2; then reconsider f = the multF of T as Function of [:T,T:],T ; f is continuous by Def8; then consider H being a_neighborhood of [a,b] such that A1: f .: H c= W by BORSUK_1:def_1; consider F being Subset-Family of [:T,T:] such that A2: Int H = union F and A3: for e being set st e in F holds ex X1, Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; [a,b] in Int H by CONNSP_2:def_1; then consider M being set such that A4: [a,b] in M and A5: M in F by A2, TARSKI:def_4; consider A, B being Subset of T such that A6: M = [:A,B:] and A7: A is open and A8: B is open by A3, A5; a in A by A4, A6, ZFMISC_1:87; then A9: a in Int A by A7, TOPS_1:23; b in B by A4, A6, ZFMISC_1:87; then b in Int B by A8, TOPS_1:23; then reconsider B = B as open a_neighborhood of b by A8, CONNSP_2:def_1; reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def_1; take A ; ::_thesis: ex B being open a_neighborhood of b st A * B c= W take B ; ::_thesis: A * B c= W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in W ) assume x in A * B ; ::_thesis: x in W then consider g, h being Element of T such that A10: x = g * h and A11: ( g in A & h in B ) ; A12: Int H c= H by TOPS_1:16; [g,h] in M by A6, A11, ZFMISC_1:87; then [g,h] in Int H by A2, A5, TARSKI:def_4; then x in f .: H by A10, A12, FUNCT_2:35; hence x in W by A1; ::_thesis: verum end; theorem Th38: :: TOPGRP_1:38 for T being non empty TopSpace-like TopGrStr st ( for a, b being Element of T for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) holds T is BinContinuous proof let T be non empty TopSpace-like TopGrStr ; ::_thesis: ( ( for a, b being Element of T for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) implies T is BinContinuous ) assume A1: for a, b being Element of T for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ; ::_thesis: T is BinContinuous let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous ) assume A2: f = the multF of T ; ::_thesis: f is continuous for W being Point of [:T,T:] for 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:]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G consider a, b being Point of T such that A3: W = [a,b] by BORSUK_1:10; f . W = a * b by A2, A3; 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 ; ::_thesis: f .: H c= G thus f .: H c= G by A2, A4, Th15; ::_thesis: verum end; hence f is continuous by BORSUK_1:def_1; ::_thesis: verum end; theorem Th39: :: TOPGRP_1:39 for T being UnContinuous TopGroup for a being Element of T for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W proof let T be UnContinuous TopGroup; ::_thesis: for a being Element of T for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W let W be a_neighborhood of a " ; ::_thesis: ex A being open a_neighborhood of a st A " c= W reconsider f = inverse_op T as Function of T,T ; ( f . a = a " & f is continuous ) by Def7, GROUP_1:def_6; then consider H being a_neighborhood of a such that A1: f .: H c= W by BORSUK_1:def_1; a in Int (Int H) by CONNSP_2:def_1; then reconsider A = Int H as open a_neighborhood of a by CONNSP_2:def_1; take A ; ::_thesis: A " c= W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in W ) assume x in A " ; ::_thesis: x in W then consider g being Element of T such that A2: x = g " and A3: g in A ; ( Int H c= H & f . g = g " ) by GROUP_1:def_6, TOPS_1:16; then g " in f .: H by A3, FUNCT_2:35; hence x in W by A1, A2; ::_thesis: verum end; theorem Th40: :: TOPGRP_1:40 for T being TopGroup st ( for a being Element of T for 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; ::_thesis: ( ( for a being Element of T for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ) implies T is UnContinuous ) assume A1: for a being Element of T for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ; ::_thesis: T is UnContinuous set f = inverse_op T; for W being Point of T for G being a_neighborhood of (inverse_op T) . W ex H being a_neighborhood of W st (inverse_op T) .: H c= G proof let a be Point of T; ::_thesis: for G being a_neighborhood of (inverse_op T) . a ex H being a_neighborhood of a st (inverse_op T) .: H c= G let G be a_neighborhood of (inverse_op T) . a; ::_thesis: ex H being a_neighborhood of a st (inverse_op T) .: H c= G (inverse_op T) . 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 ; ::_thesis: (inverse_op T) .: A c= G thus (inverse_op T) .: A c= G by A2, Th10; ::_thesis: verum end; hence inverse_op T is continuous by BORSUK_1:def_1; :: according to TOPGRP_1:def_7 ::_thesis: verum end; theorem Th41: :: TOPGRP_1:41 for T being TopologicalGroup for a, b being Element of T for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W proof let T be TopologicalGroup; ::_thesis: for a, b being Element of T for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W let W be a_neighborhood of a * (b "); ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W 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 ; ::_thesis: ex B being open a_neighborhood of b st A * (B ") c= W take C ; ::_thesis: A * (C ") c= W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (C ") or x in W ) assume x in A * (C ") ; ::_thesis: x in W then consider g, h being Element of T such that A3: x = g * h and A4: g in A and A5: h in C " ; consider k being Element of T such that A6: h = k " and k in C by A5; g * (k ") in A * B by A2, A4, A5, A6; hence x in W by A1, A3, A6; ::_thesis: verum end; theorem :: TOPGRP_1:42 for T being TopGroup st ( for a, b being Element of T for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) holds T is TopologicalGroup proof let T be TopGroup; ::_thesis: ( ( for a, b being Element of T for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) implies T is TopologicalGroup ) assume A1: for a, b being Element of T for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ; ::_thesis: T is TopologicalGroup A2: for a being Element of T for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W proof let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W let W be a_neighborhood of a " ; ::_thesis: ex A being a_neighborhood of a st A " c= W 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 ; ::_thesis: B " c= W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B " or x in W ) assume A4: x in B " ; ::_thesis: x in W then consider g being Element of T such that A5: x = g " and g in B ; 1_ T in A by CONNSP_2:4; then (1_ T) * (g ") in A * (B ") by A4, A5; then g " in A * (B ") by GROUP_1:def_4; hence x in W by A3, A5; ::_thesis: verum end; for a, b being Element of T for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W proof let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W let W be a_neighborhood of a * b; ::_thesis: ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W W is a_neighborhood of a * ((b ") ") ; 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 ; ::_thesis: ex B being a_neighborhood of b st A * B c= W take B1 ; ::_thesis: A * B1 c= W let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B1 or x in W ) assume x in A * B1 ; ::_thesis: x in W then consider g, h being Element of T such that A8: ( x = g * h & g in A ) and A9: h in B1 ; h " in B1 " by A9; then h in B " by A7, Th7; then x in A * (B ") by A8; hence x in W by A6; ::_thesis: verum end; hence T is TopologicalGroup by A2, Th38, Th40; ::_thesis: verum end; registration let G be non empty TopSpace-like BinContinuous TopGrStr ; let a be Element of G; clustera * -> continuous ; coherence a * is continuous proof set f = a * ; for w being Point of G for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A proof let w be Point of G; ::_thesis: for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A let A be a_neighborhood of (a *) . w; ::_thesis: ex W being a_neighborhood of w st (a *) .: W c= A (a *) . 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 ; ::_thesis: (a *) .: W c= A let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (a *) .: W or k in A ) assume k in (a *) .: W ; ::_thesis: k in A then k in a * W by Th16; then A2: ex h being Element of G st ( k = a * h & h in W ) by GROUP_2:27; a in B by CONNSP_2:4; then k in B * W by A2; hence k in A by A1; ::_thesis: verum end; hence a * is continuous by BORSUK_1:def_1; ::_thesis: verum end; cluster * a -> continuous ; coherence * a is continuous proof set f = * a; for w being Point of G for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A proof let w be Point of G; ::_thesis: for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A let A be a_neighborhood of (* a) . w; ::_thesis: ex W being a_neighborhood of w st (* a) .: W c= A (* a) . 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 ; ::_thesis: (* a) .: W c= A let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (* a) .: W or k in A ) assume k in (* a) .: W ; ::_thesis: k in A then k in W * a by Th17; then A4: ex h being Element of G st ( k = h * a & h in W ) by GROUP_2:28; a in B by CONNSP_2:4; then k in W * B by A4; hence k in A by A3; ::_thesis: verum end; hence * a is continuous by BORSUK_1:def_1; ::_thesis: verum end; end; theorem Th43: :: TOPGRP_1:43 for G being BinContinuous TopGroup for a being Element of G holds a * is Homeomorphism of G proof let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds a * is Homeomorphism of G let a be Element of G; ::_thesis: a * is Homeomorphism of G set f = a * ; thus ( dom (a *) = [#] G & rng (a *) = [#] G & a * is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( a * is continuous & (a *) /" is continuous ) thus a * is continuous ; ::_thesis: (a *) /" is continuous (a *) /" = (a ") * by Th18; hence (a *) /" is continuous ; ::_thesis: verum end; theorem Th44: :: TOPGRP_1:44 for G being BinContinuous TopGroup for a being Element of G holds * a is Homeomorphism of G proof let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds * a is Homeomorphism of G let a be Element of G; ::_thesis: * a is Homeomorphism of G set f = * a; thus ( dom (* a) = [#] G & rng (* a) = [#] G & * a is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( * a is continuous & (* a) /" is continuous ) thus * a is continuous ; ::_thesis: (* a) /" is continuous (* a) /" = * (a ") by Th19; hence (* a) /" is continuous ; ::_thesis: verum end; definition let G be BinContinuous TopGroup; let a be Element of G; :: original: * redefine funca * -> Homeomorphism of G; coherence a * is Homeomorphism of G by Th43; :: original: * redefine func * a -> Homeomorphism of G; coherence * a is Homeomorphism of G by Th44; end; theorem Th45: :: TOPGRP_1:45 for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G proof let G be UnContinuous TopGroup; ::_thesis: inverse_op G is Homeomorphism of G set f = inverse_op G; thus ( dom (inverse_op G) = [#] G & rng (inverse_op G) = [#] G & inverse_op G is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( inverse_op G is continuous & (inverse_op G) /" is continuous ) thus inverse_op G is continuous by Def7; ::_thesis: (inverse_op G) /" is continuous inverse_op G = (inverse_op G) " by Th14 .= (inverse_op G) /" by TOPS_2:def_4 ; hence (inverse_op G) /" is continuous by Def7; ::_thesis: verum end; definition let G be UnContinuous TopGroup; :: original: inverse_op redefine func inverse_op G -> Homeomorphism of G; coherence inverse_op G is Homeomorphism of G by Th45; end; registration cluster non empty TopSpace-like Group-like associative BinContinuous -> homogeneous for TopGrStr ; coherence for b1 being TopGroup st b1 is BinContinuous holds b1 is homogeneous proof let T be TopGroup; ::_thesis: ( T is BinContinuous implies T is homogeneous ) assume T is BinContinuous ; ::_thesis: T is homogeneous then reconsider G = T as BinContinuous TopGroup ; G is homogeneous proof let p, q be Point of G; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of G st f . p = q take * ((p ") * q) ; ::_thesis: (* ((p ") * q)) . p = q thus (* ((p ") * q)) . p = p * ((p ") * q) by Def2 .= (p * (p ")) * q by GROUP_1:def_3 .= (1_ G) * q by GROUP_1:def_5 .= q by GROUP_1:def_4 ; ::_thesis: verum end; hence T is homogeneous ; ::_thesis: verum end; end; theorem Th46: :: TOPGRP_1:46 for G being BinContinuous TopGroup for F being closed Subset of G for a being Element of G holds F * a is closed proof let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G for a being Element of G holds F * a is closed let F be closed Subset of G; ::_thesis: for a being Element of G holds F * a is closed let a be Element of G; ::_thesis: F * a is closed F * a = (* a) .: F by Th17; hence F * a is closed by TOPS_2:58; ::_thesis: verum end; theorem Th47: :: TOPGRP_1:47 for G being BinContinuous TopGroup for F being closed Subset of G for a being Element of G holds a * F is closed proof let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G for a being Element of G holds a * F is closed let F be closed Subset of G; ::_thesis: for a being Element of G holds a * F is closed let a be Element of G; ::_thesis: a * F is closed a * F = (a *) .: F by Th16; hence a * F is closed by TOPS_2:58; ::_thesis: verum end; registration let G be BinContinuous TopGroup; let F be closed Subset of G; let a be Element of G; clusterF * a -> closed ; coherence F * a is closed by Th46; clustera * F -> closed ; coherence a * F is closed by Th47; end; theorem Th48: :: TOPGRP_1:48 for G being UnContinuous TopGroup for F being closed Subset of G holds F " is closed proof let G be UnContinuous TopGroup; ::_thesis: for F being closed Subset of G holds F " is closed let F be closed Subset of G; ::_thesis: F " is closed F " = (inverse_op G) .: F by Th10; hence F " is closed by TOPS_2:58; ::_thesis: verum end; registration let G be UnContinuous TopGroup; let F be closed Subset of G; clusterF " -> closed ; coherence F " is closed by Th48; end; theorem Th49: :: TOPGRP_1:49 for G being BinContinuous TopGroup for O being open Subset of G for a being Element of G holds O * a is open proof let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G for a being Element of G holds O * a is open let O be open Subset of G; ::_thesis: for a being Element of G holds O * a is open let a be Element of G; ::_thesis: O * a is open O * a = (* a) .: O by Th17; hence O * a is open by Th25; ::_thesis: verum end; theorem Th50: :: TOPGRP_1:50 for G being BinContinuous TopGroup for O being open Subset of G for a being Element of G holds a * O is open proof let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G for a being Element of G holds a * O is open let O be open Subset of G; ::_thesis: for a being Element of G holds a * O is open let a be Element of G; ::_thesis: a * O is open a * O = (a *) .: O by Th16; hence a * O is open by Th25; ::_thesis: verum end; registration let G be BinContinuous TopGroup; let A be open Subset of G; let a be Element of G; clusterA * a -> open ; coherence A * a is open by Th49; clustera * A -> open ; coherence a * A is open by Th50; end; theorem Th51: :: TOPGRP_1:51 for G being UnContinuous TopGroup for O being open Subset of G holds O " is open proof let G be UnContinuous TopGroup; ::_thesis: for O being open Subset of G holds O " is open let O be open Subset of G; ::_thesis: O " is open O " = (inverse_op G) .: O by Th10; hence O " is open by Th25; ::_thesis: verum end; registration let G be UnContinuous TopGroup; let A be open Subset of G; clusterA " -> open ; coherence A " is open by Th51; end; theorem Th52: :: TOPGRP_1:52 for G being BinContinuous TopGroup for A, O being Subset of G st O is open holds O * A is open proof let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds O * A is open let A, O be Subset of G; ::_thesis: ( O is open implies O * A is open ) assume A1: O is open ; ::_thesis: O * A is open Int (O * A) = O * A proof thus Int (O * A) c= O * A by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: O * A c= Int (O * A) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O * A or x in Int (O * A) ) assume x in O * A ; ::_thesis: x in Int (O * A) then consider o, a being Element of G such that A2: ( x = o * a & o in O ) and A3: a in A ; set Q = O * a; A4: O * a c= O * A proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O * a or q in O * A ) assume q in O * a ; ::_thesis: q in O * A then ex h being Element of G st ( q = h * a & h in O ) by GROUP_2:28; hence q in O * A by A3; ::_thesis: verum end; x in O * a by A2, GROUP_2:28; hence x in Int (O * A) by A1, A4, TOPS_1:22; ::_thesis: verum end; hence O * A is open ; ::_thesis: verum end; theorem Th53: :: TOPGRP_1:53 for G being BinContinuous TopGroup for A, O being Subset of G st O is open holds A * O is open proof let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds A * O is open let A, O be Subset of G; ::_thesis: ( O is open implies A * O is open ) assume A1: O is open ; ::_thesis: A * O is open Int (A * O) = A * O proof thus Int (A * O) c= A * O by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: A * O c= Int (A * O) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * O or x in Int (A * O) ) assume x in A * O ; ::_thesis: x in Int (A * O) then consider a, o being Element of G such that A2: x = a * o and A3: a in A and A4: o in O ; set Q = a * O; A5: a * O c= A * O proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in a * O or q in A * O ) assume q in a * O ; ::_thesis: q in A * O then ex h being Element of G st ( q = a * h & h in O ) by GROUP_2:27; hence q in A * O by A3; ::_thesis: verum end; x in a * O by A2, A4, GROUP_2:27; hence x in Int (A * O) by A1, A5, TOPS_1:22; ::_thesis: verum end; hence A * O is open ; ::_thesis: verum end; registration let G be BinContinuous TopGroup; let A be open Subset of G; let B be Subset of G; clusterA * B -> open ; coherence A * B is open by Th52; clusterB * A -> open ; coherence B * A is open by Th53; end; theorem Th54: :: TOPGRP_1:54 for G being UnContinuous TopGroup for a being Point of G for A being a_neighborhood of a holds A " is a_neighborhood of a " proof let G be UnContinuous TopGroup; ::_thesis: for a being Point of G for A being a_neighborhood of a holds A " is a_neighborhood of a " let a be Point of G; ::_thesis: for A being a_neighborhood of a holds A " is a_neighborhood of a " let A be a_neighborhood of a; ::_thesis: A " is 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 and A2: ( Q c= A & a in Q ) by TOPS_1:22; ( Q " c= A " & a " in Q " ) by A2, Th9; hence a " in Int (A ") by A1, TOPS_1:22; :: according to CONNSP_2:def_1 ::_thesis: verum end; theorem Th55: :: TOPGRP_1:55 for G being TopologicalGroup for a being Point of G for 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; ::_thesis: for a being Point of G for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A let a be Point of G; ::_thesis: for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A let A be a_neighborhood of a * (a "); ::_thesis: ex B being open a_neighborhood of a st B * (B ") c= 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:2; take B ; ::_thesis: B * (B ") c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * (B ") or x in A ) assume x in B * (B ") ; ::_thesis: x in A then consider g, h being Point of G such that A2: x = g * h and A3: g in B and A4: h in B " ; h " in B by A4, Th7; then h " in Y by XBOOLE_0:def_4; then A5: h in Y " by Th7; g in X by A3, XBOOLE_0:def_4; then x in X * (Y ") by A2, A5; hence x in A by A1; ::_thesis: verum end; theorem Th56: :: TOPGRP_1:56 for G being UnContinuous TopGroup for A being dense Subset of G holds A " is dense proof let G be UnContinuous TopGroup; ::_thesis: for A being dense Subset of G holds A " is dense let A be dense Subset of G; ::_thesis: A " is dense (inverse_op G) " A = A " by Th11; hence A " is dense by Th29; ::_thesis: verum end; registration let G be UnContinuous TopGroup; let A be dense Subset of G; clusterA " -> dense ; coherence A " is dense by Th56; end; theorem Th57: :: TOPGRP_1:57 for G being BinContinuous TopGroup for A being dense Subset of G for a being Point of G holds a * A is dense proof let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G for a being Point of G holds a * A is dense let A be dense Subset of G; ::_thesis: for a being Point of G holds a * A is dense let a be Point of G; ::_thesis: a * A is dense (a *) .: A = a * A by Th16; hence a * A is dense by Th28; ::_thesis: verum end; theorem Th58: :: TOPGRP_1:58 for G being BinContinuous TopGroup for A being dense Subset of G for a being Point of G holds A * a is dense proof let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G for a being Point of G holds A * a is dense let A be dense Subset of G; ::_thesis: for a being Point of G holds A * a is dense let a be Point of G; ::_thesis: A * a is dense (* a) .: A = A * a by Th17; hence A * a is dense by Th28; ::_thesis: verum end; registration let G be BinContinuous TopGroup; let A be dense Subset of G; let a be Point of G; clusterA * a -> dense ; coherence A * a is dense by Th58; clustera * A -> dense ; coherence a * A is dense by Th57; end; theorem :: TOPGRP_1:59 for G being TopologicalGroup for B being Basis of 1_ G for 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; ::_thesis: for B being Basis of 1_ G for 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 let B be Basis of 1_ G; ::_thesis: for 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 let M be dense Subset of G; ::_thesis: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G set Z = { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; A1: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= the topology of G proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in the topology of G ) assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; ::_thesis: a in the topology of G then consider V being Subset of G, x being Point of G such that A2: a = V * x and A3: V in B and x in M ; reconsider V = V as Subset of G ; V is open by A3, YELLOW_8:12; hence a in the topology of G by A2, PRE_TOPC:def_2; ::_thesis: verum end; A4: for W being Subset of G st W is open holds for a being Point of G st a in W holds ex V being Subset of G st ( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) proof A5: (1_ G) * ((1_ G) ") = (1_ G) * (1_ G) by GROUP_1:8 .= 1_ G by GROUP_1:def_4 ; let W be Subset of G; ::_thesis: ( W is open implies for a being Point of G st a in W holds ex V being Subset of G st ( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) ) assume A6: W is open ; ::_thesis: for a being Point of G st a in W holds ex V being Subset of G st ( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) let a be Point of G; ::_thesis: ( a in W implies ex V being Subset of G st ( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) ) assume A7: a in W ; ::_thesis: ex V being Subset of G st ( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) 1_ G = a * (a ") by GROUP_1:def_5; then 1_ G in W * (a ") by A7, GROUP_2:28; then W * (a ") is a_neighborhood of (1_ G) * ((1_ G) ") by A6, A5, CONNSP_2:3; then consider V being open a_neighborhood of 1_ G such that A8: V * (V ") c= W * (a ") by Th55; consider E being Subset of G such that A9: E in B and A10: E c= V by CONNSP_2:4, YELLOW_8:13; ( E is open & E <> {} ) by A9, YELLOW_8:12; then a * (M ") meets E by TOPS_1:45; then consider d being set such that A11: d in (a * (M ")) /\ E by XBOOLE_0:4; reconsider d = d as Point of G by A11; take I = E * ((d ") * a); ::_thesis: ( I in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in I & I c= W ) d in a * (M ") by A11, XBOOLE_0:def_4; then consider m being Point of G such that A12: d = a * m and A13: m in M " by GROUP_2:27; (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 GROUP_1:def_3 .= ((d ") * d) * (m ") by A12, GROUP_1:def_3 .= (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 { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } by A9; ::_thesis: ( a in I & I c= W ) A14: (1_ G) * a = a by GROUP_1:def_4; A15: d in E by A11, XBOOLE_0:def_4; E * (d ") c= V * (V ") proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in E * (d ") or q in V * (V ") ) assume q in E * (d ") ; ::_thesis: q in V * (V ") then A16: ex v being Point of G st ( q = v * (d ") & v in E ) by GROUP_2:28; d " in V " by A10, A15; hence q in V * (V ") by A10, A16; ::_thesis: verum end; then E * (d ") c= W * (a ") by A8, XBOOLE_1:1; then A17: (E * (d ")) * a c= (W * (a ")) * a by Th5; d * (d ") = 1_ G by GROUP_1:def_5; then 1_ G in E * (d ") by A15, GROUP_2:28; then a in (E * (d ")) * a by A14, GROUP_2:28; hence a in I by GROUP_2:34; ::_thesis: I c= W (W * (a ")) * a = W * ((a ") * a) by GROUP_2:34 .= W * (1_ G) by GROUP_1:def_5 .= W by GROUP_2:37 ; hence I c= W by A17, GROUP_2:34; ::_thesis: verum end; { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= bool the carrier of G proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in bool the carrier of G ) assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; ::_thesis: a in bool the carrier of G then ex V being Subset of G ex x being Point of G st ( a = V * x & V in B & x in M ) ; hence a in bool the carrier of G ; ::_thesis: verum end; hence { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G by A1, A4, YELLOW_9:32; ::_thesis: verum end; theorem Th60: :: TOPGRP_1:60 for G being TopologicalGroup holds G is regular proof let G be TopologicalGroup; ::_thesis: G is regular 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 1_ G ; ::_thesis: for A being Subset of G st A is open & 1_ G in A holds ex B being Subset of G st ( 1_ G in B & B is open & Cl B c= A ) let A be Subset of G; ::_thesis: ( A is open & 1_ G in A implies ex B being Subset of G st ( 1_ G in B & B is open & Cl B c= A ) ) assume ( A is open & 1_ G in A ) ; ::_thesis: ex B being Subset of G st ( 1_ G in B & B is open & Cl B c= A ) then 1_ G in Int A by TOPS_1:23; then A1: A is a_neighborhood of 1_ G by CONNSP_2:def_1; 1_ G = (1_ G) * ((1_ G) ") by GROUP_1:def_5; then consider C being open a_neighborhood of 1_ G, B being open a_neighborhood of (1_ G) " such that A2: C * B c= A by A1, Th37; ((1_ G) ") " = 1_ G ; then B " is a_neighborhood of 1_ G by Th54; then reconsider W = C /\ (B ") as a_neighborhood of 1_ G by CONNSP_2:2; W c= B " by XBOOLE_1:17; then W " c= (B ") " by Th9; then C * (W ") c= C * B by Th4; then A3: C * (W ") c= A by A2, XBOOLE_1:1; take W ; ::_thesis: ( 1_ G in W & W is open & Cl W c= A ) Int W = W by TOPS_1:23; hence A4: ( 1_ G in W & W is open ) by CONNSP_2:def_1; ::_thesis: Cl W c= A let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Cl W or p in A ) assume A5: p in Cl W ; ::_thesis: p in A then reconsider r = p as Point of G ; r = r * (1_ G) by GROUP_1:def_4; then p in r * W by A4, GROUP_2:27; then r * W meets W by A5, PRE_TOPC:def_7; then consider a being set such that A6: a in (r * W) /\ W by XBOOLE_0:4; A7: a in W by A6, XBOOLE_0:def_4; A8: a in r * W by A6, XBOOLE_0:def_4; reconsider a = a as Point of G by A6; consider b being Element of G such that A9: a = r * b and A10: b in W by A8, GROUP_2:27; A11: ( W c= C & b " in W " ) by A10, XBOOLE_1:17; r = r * (1_ G) by GROUP_1:def_4 .= r * (b * (b ")) by GROUP_1:def_5 .= a * (b ") by A9, GROUP_1:def_3 ; then p in C * (W ") by A7, A11; hence p in A by A3; ::_thesis: verum end; hence G is regular by Th36; ::_thesis: verum end; registration cluster non empty TopSpace-like Group-like associative UnContinuous BinContinuous -> regular for TopGrStr ; coherence for b1 being TopologicalGroup holds b1 is regular by Th60; end; theorem :: TOPGRP_1:61 for T being TopStruct for f being Function of T,T st T is empty holds f is being_homeomorphism by Lm2;