set ff = SteinhausGen (f,p);
for x, z, y being Element of X holds ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
proof
let x, z, y be Element of X; :: thesis: ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
set b = 2 * (f . (x,y));
set cc = ((f . (x,p)) + (f . (y,p))) + (f . (x,y));
set dxz = 2 * (f . (x,z));
set dyz = 2 * (f . (y,z));
set pp = f . (x,y);
set q = (f . (x,y)) + ((f . (x,p)) + (f . (y,p)));
set r = ((f . (x,z)) + (f . (y,z))) - (f . (x,y));
per cases ( x = y or x = z or y = z or ( x <> y & x <> z & y <> z ) ) ;
suppose x = y ; :: thesis: ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
then F1: (SteinhausGen (f,p)) . (x,y) = 0 by METRIC_1:def 2;
( (SteinhausGen (f,p)) . (x,z) >= 0 & (SteinhausGen (f,p)) . (z,y) >= 0 ) by ZeZo;
hence ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y) by F1; :: thesis: verum
end;
suppose F0: x = z ; :: thesis: ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
then (SteinhausGen (f,p)) . (x,z) = 0 by METRIC_1:def 2;
hence ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y) by F0; :: thesis: verum
end;
suppose F0: y = z ; :: thesis: ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
then (SteinhausGen (f,p)) . (y,z) = 0 by METRIC_1:def 2;
hence ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y) by F0; :: thesis: verum
end;
suppose TT: ( x <> y & x <> z & y <> z ) ; :: thesis: ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y)
then TX: f . (x,y) > 0 by ME7;
f . (y,p) = f . (p,y) by METRIC_1:def 4;
then (f . (x,p)) + (f . (y,p)) > 0 by TX, METRIC_1:def 5;
then Y1: f . (x,y) < (f . (x,y)) + ((f . (x,p)) + (f . (y,p))) by XREAL_1:29;
E1: f . (x,y) > 0 by TT, ME7;
f . (y,z) = f . (z,y) by METRIC_1:def 4;
then ((f . (x,z)) + (f . (y,z))) - (f . (x,y)) >= (f . (x,y)) - (f . (x,y)) by XREAL_1:9, METRIC_1:def 5;
then XX: (f . (x,y)) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) <= ((f . (x,y)) + (((f . (x,z)) + (f . (y,z))) - (f . (x,y)))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,y))) + (((f . (x,z)) + (f . (y,z))) - (f . (x,y)))) by LemacikX1, Y1, E1;
S3: (SteinhausGen (f,p)) . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) by SteinGen;
2 * ((f . (x,y)) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))) <= 2 * (((f . (x,z)) + (f . (y,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) by XX, XREAL_1:64;
then (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) <= 2 * (((f . (x,z)) + (f . (y,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) by XCMPLX_1:74;
then ds: (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) <= (2 * ((f . (x,z)) + (f . (y,z)))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))) by XCMPLX_1:74;
Sc: f . (x,z) > 0 by ME7, TT;
SC: f . (y,z) > 0 by TT, ME7;
S0: ((2 * (f . (x,z))) + (2 * (f . (y,z)))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))) = ((2 * (f . (x,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) + ((2 * (f . (y,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) by XCMPLX_1:62;
R1: (SteinhausGen (f,p)) . (x,z) = (2 * (f . (x,z))) / (((f . (x,p)) + (f . (z,p))) + (f . (x,z))) by SteinGen;
f . (z,y) = f . (y,z) by METRIC_1:def 4;
then ((f . (y,z)) + (f . (y,p))) - (f . (z,p)) >= (f . (z,p)) - (f . (z,p)) by XREAL_1:9, METRIC_1:def 5;
then (f . (x,z)) + (((f . (y,z)) + (f . (y,p))) - (f . (z,p))) >= (f . (x,z)) + 0 by XREAL_1:6;
then D1: ((f . (x,p)) + (f . (z,p))) + ((((f . (x,z)) + (f . (y,z))) + (f . (y,p))) - (f . (z,p))) >= ((f . (x,p)) + (f . (z,p))) + (f . (x,z)) by XREAL_1:6;
ss: f . (z,p) = f . (p,z) by METRIC_1:def 4;
then (f . (x,p)) + (f . (z,p)) > 0 by Sc, METRIC_1:def 5;
then W3: (2 * (f . (x,z))) / ((((((f . (x,p)) + (f . (z,p))) + (f . (x,z))) + (f . (y,z))) + (f . (y,p))) - (f . (z,p))) <= (2 * (f . (x,z))) / (((f . (x,p)) + (f . (z,p))) + (f . (x,z))) by D1, XREAL_1:118, Sc;
f2: (f . (y,p)) + (f . (z,p)) > 0 by SC, METRIC_1:def 5, ss;
f . (x,z) = f . (z,x) by METRIC_1:def 4;
then ((f . (x,z)) + (f . (x,p))) - (f . (z,p)) >= (f . (z,p)) - (f . (z,p)) by XREAL_1:9, METRIC_1:def 5;
then (((f . (x,z)) + (f . (x,p))) - (f . (z,p))) + (f . (y,z)) >= 0 + (f . (y,z)) by XREAL_1:6;
then ((f . (y,p)) + (f . (z,p))) + ((((f . (y,z)) + (f . (x,z))) + (f . (x,p))) - (f . (z,p))) >= ((f . (y,p)) + (f . (z,p))) + (f . (y,z)) by XREAL_1:6;
then w3: (2 * (f . (y,z))) / ((((((f . (y,p)) + (f . (z,p))) + (f . (y,z))) + (f . (x,z))) + (f . (x,p))) - (f . (z,p))) <= (2 * (f . (y,z))) / (((f . (y,p)) + (f . (z,p))) + (f . (y,z))) by XREAL_1:118, f2, SC;
R2: (SteinhausGen (f,p)) . (z,y) = (2 * (f . (z,y))) / (((f . (z,p)) + (f . (y,p))) + (f . (z,y))) by SteinGen;
( f . (y,p) = f . (p,y) & f . (z,p) = f . (p,z) & f . (y,z) = f . (z,y) ) by METRIC_1:def 4;
then ((2 * (f . (x,z))) + (2 * (f . (y,z)))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))) <= ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) by R1, W3, S0, XREAL_1:7, w3, R2;
hence ((SteinhausGen (f,p)) . (x,z)) + ((SteinhausGen (f,p)) . (z,y)) >= (SteinhausGen (f,p)) . (x,y) by S3, ds, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence SteinhausGen (f,p) is triangle by METRIC_1:def 5; :: thesis: verum