let T be non empty TopSpace; :: thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) holds

T is metrizable

let pmet be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) implies T is metrizable )

assume that

A1: pmet is_metric_of the carrier of T and

A2: for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: T is metrizable

set PM = SpaceMetr ( the carrier of T,pmet);

reconsider PM = SpaceMetr ( the carrier of T,pmet) as non empty MetrSpace by A1, PCOMPS_1:36;

A3: for x, y being Element of PM holds pmet . (x,y) = dist (x,y)

hence T is metrizable by A1, PCOMPS_1:def 8; :: thesis: verum

T is metrizable

let pmet be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) implies T is metrizable )

assume that

A1: pmet is_metric_of the carrier of T and

A2: for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: T is metrizable

set PM = SpaceMetr ( the carrier of T,pmet);

reconsider PM = SpaceMetr ( the carrier of T,pmet) as non empty MetrSpace by A1, PCOMPS_1:36;

A3: for x, y being Element of PM holds pmet . (x,y) = dist (x,y)

proof

A4:
Family_open_set PM c= the topology of T
let x, y be Element of PM; :: thesis: pmet . (x,y) = dist (x,y)

PM = MetrStruct(# the carrier of T,pmet #) by A1, PCOMPS_1:def 7;

hence pmet . (x,y) = dist (x,y) by METRIC_1:def 1; :: thesis: verum

end;PM = MetrStruct(# the carrier of T,pmet #) by A1, PCOMPS_1:def 7;

hence pmet . (x,y) = dist (x,y) by METRIC_1:def 1; :: thesis: verum

proof

the topology of T c= Family_open_set PM
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Family_open_set PM or A in the topology of T )

assume A5: A in Family_open_set PM ; :: thesis: A in the topology of T

then reconsider AT = A as Subset of T by A1, PCOMPS_2:4;

end;assume A5: A in Family_open_set PM ; :: thesis: A in the topology of T

then reconsider AT = A as Subset of T by A1, PCOMPS_2:4;

per cases
( AT ` is empty or not AT ` is empty )
;

end;

suppose
AT ` is empty
; :: thesis: A in the topology of T

then
AT ` = ([#] T) `
by XBOOLE_1:37;

then AT = the carrier of T by TOPS_1:1;

hence A in the topology of T by PRE_TOPC:def 1; :: thesis: verum

end;then AT = the carrier of T by TOPS_1:1;

hence A in the topology of T by PRE_TOPC:def 1; :: thesis: verum

suppose A6:
not AT ` is empty
; :: thesis: A in the topology of T

for x being set holds

( x in AT iff ex U being Subset of T st

( U is open & U c= AT & x in U ) )

hence A in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;( x in AT iff ex U being Subset of T st

( U is open & U c= AT & x in U ) )

proof

then
AT is open
by TOPS_1:25;
let x be set ; :: thesis: ( x in AT iff ex U being Subset of T st

( U is open & U c= AT & x in U ) )

( x in AT implies ex U being Subset of T st

( U is open & U c= AT & x in U ) )

( U is open & U c= AT & x in U ) ) ; :: thesis: verum

end;( U is open & U c= AT & x in U ) )

( x in AT implies ex U being Subset of T st

( U is open & U c= AT & x in U ) )

proof

hence
( x in AT iff ex U being Subset of T st
assume A7:
x in AT
; :: thesis: ex U being Subset of T st

( U is open & U c= AT & x in U )

then reconsider xP = x as Element of PM by A1, PCOMPS_2:4;

consider r being Real such that

A8: r > 0 and

A9: Ball (xP,r) c= AT by A5, A7, PCOMPS_1:def 4;

reconsider xT = x as Element of T by A7;

A10: ex y being object st y in AT ` by A6;

reconsider B = Ball (xP,r) as Subset of T by A1, PCOMPS_2:4;

set Inf = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;

AT ` c= B ` by A9, SUBSET_1:12;

then consider b being set such that

A11: b in B ` by A10;

B ` = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }

then A24: B is open by TOPS_1:4;

pmet . (xT,xT) = 0 by A1, PCOMPS_1:def 6;

then dist (xP,xP) < r by A3, A8;

then xP in B by METRIC_1:11;

hence ex U being Subset of T st

( U is open & U c= AT & x in U ) by A9, A24; :: thesis: verum

end;( U is open & U c= AT & x in U )

then reconsider xP = x as Element of PM by A1, PCOMPS_2:4;

consider r being Real such that

A8: r > 0 and

A9: Ball (xP,r) c= AT by A5, A7, PCOMPS_1:def 4;

reconsider xT = x as Element of T by A7;

A10: ex y being object st y in AT ` by A6;

reconsider B = Ball (xP,r) as Subset of T by A1, PCOMPS_2:4;

set Inf = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;

AT ` c= B ` by A9, SUBSET_1:12;

then consider b being set such that

A11: b in B ` by A10;

B ` = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }

proof

then
B ` = Cl (B `)
by A2, A11;
thus
B ` c= { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
:: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } c= B `

assume y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ; :: thesis: y in B `

then consider yT being Point of T such that

A13: y = yT and

A14: (lower_bound (pmet,(B `))) . yT = 0 ;

assume not y in B ` ; :: thesis: contradiction

then A15: yT in B by A13, XBOOLE_0:def 5;

reconsider yP = yT as Point of PM by A1, PCOMPS_2:4;

pmet is_a_pseudometric_of the carrier of T by A1, Th9;

then A16: ( not (dist (pmet,yT)) .: (B `) is empty & (dist (pmet,yT)) .: (B `) is bounded_below ) by A11, Lm1;

Ball (xP,r) in Family_open_set PM by PCOMPS_1:29;

then consider s being Real such that

A17: s > 0 and

A18: Ball (yP,s) c= Ball (xP,r) by A15, PCOMPS_1:def 4;

lower_bound ((dist (pmet,yT)) .: (B `)) = 0 by A14, Def3;

then consider rn being Real such that

A19: rn in (dist (pmet,yT)) .: (B `) and

A20: rn < 0 + s by A17, A16, SEQ_4:def 2;

consider z being object such that

A21: z in dom (dist (pmet,yT)) and

A22: z in B ` and

A23: rn = (dist (pmet,yT)) . z by A19, FUNCT_1:def 6;

reconsider zT = z as Point of T by A21;

reconsider zP = z as Point of PM by A1, A21, PCOMPS_2:4;

pmet . (yT,zT) < s by A20, A23, Def2;

then dist (yP,zP) < s by A3;

then zP in Ball (yP,s) by METRIC_1:11;

then B ` meets B by A18, A22, XBOOLE_0:3;

hence contradiction by XBOOLE_1:79; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } or y in B ` )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B ` or y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } )

assume A12: y in B ` ; :: thesis: y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }

(lower_bound (pmet,(B `))) . y = 0 by A1, A12, Th6, Th9;

hence y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } by A12; :: thesis: verum

