### The Mizar article:

### Metrics in the Cartesian Product --- Part II

**by****Stanislawa Kanas, and****Adam Lecko**

- Received July 8, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: METRIC_4
- [ MML identifier index ]

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;

Back to top