set cB = system_left_uniformity TG;
now :: thesis: ( system_left_uniformity TG is quasi_basis & system_left_uniformity TG is axiom_UP1 & system_left_uniformity TG is axiom_UP2 & system_left_uniformity TG is axiom_UP3 )
now :: thesis: for B1, B2 being Element of system_left_uniformity TG ex B3 being Element of system_left_uniformity TG st B3 c= B1 /\ B2
let B1, B2 be Element of system_left_uniformity TG; :: thesis: ex B3 being Element of system_left_uniformity TG st B3 c= B1 /\ B2
B1 in system_left_uniformity TG ;
then consider U1 being a_neighborhood of 0_ TG such that
A1: B1 = element_left_uniformity U1 ;
B2 in system_left_uniformity TG ;
then consider U2 being a_neighborhood of 0_ TG such that
A2: B2 = element_left_uniformity U2 ;
reconsider U3 = U1 /\ U2 as a_neighborhood of 0_ TG by CONNSP_2:2;
set B3 = element_left_uniformity U3;
element_left_uniformity U3 in system_left_uniformity TG ;
then reconsider B3 = element_left_uniformity U3 as Element of system_left_uniformity TG ;
B3 c= B1 /\ B2
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B3 or t in B1 /\ B2 )
assume t in B3 ; :: thesis: t in B1 /\ B2
then consider x, y being Element of TG such that
A3: t = [x,y] and
A4: (- x) + y in U3 ;
( (- x) + y in U1 & (- x) + y in U2 ) by A4, XBOOLE_0:def 4;
then ( t in B1 & t in B2 ) by A3, A1, A2;
hence t in B1 /\ B2 by XBOOLE_0:def 4; :: thesis: verum
end;
hence ex B3 being Element of system_left_uniformity TG st B3 c= B1 /\ B2 ; :: thesis: verum
end;
hence system_left_uniformity TG is quasi_basis ; :: thesis: ( system_left_uniformity TG is axiom_UP1 & system_left_uniformity TG is axiom_UP2 & system_left_uniformity TG is axiom_UP3 )
now :: thesis: for B being Element of system_left_uniformity TG holds id the carrier of TG c= B
let B be Element of system_left_uniformity TG; :: thesis: id the carrier of TG c= B
B in system_left_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A5: B = element_left_uniformity U ;
now :: thesis: for t being object st t in id the carrier of TG holds
t in B
let t be object ; :: thesis: ( t in id the carrier of TG implies t in B )
assume A6: t in id the carrier of TG ; :: thesis: t in B
then consider x, y being object such that
A7: x in the carrier of TG and
A8: y in the carrier of TG and
A9: t = [x,y] by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of TG by A7, A8;
x = y by A6, A9, RELAT_1:def 10;
then (- x) + y = 0_ TG by GROUP_1A:def 4;
then ( x is Element of TG & y is Element of TG & (- x) + y in U ) by CONNSP_2:4;
hence t in B by A5, A9; :: thesis: verum
end;
hence id the carrier of TG c= B ; :: thesis: verum
end;
hence system_left_uniformity TG is axiom_UP1 ; :: thesis: ( system_left_uniformity TG is axiom_UP2 & system_left_uniformity TG is axiom_UP3 )
now :: thesis: for B1 being Element of system_left_uniformity TG ex B2 being Element of system_left_uniformity TG st B2 c= B1 ~
let B1 be Element of system_left_uniformity TG; :: thesis: ex B2 being Element of system_left_uniformity TG st B2 c= B1 ~
B1 in system_left_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A10: B1 = element_left_uniformity U ;
consider R1 being Relation of the carrier of TG such that
A11: B1 = R1 and
A12: R1 ~ = B1 ~ ;
- U is a_neighborhood of - (0_ TG) by GROUP_1A:371;
then reconsider U2 = - U as a_neighborhood of 0_ TG by GROUP_1A:8;
set B2 = element_left_uniformity U2;
element_left_uniformity U2 in system_left_uniformity TG ;
then reconsider B2 = element_left_uniformity U2 as Element of system_left_uniformity TG ;
B2 c= B1 ~
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 or t in B1 ~ )
assume t in B2 ; :: thesis: t in B1 ~
then consider a, b being Element of TG such that
A13: t = [a,b] and
A14: (- a) + b in U2 ;
consider g being Element of TG such that
A15: (- a) + b = - g and
A16: g in U by A14;
- ((- a) + b) in U by A15, A16;
then (- b) + (- (- a)) in U by GROUP_1A:16;
then [b,a] in R1 by A10, A11;
hence t in B1 ~ by A12, A13, RELAT_1:def 7; :: thesis: verum
end;
hence ex B2 being Element of system_left_uniformity TG st B2 c= B1 ~ ; :: thesis: verum
end;
hence system_left_uniformity TG is axiom_UP2 ; :: thesis: system_left_uniformity TG is axiom_UP3
now :: thesis: for B1 being Element of system_left_uniformity TG ex B2 being Element of system_left_uniformity TG st B2 * B2 c= B1
let B1 be Element of system_left_uniformity TG; :: thesis: ex B2 being Element of system_left_uniformity TG st B2 * B2 c= B1
B1 in system_left_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A17: B1 = element_left_uniformity U ;
U is a_neighborhood of (0_ TG) + (0_ TG) by GROUP_1A:def 3;
then consider A, B being open a_neighborhood of 0_ TG such that
A17bis: A + B c= U by GROUP_1A:354;
reconsider AB = A /\ B as a_neighborhood of 0_ TG by CONNSP_2:2;
( AB c= A & AB c= B ) by XBOOLE_1:17;
then A18: AB + AB c= A + B by Th3;
set B2 = element_left_uniformity AB;
element_left_uniformity AB in system_left_uniformity TG ;
then reconsider B2 = element_left_uniformity AB as Element of system_left_uniformity TG ;
B2 * B2 c= B1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 * B2 or t in B1 )
assume A19: t in B2 * B2 ; :: thesis: t in B1
consider R1, R2 being Relation of the carrier of TG such that
A20: R1 = B2 and
R2 = B2 and
B2 * B2 = R1 * R2 ;
t in { [x,y] where x, y is Element of TG : ex z being Element of TG st
( [x,z] in R1 & [z,y] in R1 ) } by A19, A20, UNIFORM2:3;
then consider x, y being Element of TG such that
A23: t = [x,y] and
A24: ex z being Element of TG st
( [x,z] in R1 & [z,y] in R1 ) ;
consider z being Element of TG such that
A25: [x,z] in R1 and
A26: [z,y] in R1 by A24;
consider a, b being Element of TG such that
A27: [x,z] = [a,b] and
A28: (- a) + b in AB by A20, A25;
A29: ( x = a & z = b ) by A27, XTUPLE_0:1;
consider c, d being Element of TG such that
A30: [z,y] = [c,d] and
A31: (- c) + d in AB by A26, A20;
A32: ( z = c & y = d ) by A30, XTUPLE_0:1;
A33: ((- a) + b) + ((- c) + d) = (- x) + (z + ((- z) + y)) by A29, A32, RLVECT_1:def 3
.= (- x) + ((z + (- z)) + y) by RLVECT_1:def 3
.= (- x) + ((0_ TG) + y) by GROUP_1A:def 4
.= (- x) + y by GROUP_1A:def 3 ;
((- a) + b) + ((- c) + d) in AB + AB by A28, A31;
then (- x) + y in U by A18, A33, A17bis;
hence t in B1 by A17, A23; :: thesis: verum
end;
hence ex B2 being Element of system_left_uniformity TG st B2 * B2 c= B1 ; :: thesis: verum
end;
hence system_left_uniformity TG is axiom_UP3 ; :: thesis: verum
end;
then ex US being strict UniformSpace st
( the carrier of US = the carrier of TG & the entourages of US = <.(system_left_uniformity TG).] ) by Th7;
hence UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace ; :: thesis: verum