end;assume A12: y in B ` ; :: thesis: y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }

(lower_bound (pmet,(B `))) . y = 0 by A1, A12, Th6, Th9;

hence y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } by A12; :: thesis: verum

assume y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ; :: thesis: y in B `

then consider yT being Point of T such that

A13: y = yT and

A14: (lower_bound (pmet,(B `))) . yT = 0 ;

assume not y in B ` ; :: thesis: contradiction

then A15: yT in B by A13, XBOOLE_0:def 5;

reconsider yP = yT as Point of PM by A1, PCOMPS_2:4;

pmet is_a_pseudometric_of the carrier of T by A1, Th9;

then A16: ( not (dist (pmet,yT)) .: (B `) is empty & (dist (pmet,yT)) .: (B `) is bounded_below ) by A11, Lm1;

Ball (xP,r) in Family_open_set PM by PCOMPS_1:29;

then consider s being Real such that

A17: s > 0 and

A18: Ball (yP,s) c= Ball (xP,r) by A15, PCOMPS_1:def 4;

lower_bound ((dist (pmet,yT)) .: (B `)) = 0 by A14, Def3;

then consider rn being Real such that

A19: rn in (dist (pmet,yT)) .: (B `) and

A20: rn < 0 + s by A17, A16, SEQ_4:def 2;

consider z being object such that

A21: z in dom (dist (pmet,yT)) and

A22: z in B ` and

A23: rn = (dist (pmet,yT)) . z by A19, FUNCT_1:def 6;

reconsider zT = z as Point of T by A21;

reconsider zP = z as Point of PM by A1, A21, PCOMPS_2:4;

pmet . (yT,zT) < s by A20, A23, Def2;

then dist (yP,zP) < s by A3;

then zP in Ball (yP,s) by METRIC_1:11;

then B ` meets B by A18, A22, XBOOLE_0:3;

hence contradiction by XBOOLE_1:79; :: thesis: verum

then A24: B is open by TOPS_1:4;

pmet . (xT,xT) = 0 by A1, PCOMPS_1:def 6;

then dist (xP,xP) < r by A3, A8;

then xP in B by METRIC_1:11;

hence ex U being Subset of T st

( U is open & U c= AT & x in U ) by A9, A24; :: thesis: verum

( U is open & U c= AT & x in U ) ) ; :: thesis: verum

hence A in the topology of T by PRE_TOPC:def 2; :: thesis: verum

proof

then
the topology of T = Family_open_set PM
by A4;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of T or A in Family_open_set PM )

assume A25: A in the topology of T ; :: thesis: A in Family_open_set PM

then reconsider AT = A as Subset of T ;

reconsider AP = A as Subset of PM by A1, A25, PCOMPS_2:4;

end;assume A25: A in the topology of T ; :: thesis: A in Family_open_set PM

then reconsider AT = A as Subset of T ;

reconsider AP = A as Subset of PM by A1, A25, PCOMPS_2:4;

per cases
( AT ` is empty or not AT ` is empty )
;

end;

suppose
AT ` is empty
; :: thesis: A in Family_open_set PM

then
AT ` = ([#] T) `
by XBOOLE_1:37;

then AT = the carrier of T by TOPS_1:1;

then AT = the carrier of PM by A1, PCOMPS_2:4;

hence A in Family_open_set PM by PCOMPS_1:30; :: thesis: verum

end;then AT = the carrier of T by TOPS_1:1;

then AT = the carrier of PM by A1, PCOMPS_2:4;

hence A in Family_open_set PM by PCOMPS_1:30; :: thesis: verum

suppose A26:
not AT ` is empty
; :: thesis: A in Family_open_set PM

for xP being Element of PM st xP in AP holds

ex r being Real st

( r > 0 & Ball (xP,r) c= AP )

end;ex r being Real st

( r > 0 & Ball (xP,r) c= AP )

proof

hence
A in Family_open_set PM
by PCOMPS_1:def 4; :: thesis: verum
let xP be Element of PM; :: thesis: ( xP in AP implies ex r being Real st

( r > 0 & Ball (xP,r) c= AP ) )

assume A27: xP in AP ; :: thesis: ex r being Real st

( r > 0 & Ball (xP,r) c= AP )

reconsider xT = xP as Element of T by A1, PCOMPS_2:4;

take r = (lower_bound (pmet,(AT `))) . xT; :: thesis: ( r > 0 & Ball (xP,r) c= AP )

