let TG be TopologicalGroup; :: thesis: the topology of (TopSpace_induced_by (left_uniformity TG)) = the topology of TG
set X = the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG)));
set Y = the topology of TG;
A2: the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG))) c= the topology of TG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG))) or x in the topology of TG )
assume x in the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG))) ; :: thesis: x in the topology of TG
then x in Family_open_set (FMT_induced_by (left_uniformity TG)) by FINTOPO7:def 16;
then consider y being open Subset of (FMT_induced_by (left_uniformity TG)) such that
A3: x = y ;
reconsider z = x as Subset of TG by A3;
z is open

proof

now :: thesis: for t being Point of TG st t in z holds
ex A being Subset of TG st
( A is a_neighborhood of t & A c= z )

let t be Point of TG; :: thesis: ( t in z implies ex A being Subset of TG st
( A is a_neighborhood of t & A c= z ) )
assume A4: t in z ; :: thesis: ex A being Subset of TG st
( A is a_neighborhood of t & A c= z )
reconsider t1 = t as Point of (FMT_induced_by (left_uniformity TG)) ;
A5: y in U_FMT t1 by A3, A4, FINTOPO7:def 1;
reconsider t2 = t1 as Element of (left_uniformity TG) ;
z in Neighborhood t2 by A3, A5, UNIFORM2:def 14;
then consider V0 being Element of the entourages of (left_uniformity TG) such that
A6: z = Neighborhood (V0,t2) ;
consider tg being Element of system_left_uniformity TG such that
A7: tg c= V0 by CARDFIL2:def 8;
tg in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;
then consider U0 being a_neighborhood of 1_ TG such that
A8: tg = element_left_uniformity U0 ;
reconsider A = {t} * U0 as a_neighborhood of t by Th4;
A c= z

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in z )
assume u in A ; :: thesis: u in z
then consider u0, u1 being Element of TG such that
A9: u = u0 * u1 and
A10: u0 in {t} and
A11: u1 in U0 ;
reconsider u2 = u as Element of TG by A9;
(1_ TG) * u1 in U0 by A11, GROUP_1:def 4;
then ((t ") * t) * u1 in U0 by GROUP_1:def 5;
then (t ") * (t * u1) in U0 by GROUP_1:def 3;
then (t ") * u2 in U0 by A9, A10, TARSKI:def 1;
then [t,u2] in element_left_uniformity U0 ;
hence u in z by A6, A7, A8; :: thesis: verum

end;

hence ex A being Subset of TG st
( A is a_neighborhood of t & A c= z ) ; :: thesis: verum

end;

hence z is open by CONNSP_2:7; :: thesis: verum

end;

hence x in the topology of TG ; :: thesis: verum

end;

the topology of TG c= the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG)))

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in the topology of TG or u in the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG))) )
assume A12: u in the topology of TG ; :: thesis: u in the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG)))
then reconsider u = u as Subset of TG ;
reconsider v = u as Subset of (FMT_induced_by (left_uniformity TG)) ;
for x being Element of (FMT_induced_by (left_uniformity TG)) st x in v holds
v in U_FMT x

proof

let x be Element of (FMT_induced_by (left_uniformity TG)); :: thesis: ( x in v implies v in U_FMT x )
assume A13: x in v ; :: thesis: v in U_FMT x
reconsider t2 = x as Element of (left_uniformity TG) ;
reconsider t3 = x as Element of TG ;
reconsider w = v as Subset of TG ;

now :: thesis: ( 1_ TG in ({t3} ") * w & ({t3} ") * w is open )

{(t3 ")} = {t3} " by GROUP_2:3;
then t3 " in {t3} " by TARSKI:def 1;
then (t3 ") * t3 in ({t3} ") * w by A13;
hence 1_ TG in ({t3} ") * w by GROUP_1:def 5; :: thesis: ({t3} ") * w is open
w is open by A12;
hence ({t3} ") * w is open ; :: thesis: verum

end;

then reconsider U0 = ({t3} ") * w as a_neighborhood of 1_ TG by CONNSP_2:6;
element_left_uniformity U0 in system_left_uniformity TG ;
then reconsider V0 = element_left_uniformity U0 as Element of the entourages of (left_uniformity TG) by CARDFIL2:def 8;
v = { y where y is Element of TG : [t2,y] in V0 }

proof

set v2 = { y where y is Element of TG : [t2,y] in V0 } ;
A15: v c= { y where y is Element of TG : [t2,y] in V0 }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in v or t in { y where y is Element of TG : [t2,y] in V0 } )
assume A16: t in v ; :: thesis: t in { y where y is Element of TG : [t2,y] in V0 }
then reconsider t4 = t as Element of TG ;
{(t3 ")} = {t3} " by GROUP_2:3;
then A17: t3 " in {t3} " by TARSKI:def 1;
(t3 ") * t4 in ({t3} ") * w by A16, A17;
then [t2,t4] in element_left_uniformity U0 ;
hence t in { y where y is Element of TG : [t2,y] in V0 } ; :: thesis: verum

end;

{ y where y is Element of TG : [t2,y] in V0 } c= v

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Element of TG : [t2,y] in V0 } or t in v )
assume t in { y where y is Element of TG : [t2,y] in V0 } ; :: thesis: t in v
then consider y0 being Element of TG such that
A18: t = y0 and
A19: [t2,y0] in V0 ;
consider xt, yt being Element of TG such that
A20: [t2,y0] = [xt,yt] and
A21: (xt ") * yt in U0 by A19;
( t2 = xt & y0 = yt ) by A20, XTUPLE_0:1;
then consider u1, u2 being Element of TG such that
A22: (t3 ") * y0 = u1 * u2 and
A23: u1 in {t3} " and
A24: u2 in w by A21;
{(t3 ")} = {t3} " by GROUP_2:3;
then u1 = t3 " by A23, TARSKI:def 1;
hence t in v by A18, A22, A24, GROUP_1:6; :: thesis: verum

end;

hence v = { y where y is Element of TG : [t2,y] in V0 } by A15; :: thesis: verum

end;

then v = Neighborhood (V0,t2) ;
then v in Neighborhood t2 ;
hence v in U_FMT x by UNIFORM2:def 14; :: thesis: verum

end;

then v is open ;
then u in Family_open_set (FMT_induced_by (left_uniformity TG)) ;
hence u in the topology of (FMT2TopSpace (FMT_induced_by (left_uniformity TG))) by FINTOPO7:def 16; :: thesis: verum

end;

hence the topology of (TopSpace_induced_by (left_uniformity TG)) = the topology of TG by A2; :: thesis: verum