let T be non empty TopSpace; :: thesis: for r being Real
for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds
min (r,m) is_metric_of the carrier of T
let r be Real; :: thesis: for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds
min (r,m) is_metric_of the carrier of T
let m be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( r > 0 & m is_metric_of the carrier of T implies min (r,m) is_metric_of the carrier of T )
assume that
A1: r > 0 and
A2: m is_metric_of the carrier of T ; :: thesis: min (r,m) is_metric_of the carrier of T
let a, b, c be Element of T; :: according to PCOMPS_1:def 6 :: thesis: ( ( not (min (r,m)) . (a,b) = 0 or a = b ) & ( not a = b or (min (r,m)) . (a,b) = 0 ) & (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) )
for a, b, c being Element of T holds
( m . (a,a) = 0 & m . (a,b) = m . (b,a) & m . (a,c) <= (m . (a,b)) + (m . (b,c)) ) by A2;
then m is_a_pseudometric_of the carrier of T by Lm8;
then A3: min (r,m) is_a_pseudometric_of the carrier of T by A1, Th30;
( (min (r,m)) . (a,b) = 0 implies a = b )
proof
assume (min (r,m)) . (a,b) = 0 ; :: thesis: a = b
then min (r,(m . (a,b))) = 0 by Lm9;
then m . (a,b) = 0 by A1, XXREAL_0:def 9;
hence a = b by A2; :: thesis: verum
end;
hence ( (min (r,m)) . (a,b) = 0 iff a = b ) by A3, Lm8; :: thesis: ( (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) )
thus ( (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) ) by A3, Lm8; :: thesis: verum