A28: Ball (xP,r) c= AP

then AT ` = Cl (AT `) by PRE_TOPC:22;

then A35: AT ` = { p where p is Point of T : (lower_bound (pmet,(AT `))) . p = 0 } by A2, A26;

(lower_bound (pmet,(AT `))) . xT > 0

end;( r > 0 & Ball (xP,r) c= AP ) )

assume A27: xP in AP ; :: thesis: ex r being Real st

( r > 0 & Ball (xP,r) c= AP )

reconsider xT = xP as Element of T by A1, PCOMPS_2:4;

take r = (lower_bound (pmet,(AT `))) . xT; :: thesis: ( r > 0 & Ball (xP,r) c= AP )

A28: Ball (xP,r) c= AP

proof

AT is open
by A25, PRE_TOPC:def 2;
pmet is_a_pseudometric_of the carrier of T
by A1, Th9;

then A29: ( not (dist (pmet,xT)) .: (AT `) is empty & (dist (pmet,xT)) .: (AT `) is bounded_below ) by A26, Lm1;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (xP,r) or y in AP )

assume that

A30: y in Ball (xP,r) and

A31: not y in AP ; :: thesis: contradiction

reconsider yP = y as Point of PM by A30;

A32: dist (xP,yP) < r by A30, METRIC_1:11;

reconsider yT = yP as Point of T by A1, PCOMPS_2:4;

A33: dom (dist (pmet,xT)) = the carrier of T by FUNCT_2:def 1;

yT in AT ` by A31, XBOOLE_0:def 5;

then (dist (pmet,xT)) . yT in (dist (pmet,xT)) .: (AT `) by A33, FUNCT_1:def 6;

then A34: lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT by A29, SEQ_4:def 2;

( (dist (pmet,xT)) . yT = pmet . (xT,yT) & lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT ) by Def2, Def3;

hence contradiction by A3, A32, A34; :: thesis: verum

end;then A29: ( not (dist (pmet,xT)) .: (AT `) is empty & (dist (pmet,xT)) .: (AT `) is bounded_below ) by A26, Lm1;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (xP,r) or y in AP )

assume that

A30: y in Ball (xP,r) and

A31: not y in AP ; :: thesis: contradiction

reconsider yP = y as Point of PM by A30;

A32: dist (xP,yP) < r by A30, METRIC_1:11;

reconsider yT = yP as Point of T by A1, PCOMPS_2:4;

A33: dom (dist (pmet,xT)) = the carrier of T by FUNCT_2:def 1;

yT in AT ` by A31, XBOOLE_0:def 5;

then (dist (pmet,xT)) . yT in (dist (pmet,xT)) .: (AT `) by A33, FUNCT_1:def 6;

then A34: lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT by A29, SEQ_4:def 2;

( (dist (pmet,xT)) . yT = pmet . (xT,yT) & lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT ) by Def2, Def3;

hence contradiction by A3, A32, A34; :: thesis: verum

then AT ` = Cl (AT `) by PRE_TOPC:22;

then A35: AT ` = { p where p is Point of T : (lower_bound (pmet,(AT `))) . p = 0 } by A2, A26;

(lower_bound (pmet,(AT `))) . xT > 0

proof

hence
( r > 0 & Ball (xP,r) c= AP )
by A28; :: thesis: verum
assume
(lower_bound (pmet,(AT `))) . xT <= 0
; :: thesis: contradiction

then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;

then xT in AT ` by A35;

then AT ` meets AT by A27, XBOOLE_0:3;

hence contradiction by XBOOLE_1:79; :: thesis: verum

end;then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;

then xT in AT ` by A35;

then AT ` meets AT by A27, XBOOLE_0:3;

hence contradiction by XBOOLE_1:79; :: thesis: verum

hence T is metrizable by A1, PCOMPS_1:def 8; :: thesis: verum