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_a_pseudometric_of the carrier of T holds
min (r,m) is_a_pseudometric_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_a_pseudometric_of the carrier of T holds
min (r,m) is_a_pseudometric_of the carrier of T
let m be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( r > 0 & m is_a_pseudometric_of the carrier of T implies min (r,m) is_a_pseudometric_of the carrier of T )
assume that
A1: r > 0 and
A2: m is_a_pseudometric_of the carrier of T ; :: thesis: min (r,m) is_a_pseudometric_of the carrier of T
now :: thesis: for a, b, c being Element of T holds
( (min (r,m)) . (a,a) = 0 & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) )
let a, b, c be Element of T; :: thesis: ( (min (r,m)) . (a,a) = 0 & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) )
m . (a,a) = 0 by A2, Th28;
then min (r,(m . (a,a))) = 0 by A1, XXREAL_0:def 9;
hence (min (r,m)) . (a,a) = 0 by Lm9; :: thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b))
thus (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) :: thesis: verum
proof
now :: thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b))
per cases ( ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) >= r or ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) < r ) ;
suppose A3: ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) >= r ; :: thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b))
min (r,(m . (a,c))) <= r by XXREAL_0:17;
then (min (r,m)) . (a,c) <= r by Lm9;
hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) by A3, XXREAL_0:2; :: thesis: verum
end;
suppose A4: ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) < r ; :: thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b))
m . (c,b) >= 0 by A2, Th29;
then 0 <= min (r,(m . (c,b))) by A1, XXREAL_0:20;
then A5: 0 <= (min (r,m)) . (c,b) by Lm9;
m . (a,b) >= 0 by A2, Th29;
then 0 <= min (r,(m . (a,b))) by A1, XXREAL_0:20;
then A6: 0 <= (min (r,m)) . (a,b) by Lm9;
then (min (r,m)) . (a,b) < r by A4, A5, Lm1;
then min (r,(m . (a,b))) < r by Lm9;
then min (r,(m . (a,b))) = m . (a,b) by XXREAL_0:def 9;
then A7: (min (r,m)) . (a,b) = m . (a,b) by Lm9;
(min (r,m)) . (c,b) < r by A4, A6, A5, Lm1;
then min (r,(m . (c,b))) < r by Lm9;
then min (r,(m . (c,b))) = m . (c,b) by XXREAL_0:def 9;
then A8: (min (r,m)) . (c,b) = m . (c,b) by Lm9;
( min (r,(m . (a,c))) <= m . (a,c) & m . (a,c) <= (m . (a,b)) + (m . (c,b)) ) by A2, Th28, XXREAL_0:17;
then min (r,(m . (a,c))) <= (m . (a,b)) + (m . (c,b)) by XXREAL_0:2;
hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) by A7, A8, Lm9; :: thesis: verum
end;
end;
end;
hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) ; :: thesis: verum
end;
end;
hence min (r,m) is_a_pseudometric_of the carrier of T by Th28; :: thesis: verum