let D be set ; :: thesis: for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
let f be Function of [:D,D:],REAL; :: thesis: ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
set DF = MetrStruct(# D,f #);
A1: ( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )

proof

assume MetrStruct(# D,f #) is MetrSpace ; :: thesis: f is_metric_of D
then reconsider DF = MetrStruct(# D,f #) as MetrSpace ;
for a, b, c being Element of DF holds
( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )

proof

let a, b, c be Element of DF; :: thesis: ( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
A2: the distance of DF . (a,b) = dist (a,b) by METRIC_1:def 1;
hence ( the distance of DF . (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; :: thesis: ( the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
the distance of DF . (b,a) = dist (b,a) by METRIC_1:def 1;
hence the distance of DF . (a,b) = the distance of DF . (b,a) by A2; :: thesis: the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c))
( the distance of DF . (a,c) = dist (a,c) & the distance of DF . (b,c) = dist (b,c) ) by METRIC_1:def 1;
hence the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) by A2, METRIC_1:4; :: thesis: verum

end;

hence f is_metric_of D ; :: thesis: verum

end;

( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )

proof

assume A3: f is_metric_of D ; :: thesis: MetrStruct(# D,f #) is MetrSpace
for a, b, c being Element of MetrStruct(# D,f #) holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )

proof

let a, b, c be Element of MetrStruct(# D,f #); :: thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A4: the distance of MetrStruct(# D,f #) . (a,b) = dist (a,b) by METRIC_1:def 1;
hence ( dist (a,b) = 0 iff a = b ) by A3; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
the distance of MetrStruct(# D,f #) . (b,a) = dist (b,a) by METRIC_1:def 1;
hence dist (a,b) = dist (b,a) by A3, A4; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
( the distance of MetrStruct(# D,f #) . (a,c) = dist (a,c) & the distance of MetrStruct(# D,f #) . (b,c) = dist (b,c) ) by METRIC_1:def 1;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A4; :: thesis: verum

end;

hence MetrStruct(# D,f #) is MetrSpace by METRIC_1:6; :: thesis: verum

end;

hence ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace ) by A1; :: thesis: verum