Copyright (c) 1991 Association of Mizar Users
environ
vocabulary METRIC_1, FUNCT_1, SQUARE_1, ARYTM_1, ABSVALUE, METRIC_4;
notation ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, FUNCT_2, ABSVALUE,
STRUCT_0, METRIC_1, DOMAIN_1, SQUARE_1;
constructors REAL_1, ABSVALUE, METRIC_1, DOMAIN_1, SQUARE_1, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, METRIC_1, METRIC_3, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems BINOP_1, DOMAIN_1, ZFMISC_1, METRIC_1, METRIC_3, REAL_1, MCART_1,
AXIOMS, SQUARE_1, ABSVALUE, XCMPLX_0, XCMPLX_1;
schemes METRIC_3;
begin :: METRICS IN THE CARTESIAN PRODUCT OF TWO SETS
reserve X,Y for non empty MetrSpace;
reserve x1,y1,z1 for Element of X;
reserve x2,y2,z2 for Element of Y;
definition let X,Y;
func dist_cart2S(X,Y) -> Function of [:[:the carrier of X,the carrier of Y:],
[:the carrier of X,the carrier of Y:]:],REAL means
:Def1:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x,y being Element of [:the carrier of X,the carrier of Y:]
st ( x = [x1,x2] & y = [y1,y2] ) holds
it.(x,y) =sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2));
existence
proof
deffunc G(Element of X,Element of X,
Element of Y,Element of Y) =
sqrt((dist($1,$2))^2 + (dist($3,$4)^2));
consider F being Function of [:[:the carrier of X,the carrier of Y:],
[:the carrier of X,the carrier of Y:]:],REAL
such that
A1:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x,y being Element of [:the carrier of X,the carrier of Y:]
st ( x = [x1,x2] & y = [y1,y2] )
holds
F.[x,y] = G(x1,y1,x2,y2) from LambdaMCART;
take F;
let x1,y1 be Element of X,
x2,y2 be Element of Y,
x,y be Element of [:the carrier of X,the carrier of Y:] such that
A2: ( x = [x1,x2] & y = [y1,y2] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of [:[:the carrier of X,the carrier of Y:],
[:the carrier of X,the carrier of Y:]:],REAL;
assume that
A3:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x,y being Element of [:the carrier of X,the carrier of Y:]
st (x = [x1,x2] & y = [y1,y2])
holds
f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) and
A4:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x,y being Element of [:the carrier of X,the carrier of Y:]
st (x = [x1,x2] & y = [y1,y2])
holds
f2.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2);
for x,y being Element of [:the carrier of X,the carrier of Y:]
holds f1.(x,y) = f2.(x,y)
proof let x,y be Element of [:the carrier of X,the carrier of Y:];
consider x1 be Element of X,
x2 be Element of Y
such that
A5: x = [x1,x2] by DOMAIN_1:9;
consider y1 be Element of X,
y2 be Element of Y
such that
A6: y = [y1,y2] by DOMAIN_1:9;
thus f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
reserve a,b for Element of REAL;
canceled;
theorem
Th2:for a,b being Element of REAL
st 0 <= a & 0 <= b holds
sqrt(a + b) = 0 iff ( a = 0 & b = 0)
proof
let a,b such that A1: 0 <= a & 0 <= b;
thus sqrt(a + b) = 0 implies (a = 0 & b = 0)
proof
assume
A2:sqrt(a + b) = 0;
0 + 0 <= a + b by A1,REAL_1:55;
then a + b = 0 by A2,SQUARE_1:92;
hence thesis by A1,METRIC_3:2;
end;
thus a = 0 & b = 0 implies sqrt(a + b) = 0 by SQUARE_1:82;
end;
theorem Th3:
for x,y being Element of [:the carrier of X,the carrier of Y:]
st (x = [x1,x2] & y = [y1,y2]) holds
dist_cart2S(X,Y).(x,y) = 0 iff x = y
proof
let x,y be Element of [:the carrier of X,the carrier of Y:] such that
A1:x = [x1,x2] & y = [y1,y2];
thus dist_cart2S(X,Y).(x,y) = 0 implies x = y
proof
assume A2:dist_cart2S(X,Y).(x,y) = 0;
set d1 = dist(x1,y1);
set d2 = dist(x2,y2);
A3:sqrt(d1^2 + d2^2) = 0 by A1,A2,Def1;
A4: 0 <= d1^2 by SQUARE_1:72;
A5: 0 <= d2^2 by SQUARE_1:72;
then A6:d1^2 = 0 & d2^2 = 0 by A3,A4,Th2;
d1^2 = 0 by A3,A4,A5,Th2;
then d1 = 0 by SQUARE_1:73;
then A7: x1 = y1 by METRIC_1:2;
d2 = 0 by A6,SQUARE_1:73;
hence thesis by A1,A7,METRIC_1:2;
end;
assume x = y;
then A8:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
then A9:(dist(x1,y1))^2 = 0 by METRIC_1:1,SQUARE_1:60;
A10: (dist(x2,y2))^2 = 0 by A8,METRIC_1:1,SQUARE_1:60;
dist_cart2S(X,Y).(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2)
by A1,Def1
.= 0 by A9,A10,Th2;
hence thesis;
end;
theorem Th4:
for x,y being Element of [:the carrier of X,the carrier of Y:]
st (x = [x1,x2] & y = [y1,y2]) holds
dist_cart2S(X,Y).(x,y) = dist_cart2S(X,Y).(y,x)
proof
let x,y be Element of [:the carrier of X,the carrier of Y:]; assume
A1:x = [x1,x2] & y = [y1,y2];
then dist_cart2S(X,Y).(x,y) = sqrt((dist(y1,x1))^2 + (dist(x2,y2))^2)
by Def1
.= dist_cart2S(X,Y).(y,x) by A1,Def1;
hence thesis;
end;
theorem Th5:
for a,b,c,d being Element of REAL
st (0 <= a & 0 <= b & 0 <= c & 0 <= d)
holds
sqrt((a + c)^2 + (b + d)^2) <= sqrt(a^2 + b^2) + sqrt(c^2 + d^2)
proof
let a,b,c,d be Element of REAL such that
A1: 0 <= a & 0 <= b & 0 <= c & 0 <= d;
0 <= ((a*d) - (c*b))^2 by SQUARE_1:72;
then 0 <= (a*d)^2 - 2*(a*d)*(c*b) + (c*b)^2 by SQUARE_1:64;
then 0 <= a^2*d^2 - 2*(a*d)*(c*b) + (c*b)^2 by SQUARE_1:68;
then 0 <= a^2*d^2 - 2*(a*d)*(c*b) + c^2*b^2 by SQUARE_1:68;
then 0 <= a^2*d^2 + (- 2*(a*d)*(c*b)) + c^2*b^2 by XCMPLX_0:def 8;
then 0 <= a^2*d^2 + c^2*b^2 + (- 2*(a*d)*(c*b)) by XCMPLX_1:1;
then 0 <= (a^2*d^2 + c^2*b^2) - 2*(a*d)*(c*b) by XCMPLX_0:def 8;
then 0 + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) by REAL_1:84;
then (b^2*d^2) + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) + (b^2*d^2
) by AXIOMS:24;
then (a^2*c^2) + ((b^2*d^2) + (2*(a*d)*(c*b))) <=
(a^2*c^2) + ((b^2*d^2) + (a^2*d^2 + c^2*b^2)) by AXIOMS:24;
then (a^2*c^2) + (2*(a*d)*(c*b) + (b^2*d^2)) <=
(a^2*c^2) + (a^2*d^2 + c^2*b^2) + (b^2*d^2) by XCMPLX_1:1
;
then (a^2*c^2) + (2*(a*d)*(c*b) + b^2*d^2) <=
(a^2*c^2 + a^2*d^2) + c^2*b^2 + (b^2*d^2) by XCMPLX_1:1;
then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
(a^2*(c^2 + d^2)) + c^2*b^2 + d^2*b^2 by XCMPLX_1:8
;
then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
(a^2*(c^2 + d^2)) + (c^2*b^2 + d^2*b^2
) by XCMPLX_1:1;
then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
(a^2*(c^2 + d^2)) + (b^2*(c^2 + d^2)) by XCMPLX_1:8
;
then a^2*c^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
a^2*(c^2 + d^2) + (b^2*(c^2 + d^2)) by XCMPLX_1:1;
then a^2*c^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:8;
then (a*c)^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
(a^2 + b^2)*(c^2 + d^2) by SQUARE_1:68;
then (a*c)^2 + 2*(a*d)*(c*b) + (b*d)^2 <=
(a^2 + b^2)*(c^2 + d^2) by SQUARE_1:68;
then (a*c)^2 + 2*((a*d)*(c*b)) + (b*d)^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
then (a*c)^2 + 2*(((a*d)*c)*b) + (b*d)^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
then (a*c)^2 + 2*(((a*c)*d)*b) + (b*d)^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
then (a*c)^2 + 2*((a*c)*(d*b)) + (b*d)^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
then (a*c)^2 + 2*(a*c)*(d*b) + (d*b)^2 <=
(a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
then A2: (a*c + d*b)^2 <= (a^2 + b^2)*(c^2 + d^2) by SQUARE_1:63;
0 <= (a*c + d*b)^2 by SQUARE_1:72;
then sqrt((a*c + d*b)^2) <= sqrt((a^2 + b^2)*(c^2 + d^2
)) by A2,SQUARE_1:94;
then A3: 2*sqrt((a*c + d*b)^2) <= 2*(sqrt((a^2 + b^2)*(c^2 + d^2)))
by AXIOMS:25;
A4: 0 <= a^2 by SQUARE_1:72;
0 <= b^2 by SQUARE_1:72;
then A5: 0 + 0 <= a^2 + b^2 by A4,REAL_1:55;
A6: 0 <= d^2 by SQUARE_1:72;
0 <= c^2 by SQUARE_1:72;
then A7: 0 + 0 <= c^2 + d^2 by A6,REAL_1:55;
then A8: 2*sqrt((a*c + d*b)^2) <= 2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2))
by A3,A5,SQUARE_1:97;
A9: 0 <= a*c by A1,SQUARE_1:19;
0 <= d*b by A1,SQUARE_1:19;
then 0 + 0 <= a*c + d*b by A9,REAL_1:55;
then 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
)) by A8,SQUARE_1:89;
then b^2 + 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)) + b^2
by AXIOMS:24;
then d^2 + (b^2 + 2*(a*c + d*b)) <=
d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2))) by AXIOMS:24;
then c^2 + (d^2 + (b^2 + 2*(a*c + d*b))) <=
(d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)))) + c^2 by AXIOMS:24;
then a^2 + (c^2 + (d^2 + (b^2 + 2*((a*c) + (d*b))))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by AXIOMS:24;
then a^2 + (c^2 + (d^2 + (b^2 + (2*(d*b) + 2*(a*c))))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:8;
then a^2 + (c^2 + (d^2 + ((b^2 + 2*(d*b)) + 2*(a*c)))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then a^2 + (c^2 + (2*(a*c) + (d^2 + (b^2 + 2*(d*b))))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then a^2 + ((c^2 + (2*(a*c) + (d^2 + b^2 + 2*(d*b))))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then a^2 + ((2*(a*c) +c^2) + (d^2 + b^2 + 2*(d*b))) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then (a^2 + (2*(a*c) + c^2)) + (d^2 + b^2 + 2*(d*b)) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then (a^2 + (2*(a*c) + c^2)) + (d^2 + (2*(d*b) + b^2)) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then (a^2 + 2*(a*c) + c^2) + (d^2 + (2*(d*b) + b^2)) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then (a^2 + 2*(a*c) + c^2) + (d^2 + 2*(d*b) + b^2) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
then (a^2 + 2*a*c + c^2) + (d^2 + 2*(d*b) + b^2) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:4;
then (a^2 + 2*a*c + c^2) + (d^2 + 2*d*b + b^2) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:4;
then (a + c)^2 + (d^2 + 2*d*b + b^2) <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by SQUARE_1:63;
then (a + c)^2 +(d + b)^2 <=
a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by SQUARE_1:63;
then (a + c)^2 + (d + b)^2 <=
a^2 + ((b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2))) + (c^2 + d^2
)) by XCMPLX_1:1;
then (a + c)^2 + (d + b)^2 <=
(a^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)))) + (c^2 + d^2
) by XCMPLX_1:1;
then (a + c)^2 + (d + b)^2 <=
(a^2 + b^2) + 2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2)) + (c^2 + d^2
) by XCMPLX_1:1;
then (a + c)^2 + (d + b)^2 <=
(sqrt(a^2 + b^2))^2 + 2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2)) + (c^2 + d^2)
by A5,SQUARE_1:def 4;
then (a + c)^2 + (d + b)^2 <= (sqrt(a^2 + b^2))^2 +
2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2)) + (sqrt(c^2 + d^2))^2
by A7,SQUARE_1:def 4;
then (a + c)^2 + (d + b)^2 <=
(sqrt(a^2 + b^2))^2 + 2*sqrt(a^2 + b^2)*sqrt(c^2 + d^2)
+ (sqrt(c^2 + d^2))^2 by XCMPLX_1:4;
then A10: (a + c)^2 + (d + b)^2 <=
(sqrt(a^2 + b^2) + sqrt(c^2 + d^2))^2 by SQUARE_1:63;
A11: 0 <= (a + c)^2 by SQUARE_1:72;
0 <= (d + b)^2 by SQUARE_1:72;
then 0 + 0 <= (a + c)^2 + (d + b)^2 by A11,REAL_1:55;
then A12: sqrt((a + c)^2 + (d + b)^2) <=
sqrt((sqrt(a^2 + b^2) + sqrt(c^2 + d^2))^2
) by A10,SQUARE_1:94;
A13: 0 <= sqrt(a^2 + b^2) by A5,SQUARE_1:def 4;
0 <= sqrt(c^2 + d^2) by A7,SQUARE_1:def 4;
then 0 + 0 <= sqrt(a^2 + b^2) + sqrt(c^2 + d^2) by A13,REAL_1:55;
hence thesis by A12,SQUARE_1:89;
end;
theorem Th6:
for x,y,z being Element of [:the carrier of X,the carrier of Y:]
st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
dist_cart2S(X,Y).(x,z) <= dist_cart2S(X,Y).(x,y) + dist_cart2S(X,Y).(y,z)
proof
let x,y,z be Element of [:the carrier of X,the carrier of Y:] such that
A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
set d1 = dist(x1,z1);
set d2 = dist(x1,y1);
set d3 = dist(y1,z1);
set d4 = dist(x2,z2);
set d5 = dist(x2,y2);
set d6 = dist(y2,z2);
A2: d1 <= d2 + d3 by METRIC_1:4;
0 <= d1 by METRIC_1:5;
then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
A4: d4 <= d5 + d6 by METRIC_1:4;
0 <= d4 by METRIC_1:5;
then (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
then A5: (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,REAL_1:55;
A6: 0 <= (d1)^2 by SQUARE_1:72;
0 <= (d4)^2 by SQUARE_1:72;
then 0 + 0 <= (d1)^2 + (d4)^2 by A6,REAL_1:55;
then A7: sqrt((d1)^2 + (d4)^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2)
by A5,SQUARE_1:94;
(0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6) by METRIC_1:5;
then sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2
+ d6^2)
by Th5;
then sqrt((d1)^2 + (d4)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2)
by A7,AXIOMS:22;
then dist_cart2S(X,Y).(x,z) <=
sqrt((d2)^2 + (d5)^2) + sqrt((d3)^2 + (d6)^2) by A1,Def1;
then dist_cart2S(X,Y).(x,z) <=
dist_cart2S(X,Y).(x,y) + sqrt((d3)^2 + (d6)^2) by A1,Def1;
hence thesis by A1,Def1;
end;
definition let X,Y;
let x,y be Element of [:the carrier of X,the carrier of Y:];
func dist2S(x,y) -> Real equals
dist_cart2S(X,Y).(x,y);
coherence;
end;
definition let X,Y;
func MetrSpaceCart2S(X,Y) -> strict non empty MetrSpace equals :Def3:
MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#);
reconsider x' = x,y' = y ,z' = z as Element of
[:the carrier of X,the carrier of Y:];
A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
A4: dist(x,y) = dist_cart2S(X,Y).(x',y') by METRIC_1:def 1;
A5: dist(x,z) = dist_cart2S(X,Y).(x',z') by METRIC_1:def 1;
A6: dist(y,z) = dist_cart2S(X,Y).(y',z') by METRIC_1:def 1;
A7: dist(y,x) = dist_cart2S(X,Y).(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th3;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th4;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th6;
end;
hence thesis by METRIC_1:6;
end;
end;
canceled;
theorem
MetrStruct(# [:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#)
is MetrSpace
proof
MetrStruct(# [:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#) =
MetrSpaceCart2S(X,Y) by Def3;
hence thesis;
end;
begin
:: METRICS IN THE CARTESIAN PRODUCT OF THREE SETS
reserve Z for non empty MetrSpace;
reserve x3,y3,z3 for Element of Z;
definition let X,Y,Z;
func dist_cart3S(X,Y,Z) -> Function of
[:[:the carrier of X,the carrier of Y,the carrier of Z:],
[:the carrier of X,the carrier of Y,the carrier of Z:]:],REAL means
:Def4:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x3,y3 being Element of Z
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st ( x = [x1,x2,x3] & y = [y1,y2,y3] ) holds
it.(x,y) =sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))
^2);
existence
proof
deffunc G(Element of X,Element of X,
Element of Y,Element of Y,
Element of Z,Element of Z)
= sqrt((dist($1,$2))^2 + (dist($3,$4))^2 + (dist($5,$6))^2);
consider F being Function of
[:[:the carrier of X,the carrier of Y,the carrier of Z:],
[:the carrier of X,the carrier of Y,the carrier of Z:]:],REAL
such that
A1:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x3,y3 being Element of Z
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st ( x = [x1,x2,x3] & y = [y1,y2,y3] )
holds
F.[x,y] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
take F;
let x1,y1 be Element of X,
x2,y2 be Element of Y,
x3,y3 be Element of Z,
x,y be Element of
[:the carrier of X,the carrier of Y,the carrier of Z:] such that
A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of
[:[:the carrier of X,the carrier of Y,the carrier of Z:],
[:the carrier of X,the carrier of Y,the carrier of Z:]:],REAL;
assume that
A3:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x3,y3 being Element of Z
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) and
A4:for x1,y1 being Element of X
for x2,y2 being Element of Y
for x3,y3 being Element of Z
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f2.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2
);
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
holds f1.(x,y) = f2.(x,y)
proof
let x,y be Element of
[:the carrier of X,the carrier of Y,the carrier of Z:];
consider x1 be Element of X,
x2 be Element of Y,
x3 be Element of Z
such that
A5: x = [x1,x2,x3] by DOMAIN_1:15;
consider y1 be Element of X,
y2 be Element of Y,
y3 be Element of Z
such that
A6: y = [y1,y2,y3] by DOMAIN_1:15;
thus f1.(x,y) =
sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
canceled;
theorem Th10:
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
dist_cart3S(X,Y,Z).(x,y) = 0 iff x = y
proof
let x,y be Element of
[:the carrier of X,the carrier of Y,the carrier of Z:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
thus dist_cart3S(X,Y,Z).(x,y) = 0 implies x = y
proof
assume A2:dist_cart3S(X,Y,Z).(x,y) = 0;
set d1 = dist(x1,y1);
set d2 = dist(x2,y2);
set d3 = dist(x3,y3);
sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,A2,Def4;
then A3: sqrt(d1^2 + (d2^2 + d3^2)) = 0 by XCMPLX_1:1;
A4: 0 <= d1^2 by SQUARE_1:72;
A5: 0 <= d2^2 by SQUARE_1:72;
0 <= d3^2 by SQUARE_1:72;
then A6: 0 + 0 <= d2^2 + d3^2 by A5,REAL_1:55;
then d1^2 = 0 & (d2^2 + d3^2) = 0 by A3,A4,Th2;
then d1 = 0 by SQUARE_1:73;
then A7: x1 = y1 by METRIC_1:2;
A8: d2^2 + d3^2 = 0 by A3,A4,A6,Th2;
A9: 0 <= d2^2 by SQUARE_1:72;
A10: 0 <= d3^2 by SQUARE_1:72;
then A11: d2^2 = 0 & d3^2 = 0 by A8,A9,METRIC_3:2;
d2^2 = 0 by A8,A9,A10,METRIC_3:2;
then d2 = 0 by SQUARE_1:73;
then A12:x2 = y2 by METRIC_1:2;
d3 = 0 by A11,SQUARE_1:73;
hence thesis by A1,A7,A12,METRIC_1:2;
end;
assume x = y;
then A13:x1 = y1 & x2 = y2 & x3 = y3 by A1,MCART_1:28;
then A14: (dist(x1,y1))^2 = 0 by METRIC_1:1,SQUARE_1:60;
A15: (dist(x2,y2))^2 = 0 by A13,METRIC_1:1,SQUARE_1:60;
dist_cart3S(X,Y,Z).(x,y) =
sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A1,Def4
.= 0 by A13,A14,A15,METRIC_1:1,SQUARE_1:60,82;
hence thesis;
end;
theorem Th11:
for x,y being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
dist_cart3S(X,Y,Z).(x,y) = dist_cart3S(X,Y,Z).(y,x)
proof
let x,y be Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]; assume
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
then dist_cart3S(X,Y,Z).(x,y) =
sqrt((dist(y1,x1))^2 + (dist(y2,x2))^2 + (dist(y3,x3))^2) by Def4
.= dist_cart3S(X,Y,Z).(y,x) by A1,Def4;
hence thesis;
end;
theorem Th12:
for a,b,c being Element of REAL holds
(a + b + c)^2 = a^2 + b^2 + c^2 + (2*a*b + 2*a*c + 2*b*c)
proof
let a,b,c be Element of REAL;
(a + b + c)^2 = (a + (b + c))^2 by XCMPLX_1:1
.= a^2 + 2*a*(b + c) + (b + c)^2 by SQUARE_1:63
.= a^2 + 2*a*(b + c) + (b^2 + 2*b*c + c^2) by SQUARE_1:63
.= a^2 + 2*a*(b + c) + (b^2 + (c^2 + 2*b*c)) by XCMPLX_1:1
.= ((a^2 + 2*a*(b + c)) + b^2) + (c^2 + 2*b*c) by XCMPLX_1:1
.= ((a^2 + b^2) + 2*a*(b + c)) + (c^2 + 2*b*c) by XCMPLX_1:1
.= ((a^2 + b^2) + 2*a*(b + c)) + c^2 + 2*b*c by XCMPLX_1:1
.= (((a^2 + b^2) + c^2) + 2*a*(b + c)) + 2*b*c by XCMPLX_1:1
.= ((a^2 + b^2) + c^2) + (2*a*(b + c) + 2*b*c) by XCMPLX_1:1
.= ((a^2 + b^2) + c^2
) + ((2*a*b + 2*a*c) + 2*b*c) by XCMPLX_1:8;
hence thesis;
end;
theorem Th13:
for a,b,c,d,e,f being Element of REAL holds
(2*(a*d)*(c*b) + 2*(a*f)*(e*c) + 2*(b*f)*(e*d)) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2)
proof
let a,b,c,d,e,f be Element of REAL;
A1:0 <= ((a*d) - (c*b))^2 by SQUARE_1:72;
A2:0 <= ((a*f) - (e*c))^2 by SQUARE_1:72;
0 <= ((b*f) - (e*d))^2 by SQUARE_1:72;
then 0 + 0 <= ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2
by A2,REAL_1:55;
then 0 + 0 <= ((a*d) - (c*b))^2 + (((a*f) - (e*c))^2 + ((b*f) - (e*d))^2)
by A1,REAL_1:55;
then 0 <= ((a*d) - (c*b))^2 + ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2
by XCMPLX_1:1;
then 0 <= ((a*d)^2 - 2*(a*d)*(c*b) + (c*b)^2) +
((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by SQUARE_1:64;
then 0 <= ((a*d)^2 + (-2*(a*d)*(c*b)) + (c*b)^2) +
((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by XCMPLX_0:def 8;
then 0 <= ((a*d)^2 + (c*b)^2) + (-2*(a*d)*(c*b)) +
((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by XCMPLX_1:1;
then 0 <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
(-2*(a*d)*(c*b)) + ((b*f) - (e*d))^2 by XCMPLX_1:1;
then 0 <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
((b*f) - (e*d))^2 + (-2*(a*d)*(c*b)) by XCMPLX_1:1;
then 0 <= (((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
((b*f) - (e*d))^2) - 2*(a*d)*(c*b) by XCMPLX_0:def 8;
then 0 + 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
((b*f) - (e*d))^2 by REAL_1:84;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
((a*f)^2 - 2*(a*f)*(e*c) + (e*c)^2) + ((b*f) - (e*d))^2 by SQUARE_1:64;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
((a*f)^2 + (- 2*(a*f)*(e*c)) + (e*c)^2) + ((b*f) - (e*d))^2
by XCMPLX_0:def 8
;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
(((a*f)^2 + (e*c)^2) + (- 2*(a*f)*(e*c))) + ((b*f) - (e*d))^2
by XCMPLX_1:1;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
((a*f)^2 + (e*c)^2) + (- 2*(a*f)*(e*c)) + ((b*f) - (e*d))^2
by XCMPLX_1:1;
then 2*(a*d)*(c*b) <= (a*d)^2 + (c*b)^2 +
((a*f)^2 + (e*c)^2) + ((b*f) - (e*d))^2
+ (- 2*(a*f)*(e*c)) by XCMPLX_1:1;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + ((b*f) - (e*d))^2
) + (- 2*(a*f)*(e*c)) by XCMPLX_1:1;
then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + ((b*f) - (e*d))^2
) - 2*(a*f)*(e*c) by XCMPLX_0:def 8;
then 2*(a*d)*(c*b) + 2*(a*f)*(e*c) <= (a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + ((b*f) - (e*d))^2 by REAL_1:84;
then 2*(a*d)*(c*b) + 2*(a*f)*(e*c) <= (a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + ((b*f)^2 - 2*(b*f)*(e*d) + (e*d)^2
) by SQUARE_1:64;
then 2*(a*d)*(c*b) + 2*(a*f)*(e*c) <= (a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + ((b*f)^2 + (- 2*(b*f)*(e*d)) + (e*d)^2
) by XCMPLX_0:def 8;
then 2*(a*d)*(c*b) + 2*(a*f)*(e*c) <= ((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2) + ((b*f)^2 + (e*d)^2
+ (- 2*(b*f)*(e*d))) by XCMPLX_1:1;
then 2*(a*d)*(c*b) + 2*(a*f)*(e*c) <= ((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2) + ((b*f)^2 + (e*d)^2
) + (- 2*(b*f)*(e*d)) by XCMPLX_1:1;
then (2*(a*d)*(c*b) + 2*(a*f)*(e*c)) <= ((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
+ (- 2*(b*f)*(e*d)) by XCMPLX_1:1;
then (2*(a*d)*(c*b) + 2*(a*f)*(e*c)) <= (((a*d)^2 + (c*b)^2 +
(a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) - 2*(b*f)*(e*d) by XCMPLX_0:def 8;
hence thesis by REAL_1:84;
end;
theorem Th14:
for a,b,c,d,e,f being Element of REAL holds
(((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
+ (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) =
(a^2 + b^2 + e^2)*(c^2 + d^2 + f^2)
proof
let a,b,c,d,e,f be Element of REAL;
(((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*
d
^2))
+ (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2)
= ((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
+ (e^2*f^2)) + (a^2*c^2) + (b^2*d^2) by XCMPLX_1:1
.= (((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
+ (a^2*c^2) + (e^2*f^2) + (b^2*d^2) by XCMPLX_1:1
.= (((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
+ (a^2*c^2) + (b^2*d^2) + (e^2*f^2) by XCMPLX_1:1
.= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2)
+ ((a^2*c^2) + (b^2*d^2)) + (e^2*f^2) by XCMPLX_1:1
.= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
+ ((a^2*c^2) + (b^2*d^2)) + (e^2*d^2) + (e^2*f^2) by XCMPLX_1:1
.= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
+ ((a^2*c^2) + (b^2*d^2)) + ((e^2*d^2) + (e^2*f^2)) by XCMPLX_1:1
.= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
+ ((a^2*c^2) + (b^2*d^2)) + (e^2*(d^2 + f^2)) by XCMPLX_1:8
.= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2) + (e^2*c^2)
+ ((a^2*c^2) + (b^2*d^2)) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2) + ((a^2*c^2) + (b^2*d^2
))
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + ((a^2*c^2) + (b^2*d^2)) + (b^2*f
^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*d^2) + ((a^2*c^2) + (b^2*d^2)) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f
^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*d^2) + (a^2*c^2) + (b^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*d^2) + (a^2*c^2) + (b^2*d^2) + (a^2*f^2) + (c^2*b^2) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= ((a^2*c^2) + (a^2*d^2)) + (a^2*f^2) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= (a^2*(c^2 + d^2)) + (a^2*f^2) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
.= (a^2*((c^2 + d^2) + f^2)) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
.= a^2*((c^2 + d^2) + f^2) + ((b^2*c^2) + (b^2*d^2)) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= a^2*((c^2 + d^2) + f^2) + (b^2*(c^2 + d^2)) + (b^2*f^2)
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
.= a^2*((c^2 + d^2) + f^2) + (b^2*(c^2 + d^2) + (b^2*f^2))
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
.= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2))
+ (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
.= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2))
+ ((e^2*c^2) + e^2*(d^2 + f^2)) by XCMPLX_1:1
.= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2)) + (e^2*(c^2 + (d^2
+ f^2)))
by XCMPLX_1:8
.= ((a^2 + b^2)*((c^2 + d^2) + f^2)) + e^2*(c^2 + (d^2 + f^2
)) by XCMPLX_1:8
.= (a^2 + b^2)*((c^2 + d^2) + f^2) + e^2*(c^2 + d^2 + f^2) by XCMPLX_1:1
.= (((a^2 + b^2) + e^2)*((c^2 + d^2) + f^2)) by XCMPLX_1:8;
hence thesis;
end;
theorem Th15:
for a,b,c,d,e,f being Element of REAL holds
((a*c) + (b*d) + (e*f))^2 <= (a^2 + b^2 + e^2)*(c^2 + d^2 + f^2)
proof
let a,b,c,d,e,f be Element of REAL;
(2*(a*d)*(c*b) + 2*(a*f)*(e*c) + 2*(b*f)*(e*d)) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2) by Th13;
then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*((b*f)*(d*e)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*(((b*f)*d)*e))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*(((b*d)*f)*e))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*((b*d)*(e*f)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*((a*f)*(c*e))) + (2*((b*d)*(e*f)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(((a*f)*c)*e)) + (2*((b*d)*(e*f)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(((a*c)*f)*e)) + (2*((b*d)*(e*f)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*((a*c)*(f*e))) + (2*((b*d)*(e*f)))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*((a*c)*(f*e))) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*d)*(c*b)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*((a*d)*(b*c))) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(((a*d)*b)*c)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(((a*b)*d)*c)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*((a*b)*(c*d))) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
then (e*f)^2 + ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f)) + (2*(b*d)*(e*f))) <=
(((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2)
+ (e*f)^2 by AXIOMS:24;
then (b*d)^2 + ((e*f)^2 + ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f)))) <= ((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2 by AXIOMS:24;
then (a*c)^2 + ((b*d)^2 + ((e*f)^2 + ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f))))) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)
^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by AXIOMS:24;
then (a*c)^2 + (b*d)^2 + ((e*f)^2 + ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f)))) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2
)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:1;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + ((2*(a*b)*(c*d)) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f))) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:1;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + ((2*((a*b)*(c*d))) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f))) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:4;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + ((2*(((a*b)*c)*d)) + (2*(a*c)*(e*f))
+ (2*(b*d)*(e*f))) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:4;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*(((a*c)*b)*d) + 2*(a*c)*(e*f)
+ 2*(b*d)*(e*f)) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:4;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*((a*c)*(b*d)) + 2*(a*c)*(e*f)
+ 2*(b*d)*(e*f)) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:4;
then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*(a*c)*(b*d) + 2*(a*c)*(e*f)
+ 2*(b*d)*(e*f)) <= (((((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by XCMPLX_1:4;
then A1:((a*c) + (b*d) + (e*f))^2 <= (((((a*d)^2 + (c*b)^2 + (a*f)^2
+ (e*c)^2
+ (b*f)^2) + (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by Th12;
set a1 = ((a*c) + (b*d) + (e*f))^2;
a1 <= (((((a^2*d^2) + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2)
+ (e*f)^2) + (b*d)^2) + (a*c)^2 by A1,SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a*f)^2 + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e*c)^2 + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b*f)^2)
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
+ (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
+ (e^2*d^2)) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
+ (e^2*d^2)) + (e^2*f^2)) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
+ (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a*c)^2 by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
+ (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) by SQUARE_1:68;
then a1 <= (((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2
))
+ (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) by XCMPLX_1:1;
hence thesis by Th14;
end;
Lm1:
for a,b,c,d,e,f being Element of REAL
st (0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f)
holds
sqrt((a + c)^2 + (b + d)^2 + (e + f)^2) <= sqrt(a^2 + b^2 + e^2) +
sqrt(c^2 + d^2 + f^2)
proof
let a,b,c,d,e,f be Element of REAL; assume
A1: 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f;
A2: ((a*c) + (b*d) + (e*f))^2 <= (a^2 + b^2 + e^2)*(c^2 + d^2 + f^2
) by Th15;
0 <= ((a*c) + (b*d) + (e*f))^2 by SQUARE_1:72;
then A3: sqrt(((a*c) + (b*d) + (e*f))^2) <=
sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f^2)) by A2,SQUARE_1:94;
A4: 0 <= a*c by A1,SQUARE_1:19;
A5: 0 <= b*d by A1,SQUARE_1:19;
0 <= e*f by A1,SQUARE_1:19;
then 0 + 0 <= b*d + e*f by A5,REAL_1:55;
then 0 + 0 <= a*c + (b*d + e*f) by A4,REAL_1:55;
then 0 <= a*c + b*d + e*f by XCMPLX_1:1;
then A6: ((a*c) + (b*d) + (e*f)) <= sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f
^2))
by A3,SQUARE_1:89;
A7: 0 <= a^2 by SQUARE_1:72;
0 <= b^2 by SQUARE_1:72;
then A8: 0 + 0 <= a^2 + b^2 by A7,REAL_1:55;
0 <= e^2 by SQUARE_1:72;
then A9: 0 + 0 <= (a^2 + b^2) + e^2 by A8,REAL_1:55;
A10: 0 <= c^2 by SQUARE_1:72;
0 <= d^2 by SQUARE_1:72;
then A11: 0 + 0 <= c^2 + d^2 by A10,REAL_1:55;
0 <= f^2 by SQUARE_1:72;
then A12: 0 + 0 <= (c^2 + d^2) + f^2 by A11,REAL_1:55;
then ((a*c) + (b*d) + (e*f)) <= sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f
^2)
by A6,A9,SQUARE_1:97;
then 2*((a*c) + (b*d) + (e*f)) <=
2*(sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) by AXIOMS:25;
then 2*(((a*c) + (b*d)) + (e*f)) <=
2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) by XCMPLX_1:4;
then (2*((a*c) + (b*d)) + 2*(e*f)) <=
2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) by XCMPLX_1:8;
then (2*((a*c) + (b*d)) + 2*(e*f)) + e^2
<= (2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2
by AXIOMS:24;
then (2*((a*c) + (b*d))) + (e^2 + 2*(e*f))
<= (2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2
by XCMPLX_1:1;
then ((2*((a*c) + (b*d))) + (e^2 + 2*(e*f))) + f^2
<= ((2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2) + f^2
by AXIOMS:24;
then (2*((a*c) + (b*d))) + (e^2 + 2*(e*f) + f^2)
<= ((2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2) + f^2
by XCMPLX_1:1;
then (2*((a*c) + (b*d))) + (e^2 + 2*e*f + f^2)
<= ((2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2) + f^2
by XCMPLX_1:4;
then (2*((a*c) + (b*d))) + ((e + f)^2)
<= ((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
by SQUARE_1:63;
then (2*(a*c) + 2*(b*d)) + ((e + f)^2)
<= ((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
by XCMPLX_1:8;
then ((2*(a*c) + 2*(b*d)) + ((e + f)^2)) + b^2
<= (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2) + b^2
by AXIOMS:24;
then ((2*(a*c) + 2*(b*d)) + b^2) + (e + f)^2
<= (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
) + b^2 by XCMPLX_1:1;
then (2*(a*c) + (b^2 + 2*(b*d))) + (e + f)^2
<= (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
) + b^2 by XCMPLX_1:1;
then ((2*(a*c) + (b^2 + 2*(b*d))) + (e + f)^2) + d^2
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by AXIOMS:24;
then ((2*(a*c) + (b^2 + 2*(b*d))) + d^2) + (e + f)^2
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by XCMPLX_1:1;
then (2*(a*c) + (b^2 + 2*(b*d) + d^2)) + (e + f)^2
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by XCMPLX_1:1;
then (2*(a*c) + (b^2 + 2*b*d + d^2)) + (e + f)^2
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by XCMPLX_1:4;
then (2*(a*c) + (b + d)^2) + (e + f)^2
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by SQUARE_1:63;
then 2*(a*c) + ((b + d)^2 + (e + f)^2)
<= (b^2 + (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
)) + d^2
by XCMPLX_1:1;
then 2*(a*c) + ((b + d)^2 + (e + f)^2)
<= b^2 + ((((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
) + d^2)
by XCMPLX_1:1;
then 2*(a*c) + ((b + d)^2 + (e + f)^2)
<= b^2 + ((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2
+ f^2)) by XCMPLX_1:1;
then a^2 + (2*(a*c) + ((b + d)^2 + (e + f)^2)) <= (b^2 +
((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
))) + a^2
by AXIOMS:24;
then (a^2 + 2*(a*c)) + ((b + d)^2 + (e + f)^2) <= a^2 + (b^2 +
((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)))
by XCMPLX_1:1;
then (a^2 + 2*(a*c)) + ((b + d)^2 + (e + f)^2) <= (a^2 + b^2) +
((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2))
by XCMPLX_1:1;
then (a^2 + 2*(a*c)) + ((b + d)^2 + (e + f)^2) <= ((a^2 + b^2) +
(e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + (d^2 + f^2)
by XCMPLX_1:1;
then (a^2 + 2*(a*c)) + ((b + d)^2 + (e + f)^2) <= ((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
) by XCMPLX_1:1;
then ((a^2 + 2*(a*c)) + ((b + d)^2 + (e + f)^2)) + c^2 <= (((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)) + c^2
by AXIOMS:24;
then ((a^2 + 2*(a*c) + c^2) + ((b + d)^2 + (e + f)^2)) <= (((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)) + c^2
by XCMPLX_1:1;
then ((a^2 + 2*a*c + c^2) + ((b + d)^2 + (e + f)^2)) <= (((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)) + c^2
by XCMPLX_1:4;
then ((a + c)^2 + ((b + d)^2 + (e + f)^2)) <= (((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)) + c^2 by SQUARE_1:63;
then ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (d^2 + f^2
)) + c^2
by XCMPLX_1:1;
then ((a + c)^2 + (b + d)^2 + (e + f)^2) <= ((a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + (c^2 + (d^2
+ f^2)) by XCMPLX_1:1;
then ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (a^2 + b^2 +
e^2) + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) + (c^2 + d^2 + f^2)
by XCMPLX_1:1;
then ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (sqrt(a^2 + b^2 + e^2))^2
+ 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) + (c^2 + d^2 + f^2)
by A9,SQUARE_1:def 4;
then ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (sqrt(a^2 + b^2 + e^2))^2
+ 2*sqrt(a^2 + b^2 + e^2)*(sqrt(c^2 + d^2 + f^2)) + (sqrt(c^2 + d^2
+ f^2))^2
by A12,SQUARE_1:def 4;
then A13: ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (sqrt(a^2 + b^2 + e^2)
+ sqrt(c^2 + d^2 + f^2))^2 by SQUARE_1:63;
A14: 0 <= (a + c)^2 by SQUARE_1:72;
0 <= (b + d)^2 by SQUARE_1:72;
then A15: 0 + 0 <= (a + c)^2 + (b + d)^2 by A14,REAL_1:55;
0 <= (e + f)^2 by SQUARE_1:72;
then 0 + 0 <= ((a + c)^2 + (b + d)^2) + (e + f)^2 by A15,REAL_1:55;
then A16: sqrt((a + c)^2 + (b + d)^2 + (e + f)^2) <= sqrt((sqrt(a^2 + b^2
+ e^2)
+ sqrt(c^2 + d^2 + f^2))^2) by A13,SQUARE_1:94;
A17: 0 <= sqrt(a^2 + b^2 + e^2) by A9,SQUARE_1:def 4;
0 <= sqrt(c^2 + d^2 + f^2) by A12,SQUARE_1:def 4;
then 0 + 0 <= (sqrt(a^2 + b^2 + e^2) + sqrt(c^2 + d^2 + f^2
)) by A17,REAL_1:55;
hence thesis by A16,SQUARE_1:89;
end;
theorem
Th16:
for x,y,z being Element of
[:the carrier of X,the carrier of Y,the carrier of Z:]
st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) holds
dist_cart3S(X,Y,Z).(x,z) <=
dist_cart3S(X,Y,Z).(x,y) + dist_cart3S(X,Y,Z).(y,z)
proof
let x,y,z be Element of
[:the carrier of X,the carrier of Y,the carrier of Z:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
set d1 = dist(x1,z1), d2 = dist(x1,y1), d3 = dist(y1,z1);
set d4 = dist(x2,z2), d5 = dist(x2,y2), d6 = dist(y2,z2);
set d7 = dist(x3,z3), d8 = dist(x3,y3), d9 = dist(y3,z3);
A2: d1 <= d2 + d3 by METRIC_1:4;
0 <= d1 by METRIC_1:5;
then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
A4: d4 <= d5 + d6 by METRIC_1:4;
0 <= d4 by METRIC_1:5;
then A5: (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
A6: d7 <= d8 + d9 by METRIC_1:4;
0 <= d7 by METRIC_1:5;
then A7: (d7)^2 <= (d8 + d9)^2 by A6,SQUARE_1:77;
(d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,A5,REAL_1:55;
then A8: (d1)^2 + (d4)^2 + (d7)^2 <= (d2 + d3)^2 + (d5 + d6)^2
+ (d8 + d9)^2
by A7,REAL_1:55;
A9: 0 <= (d1)^2 by SQUARE_1:72;
0 <= (d4)^2 by SQUARE_1:72;
then A10: 0 + 0 <= (d1)^2 + (d4)^2 by A9,REAL_1:55;
0 <= (d7)^2 by SQUARE_1:72;
then 0 + 0 <= ((d1)^2 + (d4)^2) + (d7)^2 by A10,REAL_1:55;
then A11: sqrt((d1)^2 + (d4)^2 + (d7)^2) <= sqrt((d2 + d3)^2 + (d5 + d6)
^2 +
(d8 + d9)^2) by A8,SQUARE_1:94;
(0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6 & 0 <= d8 & 0 <= d9)
by METRIC_1:5;
then sqrt((d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2) <= sqrt(d2^2 + d5^2
+ d8^2)
+ sqrt(d3^2 + d6^2 + d9^2) by Lm1;
then sqrt((d1)^2 + (d4)^2 + d7^2) <=
sqrt(d2^2 + d5^2 + d8^2) + sqrt(d3^2 + d6^2 + d9^2) by A11,AXIOMS:22;
then dist_cart3S(X,Y,Z).(x,z) <=
sqrt((d2)^2 + (d5)^2 + d8^2) + sqrt((d3)^2 + (d6)^2 + d9^2
) by A1,Def4;
then dist_cart3S(X,Y,Z).(x,z) <=
dist_cart3S(X,Y,Z).(x,y) + sqrt((d3)^2 + (d6)^2 + d9^2) by A1,Def4;
hence thesis by A1,Def4;
end;
definition let X,Y,Z;
let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:];
func dist3S(x,y) -> Real equals
dist_cart3S(X,Y,Z).(x,y);
coherence;
end;
definition let X,Y,Z;
func MetrSpaceCart3S(X,Y,Z) -> strict non empty MetrSpace equals :Def6:
MetrStruct(#[:the carrier of X,the carrier of Y,the carrier of Z:],
dist_cart3S(X,Y,Z)#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:the carrier of X,the carrier of Y,the carrier of Z:],
dist_cart3S(X,Y,Z)#);
reconsider x' = x,y' = y ,z' = z as Element of
[:the carrier of X,the carrier of Y,the carrier of Z:];
A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
A4: dist(x,y) = dist_cart3S(X,Y,Z).(x',y') by METRIC_1:def 1;
A5: dist(x,z) = dist_cart3S(X,Y,Z).(x',z') by METRIC_1:def 1;
A6: dist(y,z) = dist_cart3S(X,Y,Z).(y',z') by METRIC_1:def 1;
A7: dist(y,x) = dist_cart3S(X,Y,Z).(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th10;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th11;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th16;
end;
hence thesis by METRIC_1:6;
end;
end;
canceled;
theorem
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],
dist_cart3S(X,Y,Z)#)
is MetrSpace
proof
MetrStruct (# [:the carrier of X,the carrier of Y,the carrier of Z:],
dist_cart3S(X,Y,Z)#) = MetrSpaceCart3S(X,Y,Z) by Def6;
hence thesis;
end;
reserve x1,x2,y1,y2,z1,z2 for Element of REAL;
definition
func taxi_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
:Def7: for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
it.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2);
existence
proof
deffunc G(Element of REAL,Element of REAL,Element of REAL,Element of REAL)
= real_dist.($1,$2) + real_dist.($3,$4);
consider F being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL
such that
A1: for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
F.[x,y] = G(x1,y1,x2,y2) from LambdaMCART;
take F;
let x1,y1,x2,y2 be Element of REAL,
x,y be Element of [:REAL,REAL:] such that
A2: ( x = [x1,x2] & y = [y1,y2] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= real_dist.(x1,y1) + real_dist.(x2,y2) by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
assume that
A3:for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:] st (x = [x1,x2] & y = [y1,y2])
holds
f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) and
A4:for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:] st (x = [x1,x2] & y = [y1,y2])
holds
f2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2);
for x,y being Element of [:REAL,REAL:]
holds f1.(x,y) = f2.(x,y)
proof
let x,y be Element of [:REAL,REAL:];
consider x1 be Element of REAL,
x2 be Element of REAL
such that
A5: x = [x1,x2] by DOMAIN_1:9;
consider y1 be Element of REAL,
y2 be Element of REAL
such that
A6: y = [y1,y2] by DOMAIN_1:9;
thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th19:
for x1,x2,y1,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
taxi_dist2.(x,y) = 0 iff x = y
proof
let x1,x2,y1,y2 be Element of REAL,
x,y be Element of [:REAL,REAL:] such that
A1:x = [x1,x2] & y = [y1,y2];
thus taxi_dist2.(x,y) = 0 implies x = y
proof
assume A2:taxi_dist2.(x,y) = 0;
set d1 = real_dist.(x1,y1);
set d2 = real_dist.(x2,y2);
A3: d1 + d2 = 0 by A1,A2,Def7;
d1 = abs(x1 - y1) by METRIC_1:def 13;
then A4: 0 <= d1 by ABSVALUE:5;
d2 = abs(x2 - y2) by METRIC_1:def 13;
then A5: 0 <= d2 by ABSVALUE:5;
then A6:d1 = 0 & d2 = 0 by A3,A4,METRIC_3:2;
d1 = 0 by A3,A4,A5,METRIC_3:2;
then x1 = y1 by METRIC_1:9;
hence thesis by A1,A6,METRIC_1:9;
end;
assume x = y;
then A7:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
then A8:real_dist.(x2,y2) = 0 by METRIC_1:9;
taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A1,Def7
.= 0 by A7,A8,METRIC_1:9;
hence thesis;
end;
theorem Th20:
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
taxi_dist2.(x,y) = taxi_dist2.(y,x)
proof
let x,y be Element of [:REAL,REAL:]; assume
A1:x = [x1,x2] & y = [y1,y2];
then taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by Def7
.= real_dist.(y1,x1) + real_dist.(x2,y2) by METRIC_1:10
.= real_dist.(y1,x1) + real_dist.(y2,x2) by METRIC_1:10
.= taxi_dist2.(y,x) by A1,Def7;
hence thesis;
end;
theorem
Th21:
for x,y,z being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
taxi_dist2.(x,z) <= taxi_dist2.(x,y) + taxi_dist2.(y,z)
proof
let x,y,z be Element of [:REAL,REAL:] such that
A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
set d1 = real_dist.(x1,z1);
set d2 = real_dist.(x1,y1);
set d3 = real_dist.(y1,z1);
set d4 = real_dist.(x2,z2);
set d5 = real_dist.(x2,y2);
set d6 = real_dist.(y2,z2);
A2: (d2 + d3) + (d5 + d6) = ((d2 + d3) + d5) + d6 by XCMPLX_1:1
.= ((d2 + d5) + d3) + d6 by XCMPLX_1:1
.= (d2 + d5) + (d3 + d6) by XCMPLX_1:1
.= taxi_dist2.(x,y) + (d3 +d6) by A1,Def7
.= taxi_dist2.(x,y) + taxi_dist2.(y,z) by A1,Def7;
A3: d1 <= d2 + d3 by METRIC_1:11;
A4: d4 <= d5 + d6 by METRIC_1:11;
taxi_dist2.(x,z) = d1 + d4 by A1,Def7;
hence thesis by A2,A3,A4,REAL_1:55;
end;
definition
func RealSpaceCart2 -> strict non empty MetrSpace equals
MetrStruct(#[:REAL,REAL:],taxi_dist2#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:REAL,REAL:],taxi_dist2#);
reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL:];
A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
A4: dist(x,y) = taxi_dist2.(x',y') by METRIC_1:def 1;
A5: dist(x,z) = taxi_dist2.(x',z') by METRIC_1:def 1;
A6: dist(y,z) = taxi_dist2.(y',z') by METRIC_1:def 1;
A7: dist(y,x) = taxi_dist2.(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th19;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th20;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th21;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func Eukl_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
:Def9: for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
it.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2));
existence
proof
deffunc G(Element of REAL,Element of REAL,Element of REAL,Element of REAL)
= sqrt((real_dist.($1,$2))^2 + (real_dist.($3,$4)^2));
consider F being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL
such that
A1: for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
F.[x,y] = G(x1,y1,x2,y2)
from LambdaMCART;
take F;
let x1,y1,x2,y2 be Element of REAL,
x,y be Element of [:REAL,REAL:] such that
A2: ( x = [x1,x2] & y = [y1,y2] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)) by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
assume that
A3:for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:] st (x = [x1,x2] & y = [y1,y2])
holds
f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)) and
A4:for x1,y1,x2,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:] st (x = [x1,x2] & y = [y1,y2])
holds
f2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2));
for x,y being Element of [:REAL,REAL:]
holds f1.(x,y) = f2.(x,y)
proof
let x,y be Element of [:REAL,REAL:];
consider x1 be Element of REAL,
x2 be Element of REAL such that
A5: x = [x1,x2] by DOMAIN_1:9;
consider y1 be Element of REAL,
y2 be Element of REAL such that
A6: y = [y1,y2] by DOMAIN_1:9;
thus f1.(x,y)=sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2))
by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th22:
for x1,x2,y1,y2 being Element of REAL
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
Eukl_dist2.(x,y) = 0 iff x = y
proof
let x1,x2,y1,y2 be Element of REAL,
x,y be Element of [:REAL,REAL:] such that
A1:x = [x1,x2] & y = [y1,y2];
thus Eukl_dist2.(x,y) = 0 implies x = y
proof
assume A2:Eukl_dist2.(x,y) = 0;
set d1 = real_dist.(x1,y1);
set d2 = real_dist.(x2,y2);
A3:sqrt(d1^2 + d2^2) = 0 by A1,A2,Def9;
A4: 0 <= d1^2 by SQUARE_1:72;
A5: 0 <= d2^2 by SQUARE_1:72;
then A6:d1^2 = 0 & d2^2 = 0 by A3,A4,Th2;
d1^2 = 0 by A3,A4,A5,Th2;
then d1 = 0 by SQUARE_1:73;
then A7: x1 = y1 by METRIC_1:9;
d2 = 0 by A6,SQUARE_1:73;
hence thesis by A1,A7,METRIC_1:9;
end;
assume x = y;
then A8:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
then A9:(real_dist.(x1,y1))^2 = 0 by METRIC_1:9,SQUARE_1:60;
A10: (real_dist.(x2,y2))^2 = 0 by A8,METRIC_1:9,SQUARE_1:60;
Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2))^2
)
by A1,Def9
.= 0 by A9,A10,Th2;
hence thesis;
end;
theorem Th23:
for x,y being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2]) holds
Eukl_dist2.(x,y) = Eukl_dist2.(y,x)
proof
let x,y be Element of [:REAL,REAL:]; assume
A1:x = [x1,x2] & y = [y1,y2];
then Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)
^2
))
by Def9
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2)) by METRIC_1:10
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)) by METRIC_1:10
.= Eukl_dist2.(y,x) by A1,Def9;
hence thesis;
end;
theorem
Th24:
for x,y,z being Element of [:REAL,REAL:]
st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
Eukl_dist2.(x,z) <= Eukl_dist2.(x,y) + Eukl_dist2.(y,z)
proof
let x,y,z be Element of [:REAL,REAL:] such that
A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
set d1 = real_dist.(x1,z1);
set d2 = real_dist.(x1,y1);
set d3 = real_dist.(y1,z1);
set d4 = real_dist.(x2,z2);
set d5 = real_dist.(x2,y2);
set d6 = real_dist.(y2,z2);
A2: d1 <= d2 + d3 by METRIC_1:11;
d1 = abs(x1 - z1) by METRIC_1:def 13;
then 0 <= d1 by ABSVALUE:5;
then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
A4: d4 <= d5 + d6 by METRIC_1:11;
d4 = abs(x2 - z2) by METRIC_1:def 13;
then 0 <= d4 by ABSVALUE:5;
then (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
then A5: (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,REAL_1:55;
A6: 0 <= (d1)^2 by SQUARE_1:72;
0 <= (d4)^2 by SQUARE_1:72;
then 0 + 0 <= (d1)^2 + (d4)^2 by A6,REAL_1:55;
then A7: sqrt((d1)^2 + (d4)^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2)
by A5,SQUARE_1:94;
A8: d2 = abs(x1 - y1) by METRIC_1:def 13;
A9: d3 = abs(y1 - z1) by METRIC_1:def 13;
A10: d5 = abs(x2 - y2) by METRIC_1:def 13;
d6 = abs(y2 - z2) by METRIC_1:def 13;
then (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6) by A8,A9,A10,ABSVALUE:5;
then sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2
+ d6^2)
by Th5;
then sqrt((d1)^2 + (d4)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2)
by A7,AXIOMS:22;
then Eukl_dist2.(x,z) <=
sqrt((d2)^2 + (d5)^2) + sqrt((d3)^2 + (d6)^2) by A1,Def9;
then Eukl_dist2.(x,z) <=
Eukl_dist2.(x,y) + sqrt((d3)^2 + (d6)^2) by A1,Def9;
hence thesis by A1,Def9;
end;
definition
func EuklSpace2 -> strict non empty MetrSpace equals
MetrStruct(#[:REAL,REAL:],Eukl_dist2#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:REAL,REAL:],Eukl_dist2#);
reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL:];
A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
A4: dist(x,y) = Eukl_dist2.(x',y') by METRIC_1:def 1;
A5: dist(x,z) = Eukl_dist2.(x',z') by METRIC_1:def 1;
A6: dist(y,z) = Eukl_dist2.(y',z') by METRIC_1:def 1;
A7: dist(y,x) = Eukl_dist2.(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th22;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th23;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th24;
end;
hence thesis by METRIC_1:6;
end;
end;
reserve x3,y3,z3 for Element of REAL;
definition
func taxi_dist3 -> Function of [:[:REAL,REAL,REAL:],
[:REAL,REAL,REAL:]:],REAL means
:Def11: for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
it.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3);
existence
proof
deffunc G(Element of REAL,Element of REAL,Element of REAL,Element of REAL,
Element of REAL,Element of REAL)
= real_dist.($1,$2) + real_dist.($3,$4) + real_dist.($5,$6);
consider F being Function of [:[:REAL,REAL,REAL:],
[:REAL,REAL,REAL:]:],REAL
such that
A1: for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
F.[x,y] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
take F;
let x1,y1,x2,y2,x3,y3 be Element of REAL,
x,y be Element of [:REAL,REAL,REAL:] such that
A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3)
by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
assume that
A3:for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3)
and
A4:for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3);
for x,y being Element of [:REAL,REAL,REAL:]
holds f1.(x,y) = f2.(x,y)
proof
let x,y be Element of [:REAL,REAL,REAL:];
consider x1 be Element of REAL,x2 be Element of REAL,
x3 be Element of REAL
such that
A5: x = [x1,x2,x3] by DOMAIN_1:15;
consider y1 be Element of REAL,y2 be Element of REAL,
y3 be Element of REAL
such that
A6: y = [y1,y2,y3] by DOMAIN_1:15;
thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3
)
by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem
Th25:
for x1,x2,y1,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
taxi_dist3.(x,y) = 0 iff x = y
proof
let x1,x2,y1,y2,x3,y3 be Element of REAL,
x,y be Element of [:REAL,REAL,REAL:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
thus taxi_dist3.(x,y) = 0 implies x = y
proof
assume A2:taxi_dist3.(x,y) = 0;
set d1 = real_dist.(x1,y1);
set d2 = real_dist.(x2,y2);
set d3 = real_dist.(x3,y3);
set d4 = d1 + d2;
A3: d4 + d3 = 0 by A1,A2,Def11;
d3 = abs(x3 - y3) by METRIC_1:def 13;
then A4: 0 <= d3 by ABSVALUE:5;
d2 = abs(x2 - y2) by METRIC_1:def 13;
then A5: 0 <= d2 by ABSVALUE:5;
d1 = abs(x1 - y1) by METRIC_1:def 13;
then A6: 0 <= d1 by ABSVALUE:5;
then A7: 0 + 0 <= d1 + d2 by A5,REAL_1:55;
then A8:d4 = 0 & d3 = 0 by A3,A4,METRIC_3:2;
d4 = 0 by A3,A4,A7,METRIC_3:2;
then A9:d1 = 0 & d2 = 0 by A5,A6,METRIC_3:2;
A10: x3 = y3 by A8,METRIC_1:9;
x1 = y1 by A9,METRIC_1:9;
hence thesis by A1,A9,A10,METRIC_1:9;
end;
assume A11: x = y;
then A12: (x1 = y1 & x2 = y2) & x3 = y3 by A1,MCART_1:28;
A13: x1 = y1 & (x2 = y2 & x3 = y3) by A1,A11,MCART_1:28;
A14:real_dist.(x1,y1) = 0 by A12,METRIC_1:9;
A15:real_dist.(x2,y2) = 0 by A12,METRIC_1:9;
taxi_dist3.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2)
+ real_dist.(x3,y3) by A1,Def11
.= 0 by A13,A14,A15,METRIC_1:9;
hence thesis;
end;
theorem
Th26:
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
taxi_dist3.(x,y) = taxi_dist3.(y,x)
proof
let x,y be Element of [:REAL,REAL,REAL:]; assume
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
then taxi_dist3.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2)
+ real_dist.(x3,y3) by Def11
.= real_dist.(y1,x1) + real_dist.(x2,y2)
+ real_dist.(x3,y3) by METRIC_1:10
.= real_dist.(y1,x1) + real_dist.(y2,x2)
+ real_dist.(x3,y3) by METRIC_1:10
.= real_dist.(y1,x1) + real_dist.(y2,x2)
+ real_dist.(y3,x3) by METRIC_1:10
.= taxi_dist3.(y,x) by A1,Def11;
hence thesis;
end;
theorem
Th27:
for x,y,z being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) holds
taxi_dist3.(x,z) <= taxi_dist3.(x,y) + taxi_dist3.(y,z)
proof
let x,y,z be Element of [:REAL,REAL,REAL:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
set d1 = real_dist.(x1,z1);
set d2 = real_dist.(x1,y1);
set d3 = real_dist.(y1,z1);
set d4 = real_dist.(x2,z2);
set d5 = real_dist.(x2,y2);
set d6 = real_dist.(y2,z2);
set d7 = real_dist.(x3,z3);
set d8 = real_dist.(x3,y3);
set d9 = real_dist.(y3,z3);
A2: ((d2 + d3) + (d5 + d6)) + (d8 + d9)
= (((d2 + d3) + d5) + d6) + (d8 + d9) by XCMPLX_1:1
.= (((d2 + d5) + d3) + d6) + (d8 + d9) by XCMPLX_1:1
.= ((d2 + d5) + (d3 + d6)) + (d8 + d9) by XCMPLX_1:1
.= ((d2 + d5) + (d8 + d9)) + (d3 + d6) by XCMPLX_1:1
.= (((d2 + d5) + d8) + d9) + (d3 + d6) by XCMPLX_1:1
.= ((d2 + d5) + d8) + ((d3 + d6) + d9) by XCMPLX_1:1
.= taxi_dist3.(x,y) + ((d3 +d6) + d9) by A1,Def11
.= taxi_dist3.(x,y) + taxi_dist3.(y,z) by A1,Def11;
A3: d1 <= d2 + d3 by METRIC_1:11;
A4: d4 <= d5 + d6 by METRIC_1:11;
set d10 = d1 + d4;
A5: d10 <= (d2 + d3) + (d5 + d6) by A3,A4,REAL_1:55;
d7 <= d8 + d9 by METRIC_1:11;
then d10 + d7 <= ((d2 + d3) + (d5 + d6)) + (d8 + d9) by A5,REAL_1:55;
hence thesis by A1,A2,Def11;
end;
definition
func RealSpaceCart3 -> strict non empty MetrSpace equals
MetrStruct(#[:REAL,REAL,REAL:],taxi_dist3#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:REAL,REAL,REAL:],taxi_dist3#);
reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL,REAL:];
A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
A4: dist(x,y) = taxi_dist3.(x',y') by METRIC_1:def 1;
A5: dist(x,z) = taxi_dist3.(x',z') by METRIC_1:def 1;
A6: dist(y,z) = taxi_dist3.(y',z') by METRIC_1:def 1;
A7: dist(y,x) = taxi_dist3.(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th25;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th26;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th27;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func Eukl_dist3 -> Function of [:[:REAL,REAL,REAL:],
[:REAL,REAL,REAL:]:],REAL means
:Def13: for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
it.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2));
existence
proof
deffunc G(Element of REAL,Element of REAL,Element of REAL,Element of REAL,
Element of REAL,Element of REAL)
= sqrt((real_dist.($1,$2))^2 + (real_dist.($3,$4)^2)
+ (real_dist.($5,$6)^2));
consider F being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL
such that
A1: for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
F.[x,y] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
take F;
let x1,y1,x2,y2,x3,y3 be Element of REAL,
x,y be Element of [:REAL,REAL,REAL:] such that
A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
thus F.(x,y) = F.[x,y] by BINOP_1:def 1
.= sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2)) by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
assume that
A3:for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2)) and
A4:for x1,y1,x2,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3])
holds
f2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2));
for x,y being Element of [:REAL,REAL,REAL:]
holds f1.(x,y) = f2.(x,y)
proof
let x,y be Element of [:REAL,REAL,REAL:];
consider x1 be Element of REAL,
x2 be Element of REAL,
x3 be Element of REAL
such that
A5: x = [x1,x2,x3] by DOMAIN_1:15;
consider y1 be Element of REAL,
y2 be Element of REAL,
y3 be Element of REAL
such that
A6: y = [y1,y2,y3] by DOMAIN_1:15;
thus f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2)) by A3,A5,A6
.= f2.(x,y) by A4,A5,A6;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th28:
for x1,x2,y1,y2,x3,y3 being Element of REAL
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
Eukl_dist3.(x,y) = 0 iff x = y
proof
let x1,x2,y1,y2,x3,y3 be Element of REAL,
x,y be Element of [:REAL,REAL,REAL:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
thus Eukl_dist3.(x,y) = 0 implies x = y
proof
assume A2:Eukl_dist3.(x,y) = 0;
set d1 = real_dist.(x1,y1);
set d2 = real_dist.(x2,y2);
set d3 = real_dist.(x3,y3);
sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,A2,Def13;
then A3:sqrt(d1^2 + (d2^2 + d3^2)) =0 by XCMPLX_1:1;
A4: 0 <= d1^2 by SQUARE_1:72;
A5: 0 <= d2^2 by SQUARE_1:72;
0 <= d3^2 by SQUARE_1:72;
then A6: 0 + 0 <= d2^2 + d3^2 by A5,REAL_1:55;
then d1^2 = 0 & (d2^2 + d3^2) = 0 by A3,A4,Th2;
then d1 = 0 by SQUARE_1:73;
then A7: x1 = y1 by METRIC_1:9;
A8: d2^2 + d3^2 = 0 by A3,A4,A6,Th2;
A9: 0 <= d2^2 by SQUARE_1:72;
A10: 0 <= d3^2 by SQUARE_1:72;
then A11: d2^2 = 0 & d3^2 = 0 by A8,A9,METRIC_3:2;
d2^2 = 0 by A8,A9,A10,METRIC_3:2;
then d2 = 0 by SQUARE_1:73;
then A12:x2 = y2 by METRIC_1:9;
d3 = 0 by A11,SQUARE_1:73;
hence thesis by A1,A7,A12,METRIC_1:9;
end;
assume x = y;
then A13:x1 = y1 & x2 = y2 & x3 = y3 by A1,MCART_1:28;
then A14: (real_dist.(x1,y1))^2 = 0 by METRIC_1:9,SQUARE_1:60;
A15: (real_dist.(x2,y2))^2 = 0 by A13,METRIC_1:9,SQUARE_1:60;
Eukl_dist3.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2))^2
+ (real_dist.(x3,y3))^2) by A1,Def13
.= 0 by A13,A14,A15,METRIC_1:9,SQUARE_1:60,82;
hence thesis;
end;
theorem Th29:
for x,y being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
Eukl_dist3.(x,y) = Eukl_dist3.(y,x)
proof
let x,y be Element of [:REAL,REAL,REAL:]; assume
A1:x = [x1,x2,x3] & y = [y1,y2,y3];
then Eukl_dist3.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)
^2
)
+ (real_dist.(x3,y3)^2)) by Def13
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2)
+ (real_dist.(x3,y3)^2)) by METRIC_1:10
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)
+ (real_dist.(x3,y3)^2)) by METRIC_1:10
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)
+ (real_dist.(y3,x3)^2)) by METRIC_1:10
.= Eukl_dist3.(y,x) by A1,Def13;
hence thesis;
end;
theorem Th30:
for x,y,z being Element of [:REAL,REAL,REAL:]
st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) holds
Eukl_dist3.(x,z) <= Eukl_dist3.(x,y) + Eukl_dist3.(y,z)
proof
let x,y,z be Element of [:REAL,REAL,REAL:] such that
A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
set d1 = real_dist.(x1,z1), d2 = real_dist.(x1,y1);
set d3 = real_dist.(y1,z1), d4 = real_dist.(x2,z2);
set d5 = real_dist.(x2,y2), d6 = real_dist.(y2,z2);
set d7 = real_dist.(x3,z3), d8 = real_dist.(x3,y3);
set d9 = real_dist.(y3,z3);
A2: d1 <= d2 + d3 by METRIC_1:11;
d1 = abs(x1 - z1) by METRIC_1:def 13;
then 0 <= d1 by ABSVALUE:5;
then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
A4: d4 <= d5 + d6 by METRIC_1:11;
d4 = abs(x2 - z2) by METRIC_1:def 13;
then 0 <= d4 by ABSVALUE:5;
then A5: (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
A6: d7 <= d8 + d9 by METRIC_1:11;
d7 = abs(x3 - z3) by METRIC_1:def 13;
then 0 <= d7 by ABSVALUE:5;
then A7: (d7)^2 <= (d8 + d9)^2 by A6,SQUARE_1:77;
(d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,A5,REAL_1:55;
then A8: (d1)^2 + (d4)^2 + (d7)^2 <= (d2 + d3)^2 + (d5 + d6)^2
+ (d8 + d9)^2
by A7,REAL_1:55;
A9: 0 <= (d1)^2 by SQUARE_1:72;
0 <= (d4)^2 by SQUARE_1:72;
then A10: 0 + 0 <= (d1)^2 + (d4)^2 by A9,REAL_1:55;
0 <= (d7)^2 by SQUARE_1:72;
then 0 + 0 <= ((d1)^2 + (d4)^2) + (d7)^2 by A10,REAL_1:55;
then A11: sqrt((d1)^2 + (d4)^2 + (d7)^2) <= sqrt((d2 + d3)^2 + (d5 + d6)
^2 +
(d8 + d9)^2) by A8,SQUARE_1:94;
A12: d2 = abs(x1 - y1) by METRIC_1:def 13;
A13: d3 = abs(y1 - z1) by METRIC_1:def 13;
A14: d5 = abs(x2 - y2) by METRIC_1:def 13;
A15: d6 = abs(y2 - z2) by METRIC_1:def 13;
A16: d8 = abs(x3 - y3) by METRIC_1:def 13;
d9 = abs(y3 - z3) by METRIC_1:def 13;
then (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6 & 0 <= d8 & 0 <= d9)
by A12,A13,A14,A15,A16,ABSVALUE:5;
then sqrt((d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2) <= sqrt(d2^2 + d5^2
+ d8^2)
+ sqrt(d3^2 + d6^2 + d9^2) by Lm1;
then sqrt((d1)^2 + (d4)^2 + d7^2) <= sqrt(d2^2 + d5^2 + d8^2) +
sqrt(d3^2 + d6^2 + d9^2)
by A11,AXIOMS:22;
then Eukl_dist3.(x,z) <=
sqrt((d2)^2 + (d5)^2 + d8^2) + sqrt((d3)^2 + (d6)^2 + d9^2
) by A1,Def13;
then Eukl_dist3.(x,z) <=
Eukl_dist3.(x,y) + sqrt((d3)^2 + (d6)^2 + d9^2) by A1,Def13;
hence thesis by A1,Def13;
end;
definition
func EuklSpace3 -> strict non empty MetrSpace equals
MetrStruct(#[:REAL,REAL,REAL:],Eukl_dist3#);
coherence
proof
now
let x,y,z be Element of
MetrStruct(#[:REAL,REAL,REAL:],Eukl_dist3#);
reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL,REAL:];
A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
A4: dist(x,y) = Eukl_dist3.(x',y') by METRIC_1:def 1;
A5: dist(x,z) = Eukl_dist3.(x',z') by METRIC_1:def 1;
A6: dist(y,z) = Eukl_dist3.(y',z') by METRIC_1:def 1;
A7: dist(y,x) = Eukl_dist3.(y',x') by METRIC_1:def 1;
thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th28;
thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th29;
thus dist(x,z) <= dist(x,y) + dist(y,z)
by A1,A2,A3,A4,A5,A6,Th30;
end;
hence thesis by METRIC_1:6;
end;
end;