:: Metrics in Cartesian Product
:: by Stanis{\l}awa Kanas and Jan Stankiewicz
::
:: Received September 27, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, METRIC_1, SUBSET_1, FUNCT_1, ZFMISC_1, MCART_1,
STRUCT_0, NUMBERS, ARYTM_3, CARD_1, XXREAL_0, REAL_1, METRIC_3, SQUARE_1,
RELAT_1, ARYTM_1, COMPLEX1, RECDEF_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_2, BINOP_1, STRUCT_0,
METRIC_1, MCART_1, XXREAL_0, SQUARE_1;
constructors XXREAL_0, REAL_1, MEMBERED, METRIC_1, SQUARE_1, DOMAIN_1,
COMPLEX1, BINOP_1;
registrations SUBSET_1, NUMBERS, STRUCT_0, METRIC_1, RELAT_1, XCMPLX_0,
XREAL_0, SQUARE_1, ORDINAL1, XTUPLE_0, MCART_1;
requirements SUBSET, BOOLE, ARITHM, NUMERALS, REAL;
equalities SQUARE_1;
theorems BINOP_1, DOMAIN_1, METRIC_1, XREAL_1, SQUARE_1, COMPLEX1, XXREAL_0;
schemes BINOP_1;
begin
reserve X, Y, Z, W for non empty MetrSpace;
scheme LambdaMCART { X, Y, Z() -> non empty set,
F(object,object,object,object) -> Element of Z()} :
ex f being Function of [:[:X(),Y():],[:X(),Y():]:],Z() st
for x1,y1 being Element of X()
for x2,y2 being Element of Y()
for x,y being Element of [:X(),Y():] st
x = [x1,x2] & y = [y1,y2] holds f.(x,y) = F(x1,y1,x2,y2)
proof
deffunc G(Element of [:X(),Y():],Element of [:X(),Y():]) =
F($1`1,$2`1,$1`2,$2`2);
consider f being Function of [:[:X(),Y():],[:X(),Y():]:],Z() such that
A1: for x,y being Element of [:X(),Y():] holds f.(x,y) = G(x,y) from
BINOP_1:sch 4;
take f;
let x1,y1 be Element of X(), x2,y2 be Element of Y(), x,y be Element of [:X(
),Y():] such that
A2: x = [x1,x2] and
A3: y = [y1,y2];
A4: y1 = y`1 & y2 = y`2 by A3;
x1 = x`1 & x2 = x`2 by A2;
hence thesis by A1,A4;
end;
definition let X,Y;
func dist_cart2(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, x2, y2 being Element of Y,
x, y being Element of [:the carrier of X,the carrier of Y:] st
x = [x1,x2] & y = [y1,y2] holds it.(x,y) = dist(x1,y1) + dist(x2,y2);
existence
proof
deffunc G(Element of X,Element of X, Element of Y,Element of Y)
= In(dist($1,$2) + dist($3,$4),REAL);
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:];
assume x = [x1,x2] & y = [y1,y2];
then F.(x,y) = G(x1,y1,x2,y2) by A1;
hence thesis;
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
A2: 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) = dist(x1,y1) + dist(x2,y2) and
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 f2.(x,y) = dist(x1,y1) + dist(x2,y2);
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
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1 be Element of X, y2 be Element of Y such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1.(x,y) =dist(x1,y1) + dist(x2,y2) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th1:
for x, y being Element of [:the carrier of X,the carrier of Y:]
holds dist_cart2(X,Y).(x,y) = 0 iff x = y
proof
let x,y be Element of [:the carrier of X,the carrier of Y:];
reconsider x1 = x`1, y1 = y`1 as Element of X;
reconsider x2 = x`2, y2 = y`2 as Element of Y;
A1: x = [x1,x2] & y = [y1,y2];
thus dist_cart2(X,Y).(x,y) = 0 implies x = y
proof
set d1 = dist(x1,y1), d2 = dist(x2,y2);
assume dist_cart2(X,Y).(x,y) = 0;
then
A2: d1 + d2 = 0 by A1,Def1;
A3: 0 <= d1 & 0 <= d2 by METRIC_1:5;
then d1 = 0 by A2,XREAL_1:27;
then
A4: x1 = y1 by METRIC_1:2;
d2 = 0 by A2,A3,XREAL_1:27;
hence thesis by A1,A4,METRIC_1:2;
end;
assume
A5: x = y;
then
A6: dist(x2,y2) = 0 by METRIC_1:1;
dist_cart2(X,Y).(x,y) = dist(x1,y1) + dist(x2,y2) by A1,Def1
.= 0 by A5,A6,METRIC_1:1;
hence thesis;
end;
theorem Th2:
for x,y being Element of [:the carrier of X,the carrier of Y:]
holds dist_cart2(X,Y).(x,y) = dist_cart2(X,Y).(y,x)
proof
let x,y be Element of [:the carrier of X,the carrier of Y:];
reconsider x1 = x`1, y1 = y`1 as Element of X;
reconsider x2 = x`2, y2 = y`2 as Element of Y;
A1: x = [x1,x2] & y = [y1,y2];
then dist_cart2(X,Y).(x,y) = dist(y1,x1) + dist(x2,y2) by Def1
.= dist_cart2(X,Y).(y,x) by A1,Def1;
hence thesis;
end;
theorem Th3:
for x,y,z being Element of [:the carrier of X,the carrier of Y:]
holds dist_cart2(X,Y).(x,z) <= dist_cart2(X,Y).(x,y) + dist_cart2(X,Y).(y,z)
proof
let x,y,z be Element of [:the carrier of X,the carrier of Y:];
reconsider x1 = x`1, y1 = y`1, z1 = z`1 as Element of X;
reconsider x2 = x`2, y2 = y`2, z2 = z`2 as Element of Y;
A1: y = [y1,y2];
set d6 = dist(y2,z2);
set d5 = dist(x2,y2);
set d4 = dist(x2,z2);
set d3 = dist(y1,z1);
set d2 = dist(x1,y1);
set d1 = dist(x1,z1);
A2: z = [z1,z2];
A3: x = [x1,x2];
then
A4: dist_cart2(X,Y).(x,z) = d1 + d4 by A2,Def1;
A5: d1 <= d2 + d3 & d4 <= d5 + d6 by METRIC_1:4;
(d2 + d3) + (d5 + d6) = (d2 + d5) + (d3 + d6)
.= dist_cart2(X,Y).(x,y) + (d3 +d6) by A3,A1,Def1
.= dist_cart2(X,Y).(x,y) + dist_cart2(X,Y).(y,z) by A1,A2,Def1;
hence thesis by A5,A4,XREAL_1:7;
end;
definition let X,Y;
let x,y be Element of [:the carrier of X,the carrier of Y:];
func dist2(x,y) -> Real equals
dist_cart2(X,Y).(x,y);
coherence;
end;
registration
let A be non empty set, r be Function of [:A,A:], REAL;
cluster MetrStruct(#A,r#) -> non empty;
coherence;
end;
definition
let X,Y;
func MetrSpaceCart2(X,Y) -> strict non empty MetrSpace equals
MetrStruct (#[:the carrier of X,the carrier of Y:], dist_cart2(X,Y)#);
coherence
proof
set M = MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2(X,Y)
#);
now
let x,y,z be Element of M;
A1: dist(x,y) = dist_cart2(X,Y).(x,y) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th1;
dist(y,x) = dist_cart2(X,Y).(y,x) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th2;
dist(x,z) = dist_cart2(X,Y).(x,z) & dist(y,z) = dist_cart2(X,Y).(y,z
) by METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th3;
end;
hence thesis by METRIC_1:6;
end;
end;
:: Metrics in the Cartesian product of three sets
scheme
LambdaMCART1 { X, Y, Z, T() -> non empty set,
F(object,object,object,object,object,object) -> Element of T()}:
ex f being Function of [:[:X(),Y(),Z():],[:X(),Y(),Z():]:],T()
st 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 [:X(),Y(),Z():] st x = [x1,x2,x3]
& y = [y1,y2,y3] holds f.(x,y) = F(x1,y1,x2,y2,x3,y3) proof
deffunc G(Element of [:X(),Y(),Z():],Element of [:X(),Y(),Z():])
= F($1`1_3,$2`1_3,$1`2_3,$2`2_3,$1`3_3,$2`3_3);
consider f being Function of [:[:X(),Y(),Z():],[:X(),Y(),Z():]:],T() such
that
A1: for x,y being Element of [:X(),Y(),Z():] holds f.(x,y) =G(x,y) from
BINOP_1:sch 4;
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 [:X(),Y(),Z():] such that
A2: x = [x1,x2,x3] and
A3: y = [y1,y2,y3];
A5: y1 = y`1_3 & y2 = y`2_3 by A3;
A7: x3 = x`3_3 by A2;
A8: y3 = y`3_3 by A3;
x1 = x`1_3 & x2 = x`2_3 by A2;
hence thesis by A1,A5,A7,A8;
end;
definition
let X,Y,Z;
func dist_cart3(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) = (dist(x1,y1) + dist(x2,y2)) + dist(x3,y3);
existence
proof
deffunc G(Element of X,Element of X, Element of Y,Element of Y, Element of
Z,Element of Z) =In((dist($1,$2) + dist($3,$4)) + dist($5,$6),REAL);
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:];
assume x = [x1,x2,x3] & y = [y1,y2,y3];
then F.(x,y) = G(x1,y1,x2,y2,x3,y3) by A1;
hence thesis;
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
A2: 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) = (
dist(x1,y1) + dist(x2,y2)) + dist(x3,y3) and
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 f2.(x,y) = (
dist(x1,y1) + dist(x2,y2)) + dist(x3,y3);
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 being Element of X, x2 being Element of Y, x3 being Element
of Z such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1 being Element of X, y2 being Element of Y, y3 being Element
of Z such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1.(x,y) = (dist(x1,y1) + dist(x2,y2)) +dist(x3,y3) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th4:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z:] holds dist_cart3(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:];
reconsider x1 = x`1_3, y1 = y`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3 as Element of Z;
A1: x = [x1,x2,x3] & y = [y1,y2,y3];
thus dist_cart3(X,Y,Z).(x,y) = 0 implies x = y
proof
set d3 = dist(x3,y3);
set d2 = dist(x2,y2);
set d1 = dist(x1,y1);
set d4 = d1 + d2;
assume dist_cart3(X,Y,Z).(x,y) = 0;
then
A2: d4 + d3 = 0 by A1,Def4;
A3: 0 <= d1 & 0 <= d2 by METRIC_1:5;
then
A4: 0 <= d3 & 0 + 0 <= d1 + d2 by METRIC_1:5,XREAL_1:7;
then
A5: d4 = 0 by A2,XREAL_1:27;
then d1 = 0 by A3,XREAL_1:27;
then
A6: x1 = y1 by METRIC_1:2;
d3 = 0 by A2,A4,XREAL_1:27;
then
A7: x3 = y3 by METRIC_1:2;
d2 = 0 by A3,A5,XREAL_1:27;
hence thesis by A1,A7,A6,METRIC_1:2;
end;
assume
A8: x = y;
then
A9: dist(x1,y1) = 0 & dist(x2,y2) = 0 by METRIC_1:1;
dist_cart3(X,Y,Z).(x,y) = (dist(x1,y1) + dist(x2,y2)) + dist(x3,y3) by A1
,Def4
.= 0 by A8,A9,METRIC_1:1;
hence thesis;
end;
theorem Th5:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z:] holds dist_cart3(X,Y,Z).(x,y) = dist_cart3(X,Y,Z).(y,x)
proof
let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:];
reconsider x1 = x`1_3, y1 = y`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3 as Element of Z;
A1: x = [x1,x2,x3] & y = [y1,y2,y3];
then dist_cart3(X,Y,Z).(x,y) = (dist(y1,x1) + dist(y2,x2)) + dist(y3,x3) by
Def4
.= dist_cart3(X,Y,Z).(y,x) by A1,Def4;
hence thesis;
end;
theorem Th6:
for x,y,z being Element of [:the carrier of X,the carrier of Y,
the carrier of Z:] holds dist_cart3(X,Y,Z).(x,z) <= dist_cart3(X,Y,Z).(x,y) +
dist_cart3(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
:];
reconsider x1 = x`1_3, y1 = y`1_3, z1 = z`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3, z2 = z`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3, z3 = z`3_3 as Element of Z;
A1: x = [x1,x2,x3];
set d4 = dist(x2,z2), d5 = dist(x2,y2), d6 = dist(y2,z2);
A2: z = [z1,z2,z3];
set d7 = dist(x3,z3), d8 = dist(x3,y3), d9 = dist(y3,z3);
set d1 = dist(x1,z1), d2 = dist(x1,y1), d3 = dist(y1,z1);
A3: y = [y1,y2,y3];
set d10 = d1 + d4;
d1 <= d2 + d3 & d4 <= d5 + d6 by METRIC_1:4;
then
A4: d10 <= (d2 + d3) + (d5 + d6) by XREAL_1:7;
d7 <= d8 + d9 by METRIC_1:4;
then
A5: d10 + d7 <= ((d2 + d3) + (d5 + d6)) + (d8 + d9) by A4,XREAL_1:7;
((d2 + d3) + (d5 + d6)) + (d8 + d9) = ((d2 + d5) + d8) + ((d3 + d6) + d9)
.= dist_cart3(X,Y,Z).(x,y) + ((d3 +d6) + d9) by A1,A3,Def4
.= dist_cart3(X,Y,Z).(x,y) + dist_cart3(X,Y,Z).(y,z) by A3,A2,Def4;
hence thesis by A1,A2,A5,Def4;
end;
definition
let X,Y,Z;
func MetrSpaceCart3(X,Y,Z) -> strict non empty MetrSpace equals
MetrStruct(#
[:the carrier of X,the carrier of Y,the carrier of Z:], dist_cart3(X,Y,Z)#);
coherence
proof
set M = MetrStruct(#[:the carrier of X,the carrier of Y,the carrier of Z:]
, dist_cart3(X,Y,Z)#);
now
let x,y,z be Element of M;
A1: dist(x,y) = dist_cart3(X,Y,Z).(x,y) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th4;
dist(y,x) = dist_cart3(X,Y,Z).(y,x) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th5;
dist(x,z) = dist_cart3(X,Y,Z).(x,z) & dist(y,z) = dist_cart3(X,Y,Z).
(y,z) by METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th6;
end;
hence thesis by METRIC_1:6;
end;
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 dist3(x,y) -> Real equals
dist_cart3(X,Y,Z).(x,y);
coherence;
end;
:: Metrics in the Cartesian product of four sets
scheme
LambdaMCART2 { X, Y, Z, W, T() -> non empty set,
F(object,object,object,object,object,object,object,object) ->Element of T()}:
ex f being Function of [:[:X(),Y(),Z(),W():],[:X(),
Y(),Z(),W():]:],T() st for x1,y1 being Element of X() for x2,y2 being Element
of Y() for x3,y3 being Element of Z() for x4,y4 being Element of W() for x,y
being Element of [:X(),Y(),Z(),W():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4]
holds f.(x,y) = F(x1,y1,x2,y2,x3,y3,x4,y4) proof
deffunc G(Element of [:X(),Y(),Z(),W():],Element of [:X(),Y(),Z(),W():])
= F($1`1_4,$2`1_4,$1`2_4,$2`2_4,$1`3_4,$2`3_4,$1`4_4,$2`4_4);
consider f being Function of [:[:X(),Y(),Z(),W():],[:X(),Y(),Z(),W():]:],T()
such that
A1: for x,y being Element of [:X(),Y(),Z(),W():] holds f.(x,y) = G(x,y)
from BINOP_1:sch 4;
take f;
let x1,y1 be Element of X(), x2,y2 be Element of Y(), x3,y3 be Element of Z(
), x4,y4 be Element of W(), x,y be Element of [:X(),Y(),Z(),W():] such that
A2: x = [x1,x2,x3,x4] and
A3: y = [y1,y2,y3,y4];
A5: y1 = y`1_4 & y2 = y`2_4 by A3;
A7: x3 = x`3_4 & x4 = x`4_4 by A2;
A8: y3 = y`3_4 & y4 = y`4_4 by A3;
x1 = x`1_4 & x2 = x`2_4 by A2;
hence thesis by A1,A5,A7,A8;
end;
definition
let X,Y,Z,W;
func dist_cart4(X,Y,Z,W) -> Function of [:[:the carrier of X,the carrier of
Y,the carrier of Z,the carrier of W:], [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:]:], REAL means
:Def7:
for x1,y1 being Element of
X for x2,y2 being Element of Y for x3,y3 being Element of Z for x4,y4 being
Element of W for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
it.(x,y) = (dist(x1,y1) + dist(x2,y2)) + (dist(x3,y3) + dist(x4,y4));
existence
proof
deffunc G(Element of X,Element of X, Element of Y,Element of Y, Element of
Z,Element of Z, Element of W,Element of W)
= In((dist($1,$2) + dist($3,$4)) + (dist($5,$6) + dist($7,$8)),REAL);
consider F being Function of [:[:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:], [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:]:], 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 x4,y4 being Element of W for x,y being Element of [:
the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [
x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds F.(x,y) = G(x1,y1,x2,y2,x3,y3,x4,y4)
from LambdaMCART2;
take F;
let x1,y1 be Element of X, x2,y2 be Element of Y, x3,y3 be Element of Z,
x4,y4 be Element of W, x,y be Element of [:the carrier of X,the carrier of Y,
the carrier of Z,the carrier of W:];
assume x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4];
then F.(x,y) = G(x1,y1,x2,y2,x3,y3,x4,y4) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of [:[:the carrier of X,the carrier of Y,the carrier
of Z,the carrier of W:], [:the carrier of X,the carrier of Y,the carrier of Z,
the carrier of W:]:], REAL;
assume that
A2: for x1,y1 being Element of X, x2,y2 being Element of Y, x3,y3
being Element of Z, x4,y4 being Element of W, x,y being Element of [:the
carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2
,x3,x4] & y = [y1,y2,y3,y4] holds f1.(x,y) = (dist(x1,y1) + dist(x2,y2)) + (
dist(x3,y3) + dist(x4,y4)) and
A3: for x1,y1 being Element of X, x2,y2 being Element of Y, x3,y3
being Element of Z, x4,y4 being Element of W for x,y being Element of [:the
carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2
,x3,x4] & y = [y1,y2,y3,y4] holds f2.(x,y) = (dist(x1,y1) + dist(x2,y2)) + (
dist(x3,y3) + dist(x4,y4));
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:] 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,the carrier of W:];
consider x1 being Element of X, x2 being Element of Y, x3 being Element
of Z, x4 being Element of W such that
A4: x = [x1,x2,x3,x4] by DOMAIN_1:10;
consider y1 being Element of X, y2 being Element of Y, y3 being Element
of Z, y4 being Element of W such that
A5: y = [y1,y2,y3,y4] by DOMAIN_1:10;
thus f1.(x,y) = (dist(x1,y1) + dist(x2,y2)) + (dist(x3,y3) + dist(x4,y4)
) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th7:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(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,
the carrier of W:];
reconsider x1 = x`1_4, y1 = y`1_4 as Element of X;
reconsider x2 = x`2_4, y2 = y`2_4 as Element of Y;
reconsider x3 = x`3_4, y3 = y`3_4 as Element of Z;
reconsider x4 = x`4_4, y4 = y`4_4 as Element of W;
A1: x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4];
thus dist_cart4(X,Y,Z,W).(x,y) = 0 implies x = y
proof
set d1 = dist(x1,y1), d2 = dist(x2,y2), d3 = dist(x3,y3);
set d5 = dist(x4,y4), d4 = d1 + d2, d6 = d3 + d5;
A2: 0 <= d3 & 0 <= d5 by METRIC_1:5;
then
A3: 0 + 0 <= d3 + d5 by XREAL_1:7;
assume dist_cart4(X,Y,Z,W).(x,y) = 0;
then
A4: d4 + d6 = 0 by A1,Def7;
A5: 0 <= d1 & 0 <= d2 by METRIC_1:5;
then
A6: 0 + 0 <= d1 + d2 by XREAL_1:7;
then
A7: d4 = 0 by A4,A3,XREAL_1:27;
then d2 = 0 by A5,XREAL_1:27;
then
A8: x2 = y2 by METRIC_1:2;
A9: d6 = 0 by A4,A6,A3,XREAL_1:27;
then d3 = 0 by A2,XREAL_1:27;
then
A10: x3 = y3 by METRIC_1:2;
d5 = 0 by A2,A9,XREAL_1:27;
then
A11: x4 = y4 by METRIC_1:2;
d1 = 0 by A5,A7,XREAL_1:27;
hence thesis by A1,A8,A10,A11,METRIC_1:2;
end;
assume
A12: x = y;
then
A13: dist(x2,y2) = 0 & dist(x3,y3) = 0 by METRIC_1:1;
A14: dist(x4,y4) = 0 by A12,METRIC_1:1;
dist_cart4(X,Y,Z,W).(x,y) = (dist(x1,y1) + dist(x2,y2)) + (dist(x3,y3)
+ dist(x4,y4)) by A1,Def7
.= 0 by A12,A13,A14,METRIC_1:1;
hence thesis;
end;
theorem Th8:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(x,y) = dist_cart4(X,
Y,Z,W).(y,x)
proof
let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z,
the carrier of W:];
reconsider x1 = x`1_4, y1 = y`1_4 as Element of X;
reconsider x2 = x`2_4, y2 = y`2_4 as Element of Y;
reconsider x3 = x`3_4, y3 = y`3_4 as Element of Z;
reconsider x4 = x`4_4, y4 = y`4_4 as Element of W;
A1: x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4];
then
dist_cart4(X,Y,Z,W).(x,y) = (dist(y1,x1) + dist(y2,x2)) + (dist(y3,x3) +
dist(x4,y4)) by Def7
.= dist_cart4(X,Y,Z,W).(y,x) by A1,Def7;
hence thesis;
end;
theorem Th9:
for x,y,z being Element of [:the carrier of X,the carrier of Y,
the carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(x,z) <=
dist_cart4(X,Y,Z,W).(x,y) + dist_cart4(X,Y,Z,W).(y,z)
proof
let x,y,z be Element of [:the carrier of X,the carrier of Y,the carrier of Z
,the carrier of W:];
reconsider x1 = x`1_4, y1 = y`1_4, z1 = z`1_4 as Element of X;
reconsider x2 = x`2_4, y2 = y`2_4, z2 = z`2_4 as Element of Y;
reconsider x3 = x`3_4, y3 = y`3_4, z3 = z`3_4 as Element of Z;
reconsider x4 = x`4_4, y4 = y`4_4, z4 = z`4_4 as Element of W;
A1: x = [x1,x2,x3,x4];
set d7 = dist(x3,z3), d8 = dist(x3,y3), d9 = dist(y3,z3);
set d1 = dist(x1,z1), d2 = dist(x1,y1), d3 = dist(y1,z1);
A2: y = [y1,y2,y3,y4];
set d10 = dist(x4,z4), d11 = dist(x4,y4), d12 = dist(y4,z4);
set d4 = dist(x2,z2), d5 = dist(x2,y2), d6 = dist(y2,z2);
A3: z = [z1,z2,z3,z4];
set d16 = d7 + d10;
set d14 = d1 + d4;
set d17 = (d8 + d9) + (d11 + d12), d15 = (d2 + d3) + (d5 + d6);
d7 <= d8 + d9 & d10 <= d11 + d12 by METRIC_1:4;
then
A4: d16 <= d17 by XREAL_1:7;
d1 <= d2 + d3 & d4 <= d5 + d6 by METRIC_1:4;
then d14 <= d15 by XREAL_1:7;
then
A5: d14 + d16 <= d15 + d17 by A4,XREAL_1:7;
(d15 + d17) = ((d2 + d5) + (d8 + d11)) + ((d3 + d6) + (d9 + d12))
.= dist_cart4(X,Y,Z,W).(x,y) + ((d3 +d6) + (d9 + d12)) by A1,A2,Def7
.= dist_cart4(X,Y,Z,W).(x,y) + dist_cart4(X,Y,Z,W).(y,z) by A2,A3,Def7;
hence thesis by A1,A3,A5,Def7;
end;
definition
let X,Y,Z,W;
func MetrSpaceCart4(X,Y,Z,W) -> strict non empty MetrSpace equals
MetrStruct
(#[:the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],
dist_cart4(X,Y,Z,W)#);
coherence
proof
set M = MetrStruct(#[:the carrier of X,the carrier of Y, the carrier of Z,
the carrier of W:],dist_cart4(X,Y,Z,W)#);
now
let x,y,z be Element of M;
reconsider x9 = x,y9 = y,z9 = z as Element of [:the carrier of X,the
carrier of Y,the carrier of Z,the carrier of W:];
A1: dist(x,y) = dist_cart4(X,Y,Z,W).(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th7;
dist(y,x) = dist_cart4(X,Y,Z,W).(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th8;
dist(x,z) = dist_cart4(X,Y,Z,W).(x9,z9) & dist(y,z) = dist_cart4(X,Y
,Z,W).( y9,z9) by METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th9;
end;
hence thesis by METRIC_1:6;
end;
end;
definition let X,Y,Z,W;
let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z,
the carrier of W:];
func dist4(x,y) -> Real equals
dist_cart4(X,Y,Z,W).(x,y);
coherence;
end;
begin :: Metrics in the Cartesian Product of Two Sets (METRIC_4)
reserve X,Y for non empty MetrSpace;
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
:Def10:
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) =
In(sqrt(dist($1,$2)^2 + dist($3,$4)^2),REAL);
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:];
assume x = [x1,x2] & y = [y1,y2];
then F.(x,y) = G(x1,y1,x2,y2) by A1;
hence thesis;
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
A2: 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
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 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
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1 be Element of X, y2 be Element of Y such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
Lm1:
for a,b being Real st 0 <= a & 0 <= b holds sqrt(a + b) =
0 iff a = 0 & b = 0 by SQUARE_1:31;
theorem Th10:
for x,y being Element of [:the carrier of X,the carrier of Y:]
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:];
reconsider x1 = x`1, y1 = y`1 as Element of X;
reconsider x2 = x`2, y2 = y`2 as Element of Y;
A1: x = [x1,x2] & y = [y1,y2];
thus dist_cart2S(X,Y).(x,y) = 0 implies x = y
proof
set d2 = dist(x2,y2);
set d1 = dist(x1,y1);
assume dist_cart2S(X,Y).(x,y) = 0;
then
A2: sqrt(d1^2 + d2^2) = 0 by A1,Def10;
A3: 0 <= d1^2 & 0 <= d2^2 by XREAL_1:63;
then d1 = 0 by A2,Lm1;
then
A4: x1 = y1 by METRIC_1:2;
d2 = 0 by A2,A3,Lm1;
hence thesis by A1,A4,METRIC_1:2;
end;
assume x = y;
then
A5: (dist(x1,y1))^2 = 0^2 & (dist(x2,y2))^2 = 0^2 by METRIC_1:1;
dist_cart2S(X,Y).(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2) by A1,Def10
.= 0 by A5;
hence thesis;
end;
theorem Th11:
for x,y being Element of [:the carrier of X,the carrier of Y:]
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:];
reconsider x1 = x`1, y1 = y`1 as Element of X;
reconsider x2 = x`2, y2 = y`2 as Element of Y;
A1: x = [x1,x2] & y = [y1,y2];
then dist_cart2S(X,Y).(x,y) = sqrt((dist(y1,x1))^2 + (dist(x2,y2))^2) by
Def10
.= dist_cart2S(X,Y).(y,x) by A1,Def10;
hence thesis;
end;
theorem Th12: :::
for a,b,c,d being 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 Real;
assume 0 <= a & 0 <= b & 0 <= c & 0 <= d;
then 0 <= a*c & 0 <= d*b by XREAL_1:127;
then
A1: 0 + 0 <= a*c + d*b by XREAL_1:7;
0 <= d^2 & 0 <= c^2 by XREAL_1:63;
then
A2: 0 + 0 <= c^2 + d^2 by XREAL_1:7;
then
A3: 0 <= sqrt(c^2 + d^2) by SQUARE_1:def 2;
0 <= ((a*d) - (c*b))^2 by XREAL_1:63;
then 0 <= (a^2*d^2 + c^2*b^2) - 2*(a*d)*(c*b);
then 0 + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) by XREAL_1:19;
then (b^2*d^2) + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) + (b^2*d^2 ) by
XREAL_1:6;
then
A4: (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 XREAL_1:6;
0 <= a^2 & 0 <= b^2 by XREAL_1:63;
then
A5: 0 + 0 <= a^2 + b^2 by XREAL_1:7;
then 0 <= sqrt(a^2 + b^2) by SQUARE_1:def 2;
then
A6: 0 + 0 <= sqrt(a^2 + b^2) + sqrt(c^2 + d^2) by A3,XREAL_1:7;
0 <= (a*c + d*b)^2 by XREAL_1:63;
then sqrt((a*c + d*b)^2) <= sqrt((a^2 + b^2)*(c^2 + d^2)) by A4,SQUARE_1:26;
then 2*sqrt((a*c + d*b)^2) <= 2*(sqrt((a^2 + b^2)*(c^2 + d^2))) by XREAL_1:64
;
then 2*sqrt((a*c + d*b)^2) <= 2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2)) by A5,A2,
SQUARE_1:29;
then 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)) by A1,SQUARE_1:22;
then b^2 + 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)) + b^2 by
XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
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);
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 2;
then
A7: (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 A2,SQUARE_1:def 2;
0 <= (a + c)^2 & 0 <= (d + b)^2 by XREAL_1:63;
then 0 + 0 <= (a + c)^2 + (d + b)^2 by XREAL_1:7;
then
sqrt((a + c)^2 + (d + b)^2) <= sqrt((sqrt(a^2 + b^2) + sqrt(c^2 + d^2))
^2) by A7,SQUARE_1:26;
hence thesis by A6,SQUARE_1:22;
end;
theorem Th13:
for x,y,z being Element of [:the carrier of X,the carrier of Y:]
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:];
reconsider x1 = x`1, y1 = y`1, z1 = z`1 as Element of X;
reconsider x2 = x`2, y2 = y`2, z2 = z`2 as Element of Y;
A1: x = [x1,x2];
set d5 = dist(x2,y2);
set d3 = dist(y1,z1);
set d1 = dist(x1,z1);
A2: y = [y1,y2];
set d6 = dist(y2,z2);
set d4 = dist(x2,z2);
set d2 = dist(x1,y1);
A3: z = [z1,z2];
0 <= d1^2 & 0 <= d4^2 by XREAL_1:63;
then
A4: 0 + 0 <= d1^2 + d4^2 by XREAL_1:7;
d4 <= d5 + d6 & 0 <= d4 by METRIC_1:4,5;
then
A5: d4^2 <= (d5 + d6)^2 by SQUARE_1:15;
d1 <= d2 + d3 & 0 <= d1 by METRIC_1:4,5;
then d1^2 <= (d2 + d3)^2 by SQUARE_1:15;
then d1^2 + d4^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A5,XREAL_1:7;
then
A6: sqrt(d1^2 + d4^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2) by A4,SQUARE_1:26;
A7: 0 <= d5 & 0 <= d6 by METRIC_1:5;
0 <= d2 & 0 <= d3 by METRIC_1:5;
then
sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2+ d6^2)
by A7,Th12;
then sqrt(d1^2 + d4^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2) by A6,
XXREAL_0:2;
then
dist_cart2S(X,Y).(x,z) <= sqrt((d2)^2 + (d5)^2) + sqrt((d3)^2 + (d6)^2)
by A1,A3,Def10;
then
dist_cart2S(X,Y).(x,z) <= dist_cart2S(X,Y).(x,y) + sqrt((d3)^2 + (d6)^2
) by A1,A2,Def10;
hence thesis by A2,A3,Def10;
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
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 x9 = x, y9 = y, z9 = z as Element of [:the carrier of X,the
carrier of Y:];
A1: dist(x,y) = dist_cart2S(X,Y).(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th10;
dist(y,x) = dist_cart2S(X,Y).(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th11;
dist(x,z) = dist_cart2S(X,Y).(x9,z9) & dist(y,z) = dist_cart2S(X,Y).
(y9,z9) by METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th13;
end;
hence thesis by METRIC_1:6;
end;
end;
begin :: Metrics in the Cartesian Product of Three Sets
reserve Z for non empty MetrSpace;
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
:Def13:
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)
= In(sqrt((dist($1,$2))^2 + (dist($3,$4))^2 + (dist($5,$6))^2),REAL);
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:];
assume x = [x1,x2,x3] & y = [y1,y2,y3];
then F.(x,y) = G(x1,y1,x2,y2,x3,y3) by A1;
hence thesis;
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
A2: 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
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 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
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1 be Element of X, y2 be Element of Y, y3 be Element of Z such
that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2
) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th14:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z:] 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:];
reconsider x1 = x`1_3, y1 = y`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3 as Element of Z;
A1: x = [x1,x2,x3] & y = [y1,y2,y3];
thus dist_cart3S(X,Y,Z).(x,y) = 0 implies x = y
proof
set d3 = dist(x3,y3);
set d2 = dist(x2,y2);
set d1 = dist(x1,y1);
A2: 0 <= d2^2 & 0 <= d3^2 by XREAL_1:63;
assume dist_cart3S(X,Y,Z).(x,y) = 0;
then sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,Def13;
then
A3: sqrt(d1^2 + (d2^2 + d3^2)) = 0;
0 <= d2^2 & 0 <= d3^2 by XREAL_1:63;
then
A4: 0 <= d1^2 & 0 + 0 <= d2^2 + d3^2 by XREAL_1:7,63;
then d1 = 0 by A3,Lm1;
then
A5: x1 = y1 by METRIC_1:2;
A6: d2^2 + d3^2 = 0 by A3,A4,Lm1;
then d2 = 0 by A2,XREAL_1:27;
then
A7: x2 = y2 by METRIC_1:2;
d3 = 0 by A6,A2,XREAL_1:27;
hence thesis by A1,A5,A7,METRIC_1:2;
end;
assume
A8: x = y;
then
A9: (dist(x1,y1))^2 = 0^2 & (dist(x2,y2))^2 = 0^2 by METRIC_1:1;
dist_cart3S(X,Y,Z).(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (
dist(x3,y3))^2) by A1,Def13
.= 0^2 by A8,A9,METRIC_1:1,SQUARE_1:17;
hence thesis;
end;
theorem Th15:
for x,y being Element of [:the carrier of X,the carrier of Y,the
carrier of Z:] 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:];
reconsider x1 = x`1_3, y1 = y`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3 as Element of Z;
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 Def13
.= dist_cart3S(X,Y,Z).(y,x) by A1,Def13;
hence thesis;
end;
theorem Th16: :::
for a,b,c,d,e,f being 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 Real;
0 <= ((a*f) - (e*c))^2 & 0 <= ((b*f) - (e*d))^2 by XREAL_1:63;
then
0 <= ((a*d) - (c*b))^2 & 0 + 0 <= ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2
by XREAL_1:7,63;
then
0 + 0 <= ((a*d) - (c*b))^2 + (((a*f) - (e*c))^2 + ((b*f) - (e*d))^2) by
XREAL_1:7;
then
0 <= (((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2) - 2*(
a*d)*(c*b);
then
0 + 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 + ((b*f) -
(e*d))^2 by XREAL_1:19;
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);
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 XREAL_1:19;
hence thesis by XREAL_1:19;
end;
theorem Th17: :::
for a,b,c,d,e,f being 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 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 Th16;
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
XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
hence thesis;
end;
Lm2: for a,b,c,d,e,f being 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 Real;
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: 0 <= c and
A4: 0 <= d & 0 <= e & 0 <= f;
0 <= b*d & 0 <= e*f by A2,A4,XREAL_1:127;
then
A5: 0 + 0 <= b*d + e*f by XREAL_1:7;
0 <= c^2 & 0 <= d^2 by XREAL_1:63;
then
A6: 0 + 0 <= c^2 + d^2 by XREAL_1:7;
0 <= f^2 by XREAL_1:63;
then
A7: 0 + 0 <= (c^2 + d^2) + f^2 by A6,XREAL_1:7;
then
A8: 0 <= sqrt(c^2 + d^2 + f^2) by SQUARE_1:def 2;
0 <= ((a*c) + (b*d) + (e*f))^2 by XREAL_1:63;
then
A9: sqrt(((a*c) + (b*d) + (e*f))^2) <= sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f
^2)) by Th17,SQUARE_1:26;
0 <= a^2 & 0 <= b^2 by XREAL_1:63;
then
A10: 0 + 0 <= a^2 + b^2 by XREAL_1:7;
0 <= e^2 by XREAL_1:63;
then
A11: 0 + 0 <= (a^2 + b^2) + e^2 by A10,XREAL_1:7;
0 <= a*c by A1,A3,XREAL_1:127;
then 0 + 0 <= a*c + (b*d + e*f) by A5,XREAL_1:7;
then ((a*c) + (b*d) + (e*f)) <= sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f ^2))
by A9,SQUARE_1:22;
then
((a*c) + (b*d) + (e*f)) <= sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f ^2)
by A11,A7,SQUARE_1:29;
then 2*((a*c) + (b*d) + (e*f)) <= 2*(sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 +
f^2)) by XREAL_1:64;
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 XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
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 XREAL_1:6;
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
XREAL_1:6;
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));
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 A11,
SQUARE_1:def 2;
then
A12: ((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
A7,SQUARE_1:def 2;
0 <= (a + c)^2 & 0 <= (b + d)^2 by XREAL_1:63;
then
A13: 0 + 0 <= (a + c)^2 + (b + d)^2 by XREAL_1:7;
0 <= (e + f)^2 by XREAL_1:63;
then 0 + 0 <= ((a + c)^2 + (b + d)^2) + (e + f)^2 by A13,XREAL_1:7;
then
A14: 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 A12,SQUARE_1:26;
0 <= sqrt(a^2 + b^2 + e^2) by A11,SQUARE_1:def 2;
then 0 + 0 <= (sqrt(a^2 + b^2 + e^2) + sqrt(c^2 + d^2 + f^2 )) by A8,
XREAL_1:7;
hence thesis by A14,SQUARE_1:22;
end;
theorem Th18:
for x,y,z being Element of [:the carrier of X,the carrier of Y,
the carrier of Z:] 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
:];
reconsider x1 = x`1_3, y1 = y`1_3, z1 = z`1_3 as Element of X;
reconsider x2 = x`2_3, y2 = y`2_3, z2 = z`2_3 as Element of Y;
reconsider x3 = x`3_3, y3 = y`3_3, z3 = z`3_3 as Element of Z;
A1: x = [x1,x2,x3];
set d7 = dist(x3,z3), d8 = dist(x3,y3), d9 = dist(y3,z3);
set d1 = dist(x1,z1), d2 = dist(x1,y1), d3 = dist(y1,z1);
A2: y = [y1,y2,y3];
d7 <= d8 + d9 & 0 <= d7 by METRIC_1:4,5;
then
A3: d7^2 <= (d8 + d9)^2 by SQUARE_1:15;
A4: 0 <= d8 & 0 <= d9 by METRIC_1:5;
set d4 = dist(x2,z2), d5 = dist(x2,y2), d6 = dist(y2,z2);
A5: z = [z1,z2,z3];
d4 <= d5 + d6 & 0 <= d4 by METRIC_1:4,5;
then
A6: d4^2 <= (d5 + d6)^2 by SQUARE_1:15;
A7: 0 <= d5 & 0 <= d6 by METRIC_1:5;
0 <= d1^2 & 0 <= d4^2 by XREAL_1:63;
then
A8: 0 + 0 <= d1^2 + d4^2 by XREAL_1:7;
d1 <= d2 + d3 & 0 <= d1 by METRIC_1:4,5;
then d1^2 <= (d2 + d3)^2 by SQUARE_1:15;
then d1^2 + d4^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A6,XREAL_1:7;
then
A9: d1^2 + d4^2 + d7^2 <= (d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2 by A3,
XREAL_1:7;
0 <= d7^2 by XREAL_1:63;
then 0 + 0 <= (d1^2 + d4^2) + d7^2 by A8,XREAL_1:7;
then
A10: sqrt(d1^2 + d4^2 + d7^2) <= sqrt((d2 + d3)^2 + (d5 + d6) ^2 + (d8 + d9)
^2) by A9,SQUARE_1:26;
0 <= d2 & 0 <= d3 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 A7,A4,Lm2;
then
sqrt(d1^2 + d4^2 + d7^2) <= sqrt(d2^2 + d5^2 + d8^2) + sqrt(d3^2 + d6^2
+ d9^2) by A10,XXREAL_0:2;
then dist_cart3S(X,Y,Z).(x,z) <= sqrt(d2^2 + d5^2 + d8^2) + sqrt((d3)^2 + (
d6)^2 + d9^2 ) by A1,A5,Def13;
then dist_cart3S(X,Y,Z).(x,z) <= dist_cart3S(X,Y,Z).(x,y) + sqrt((d3)^2 + (
d6)^2 + d9^2) by A1,A2,Def13;
hence thesis by A2,A5,Def13;
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
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 x9 = x,y9 = y,z9 = z as Element of [:the carrier of X,the
carrier of Y,the carrier of Z:];
A1: dist(x,y) = dist_cart3S(X,Y,Z).(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th14;
dist(y,x) = dist_cart3S(X,Y,Z).(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th15;
dist(x,z) = dist_cart3S(X,Y,Z).(x9,z9) & dist(y,z) = dist_cart3S(X,Y
,Z).(y9, z9) by METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th18;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func taxi_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
:
Def16: 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:];
assume x = [x1,x2] & y = [y1,y2];
hence thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
assume that
A2: 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
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 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,x2 be Element of REAL such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1,y2 be Element of REAL such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th19:
for x,y being Element of [:REAL,REAL:] holds taxi_dist2.(x,y) = 0 iff x = y
proof
let x,y be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of REAL;
A1: x = [x1,x2] & y = [y1,y2];
thus taxi_dist2.(x,y) = 0 implies x = y
proof
set d2 = real_dist.(x2,y2);
set d1 = real_dist.(x1,y1);
d1 = |.x1 - y1.| by METRIC_1:def 12;
then
A2: 0 <= d1 by COMPLEX1:46;
d2 = |.x2 - y2.| by METRIC_1:def 12;
then
A3: 0 <= d2 by COMPLEX1:46;
assume taxi_dist2.(x,y) = 0;
then
A4: d1 + d2 = 0 by A1,Def16;
then d1 = 0 by A2,A3,XREAL_1:27;
then
A5: x1 = y1 by METRIC_1:8;
d2 = 0 by A4,A2,A3,XREAL_1:27;
hence thesis by A1,A5,METRIC_1:8;
end;
assume
A6: x = y;
then
A7: real_dist.(x2,y2) = 0 by METRIC_1:8;
taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A1,Def16
.= 0 by A6,A7,METRIC_1:8;
hence thesis;
end;
theorem Th20:
for x,y being Element of [:REAL,REAL:] holds taxi_dist2.(x,y) =
taxi_dist2.(y,x)
proof
let x,y be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of REAL;
A1: x = [x1,x2] & y = [y1,y2];
then taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by Def16
.= real_dist.(y1,x1) + real_dist.(x2,y2) by METRIC_1:9
.= real_dist.(y1,x1) + real_dist.(y2,x2) by METRIC_1:9
.= taxi_dist2.(y,x) by A1,Def16;
hence thesis;
end;
theorem Th21:
for x,y,z being Element of [:REAL,REAL:] holds taxi_dist2.(x,z)
<= taxi_dist2.(x,y) + taxi_dist2.(y,z)
proof
let x,y,z be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2, z1 = z`1, z2 = z`2 as
Element of REAL;
A1: y = [y1,y2];
set d5 = real_dist.(x2,y2), d6 = real_dist.(y2,z2);
set d3 = real_dist.(y1,z1), d4 = real_dist.(x2,z2);
set d1 = real_dist.(x1,z1), d2 = real_dist.(x1,y1);
A2: z = [z1,z2];
A3: x = [x1,x2];
then
A4: taxi_dist2.(x,z) = d1 + d4 by A2,Def16;
A5: d1 <= d2 + d3 & d4 <= d5 + d6 by METRIC_1:10;
(d2 + d3) + (d5 + d6) = (d2 + d5) + (d3 + d6)
.= taxi_dist2.(x,y) + (d3 +d6) by A3,A1,Def16
.= taxi_dist2.(x,y) + taxi_dist2.(y,z) by A1,A2,Def16;
hence thesis by A5,A4,XREAL_1:7;
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 x9 = x,y9 = y,z9 = z as Element of [:REAL,REAL:];
A1: dist(x,y) = taxi_dist2.(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th19;
dist(y,x) = taxi_dist2.(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th20;
dist(x,z) = taxi_dist2.(x9,z9) & dist(y,z) = taxi_dist2.(y9,z9) by
METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th21;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func Eukl_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
:
Def18: 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)
= In(sqrt((real_dist.($1,$2))^2 + (real_dist.($3,$4)^2)),REAL);
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:];
assume x = [x1,x2] & y = [y1,y2];
then F.(x,y) = G(x1,y1,x2,y2) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
assume that
A2: 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
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 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,x2 be Element of REAL such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1,y2 be Element of REAL such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1.(x,y)=sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)) by A2
,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th22:
for x,y being Element of [:REAL,REAL:] holds Eukl_dist2.(x,y) = 0 iff x = y
proof
let x,y be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of REAL;
A1: x = [x1,x2] & y = [y1,y2];
thus Eukl_dist2.(x,y) = 0 implies x = y
proof
set d2 = real_dist.(x2,y2);
set d1 = real_dist.(x1,y1);
assume Eukl_dist2.(x,y) = 0;
then
A2: sqrt(d1^2 + d2^2) = 0 by A1,Def18;
A3: 0 <= d1^2 & 0 <= d2^2 by XREAL_1:63;
then d1 = 0 by A2,Lm1;
then
A4: x1 = y1 by METRIC_1:8;
d2 = 0 by A2,A3,Lm1;
hence thesis by A1,A4,METRIC_1:8;
end;
assume x = y;
then
A5: (real_dist.(x1,y1))^2 = 0^2 & (real_dist.(x2,y2))^2 = 0^2 by METRIC_1:8;
Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2) ) ^2
) by A1,Def18
.= 0 by A5;
hence thesis;
end;
theorem Th23:
for x,y being Element of [:REAL,REAL:] holds Eukl_dist2.(x,y) =
Eukl_dist2.(y,x)
proof
let x,y be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of REAL;
A1: x = [x1,x2] & y = [y1,y2];
then
Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2) ^2))
by Def18
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2)) by METRIC_1:9
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)) by METRIC_1:9
.= Eukl_dist2.(y,x) by A1,Def18;
hence thesis;
end;
theorem Th24:
for x,y,z being Element of [:REAL,REAL:] holds Eukl_dist2.(x,z)
<= Eukl_dist2.(x,y) + Eukl_dist2.(y,z)
proof
let x,y,z be Element of [:REAL,REAL:];
reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2, z1 = z`1, z2 = z`2 as
Element of REAL;
A1: x = [x1,x2];
set d5 = real_dist.(x2,y2);
set d3 = real_dist.(y1,z1);
set d1 = real_dist.(x1,z1);
A2: y = [y1,y2];
set d6 = real_dist.(y2,z2);
set d4 = real_dist.(x2,z2);
set d2 = real_dist.(x1,y1);
A3: z = [z1,z2];
d4 = |.x2 - z2.| by METRIC_1:def 12;
then 0 <= d4 by COMPLEX1:46;
then
A4: d4^2 <= (d5 + d6)^2 by METRIC_1:10,SQUARE_1:15;
0 <= d1^2 & 0 <= d4^2 by XREAL_1:63;
then
A5: 0 + 0 <= d1^2 + d4^2 by XREAL_1:7;
d1 = |.x1 - z1.| by METRIC_1:def 12;
then 0 <= d1 by COMPLEX1:46;
then d1^2 <= (d2 + d3)^2 by METRIC_1:10,SQUARE_1:15;
then d1^2 + d4^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A4,XREAL_1:7;
then
A6: sqrt(d1^2 + d4^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2) by A5,SQUARE_1:26;
d6 = |.y2 - z2.| by METRIC_1:def 12;
then
A7: 0 <= d6 by COMPLEX1:46;
d5 = |.x2 - y2.| by METRIC_1:def 12;
then
A8: 0 <= d5 by COMPLEX1:46;
d3 = |.y1 - z1.| by METRIC_1:def 12;
then
A9: 0 <= d3 by COMPLEX1:46;
d2 = |.x1 - y1.| by METRIC_1:def 12;
then 0 <= d2 by COMPLEX1:46;
then
sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2
) by A9,A8,A7,Th12;
then sqrt(d1^2 + d4^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2) by A6,
XXREAL_0:2;
then Eukl_dist2.(x,z) <= sqrt(d2^2 + (d5)^2) + sqrt(d3^2 + d6^2) by A1,A3
,Def18;
then Eukl_dist2.(x,z) <= Eukl_dist2.(x,y) + sqrt(d3^2 + d6^2) by A1,A2,Def18;
hence thesis by A2,A3,Def18;
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 x9 = x,y9 = y,z9 = z as Element of [:REAL,REAL:];
A1: dist(x,y) = Eukl_dist2.(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th22;
dist(y,x) = Eukl_dist2.(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th23;
dist(x,z) = Eukl_dist2.(x9,z9) & dist(y,z) = Eukl_dist2.(y9,z9) by
METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th24;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func taxi_dist3 -> Function of [:[:REAL,REAL,REAL:], [:REAL,REAL,REAL:]:],
REAL means
:Def20:
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:];
assume x = [x1,x2,x3] & y = [y1,y2,y3];
hence thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
assume that
A2: 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
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 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,x2,x3 be Element of REAL such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1,y2,y3 be Element of REAL such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3
) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th25:
for x,y being Element of [:REAL,REAL,REAL:] holds
taxi_dist3.(x,y) = 0 iff x = y
proof
let x,y be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3 as
Element of REAL;
A1: x = [x1,x2,x3] & y = [y1,y2,y3];
thus taxi_dist3.(x,y) = 0 implies x = y
proof
set d3 = real_dist.(x3,y3);
set d2 = real_dist.(x2,y2);
set d1 = real_dist.(x1,y1);
set d4 = d1 + d2;
d3 = |.x3 - y3.| by METRIC_1:def 12;
then
A2: 0 <= d3 by COMPLEX1:46;
d1 = |.x1 - y1.| by METRIC_1:def 12;
then
A3: 0 <= d1 by COMPLEX1:46;
assume taxi_dist3.(x,y) = 0;
then
A4: d4 + d3 = 0 by A1,Def20;
d2 = |.x2 - y2.| by METRIC_1:def 12;
then
A5: 0 <= d2 by COMPLEX1:46;
then
A6: 0 + 0 <= d1 + d2 by A3,XREAL_1:7;
then
A7: d4 = 0 by A4,A2,XREAL_1:27;
then d1 = 0 by A5,A3,XREAL_1:27;
then
A8: x1 = y1 by METRIC_1:8;
d3 = 0 by A4,A2,A6,XREAL_1:27;
then
A9: x3 = y3 by METRIC_1:8;
d2 = 0 by A5,A3,A7,XREAL_1:27;
hence thesis by A1,A9,A8,METRIC_1:8;
end;
assume
A10: x = y;
then
A11: real_dist.(x1,y1) = 0 & real_dist.(x2,y2) = 0 by METRIC_1:8;
taxi_dist3.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(
x3,y3) by A1,Def20
.= 0 by A10,A11,METRIC_1:8;
hence thesis;
end;
theorem Th26:
for x,y being Element of [:REAL,REAL,REAL:] holds taxi_dist3.(x,
y) = taxi_dist3.(y,x)
proof
let x,y be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3 as
Element of REAL;
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 Def20
.= real_dist.(y1,x1) + real_dist.(x2,y2) + real_dist.(x3,y3) by METRIC_1:9
.= real_dist.(y1,x1) + real_dist.(y2,x2) + real_dist.(x3,y3) by METRIC_1:9
.= real_dist.(y1,x1) + real_dist.(y2,x2) + real_dist.(y3,x3) by METRIC_1:9
.= taxi_dist3.(y,x) by A1,Def20;
hence thesis;
end;
theorem Th27:
for x,y,z being Element of [:REAL,REAL,REAL:] holds taxi_dist3.(
x,z) <= taxi_dist3.(x,y) + taxi_dist3.(y,z)
proof
let x,y,z be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3, z1 =
z`1_3, z2 = z`2_3, z3 = z`3_3 as Element of REAL;
A1: x = [x1,x2,x3];
set d7 = real_dist.(x3,z3), d8 = real_dist.(x3,y3);
set d3 = real_dist.(y1,z1), d4 = real_dist.(x2,z2);
A2: z = [z1,z2,z3];
set d9 = real_dist.(y3,z3);
set d5 = real_dist.(x2,y2), d6 = real_dist.(y2,z2);
set d1 = real_dist.(x1,z1), d2 = real_dist.(x1,y1);
A3: y = [y1,y2,y3];
set d10 = d1 + d4;
d1 <= d2 + d3 & d4 <= d5 + d6 by METRIC_1:10;
then
A4: d10 <= (d2 + d3) + (d5 + d6) by XREAL_1:7;
d7 <= d8 + d9 by METRIC_1:10;
then
A5: d10 + d7 <= ((d2 + d3) + (d5 + d6)) + (d8 + d9) by A4,XREAL_1:7;
((d2 + d3) + (d5 + d6)) + (d8 + d9) = ((d2 + d5) + d8) + ((d3 + d6) + d9)
.= taxi_dist3.(x,y) + ((d3 +d6) + d9) by A1,A3,Def20
.= taxi_dist3.(x,y) + taxi_dist3.(y,z) by A3,A2,Def20;
hence thesis by A1,A2,A5,Def20;
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 x9 = x,y9 = y,z9 = z as Element of [:REAL,REAL,REAL:];
A1: dist(x,y) = taxi_dist3.(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th25;
dist(y,x) = taxi_dist3.(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th26;
dist(x,z) = taxi_dist3.(x9,z9) & dist(y,z) = taxi_dist3.(y9,z9) by
METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th27;
end;
hence thesis by METRIC_1:6;
end;
end;
definition
func Eukl_dist3 -> Function of [:[:REAL,REAL,REAL:], [:REAL,REAL,REAL:]:],
REAL means
:Def22:
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)
= In(sqrt((real_dist.($1,$2))^2 + (real_dist.($3,
$4)^2) + (real_dist.($5,$6)^2)),REAL);
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:];
assume x = [x1,x2,x3] & y = [y1,y2,y3];
then F.(x,y) = G(x1,y1,x2,y2,x3,y3) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
assume that
A2: 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
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 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,x2,x3 be Element of REAL such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1, y2, y3 be Element of REAL such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2) + (
real_dist.(x3,y3)^2)) by A2,A4,A5
.= f2.(x,y) by A3,A4,A5;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th28:
for x,y being Element of [:REAL,REAL,REAL:] holds
Eukl_dist3.(x,y) = 0 iff x = y
proof
let x,y be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3 as
Element of REAL;
A1: x = [x1,x2,x3] & y = [y1,y2,y3];
thus Eukl_dist3.(x,y) = 0 implies x = y
proof
set d3 = real_dist.(x3,y3);
set d2 = real_dist.(x2,y2);
set d1 = real_dist.(x1,y1);
A2: 0 <= d2^2 & 0 <= d3^2 by XREAL_1:63;
assume Eukl_dist3.(x,y) = 0;
then sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,Def22;
then
A3: sqrt(d1^2 + (d2^2 + d3^2)) =0;
0 <= d2^2 & 0 <= d3^2 by XREAL_1:63;
then
A4: 0 <= d1^2 & 0 + 0 <= d2^2 + d3^2 by XREAL_1:7,63;
then d1 = 0 by A3,Lm1;
then
A5: x1 = y1 by METRIC_1:8;
A6: d2^2 + d3^2 = 0 by A3,A4,Lm1;
then d2 = 0 by A2,XREAL_1:27;
then
A7: x2 = y2 by METRIC_1:8;
d3 = 0 by A6,A2,XREAL_1:27;
hence thesis by A1,A5,A7,METRIC_1:8;
end;
assume
A8: x = y;
then
A9: (real_dist.(x1,y1))^2 = 0^2 & (real_dist.(x2,y2))^2 = 0^2 by METRIC_1:8;
Eukl_dist3.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2))^2 +
(real_dist.(x3,y3))^2) by A1,Def22
.= 0^2 by A8,A9,METRIC_1:8,SQUARE_1:17;
hence thesis;
end;
theorem Th29:
for x,y being Element of [:REAL,REAL,REAL:] holds Eukl_dist3.(x,
y) = Eukl_dist3.(y,x)
proof
let x,y be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3 as
Element of REAL;
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 Def22
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2) + (real_dist.(x3,
y3)^2)) by METRIC_1:9
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2) + (real_dist.(x3,
y3)^2)) by METRIC_1:9
.= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2) + (real_dist.(y3,
x3)^2)) by METRIC_1:9
.= Eukl_dist3.(y,x) by A1,Def22;
hence thesis;
end;
theorem Th30:
for x,y,z being Element of [:REAL,REAL,REAL:] holds Eukl_dist3.(
x,z) <= Eukl_dist3.(x,y) + Eukl_dist3.(y,z)
proof
let x,y,z be Element of [:REAL,REAL,REAL:];
reconsider x1 = x`1_3, x2 = x`2_3, x3 = x`3_3,
y1 = y`1_3, y2 = y`2_3, y3 = y`3_3, z1 =
z`1_3, z2 = z`2_3, z3 = z`3_3 as Element of REAL;
A1: x = [x1,x2,x3];
set d9 = real_dist.(y3,z3);
set d5 = real_dist.(x2,y2), d6 = real_dist.(y2,z2);
set d1 = real_dist.(x1,z1), d2 = real_dist.(x1,y1);
A2: y = [y1,y2,y3];
d9 = |.y3 - z3.| by METRIC_1:def 12;
then
A3: 0 <= d9 by COMPLEX1:46;
d6 = |.y2 - z2.| by METRIC_1:def 12;
then
A4: 0 <= d6 by COMPLEX1:46;
d5 = |.x2 - y2.| by METRIC_1:def 12;
then
A5: 0 <= d5 by COMPLEX1:46;
set d7 = real_dist.(x3,z3), d8 = real_dist.(x3,y3);
set d3 = real_dist.(y1,z1), d4 = real_dist.(x2,z2);
A6: z = [z1,z2,z3];
d7 = |.x3 - z3.| by METRIC_1:def 12;
then 0 <= d7 by COMPLEX1:46;
then
A7: d7^2 <= (d8 + d9)^2 by METRIC_1:10,SQUARE_1:15;
d4 = |.x2 - z2.| by METRIC_1:def 12;
then 0 <= d4 by COMPLEX1:46;
then
A8: d4^2 <= (d5 + d6)^2 by METRIC_1:10,SQUARE_1:15;
d1 = |.x1 - z1.| by METRIC_1:def 12;
then 0 <= d1 by COMPLEX1:46;
then d1^2 <= (d2 + d3)^2 by METRIC_1:10,SQUARE_1:15;
then d1^2 + d4^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A8,XREAL_1:7;
then
A9: d1^2 + d4^2 + d7^2 <= (d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2 by A7,
XREAL_1:7;
0 <= d1^2 & 0 <= d4^2 by XREAL_1:63;
then
A10: 0 + 0 <= d1^2 + d4^2 by XREAL_1:7;
0 <= d7^2 by XREAL_1:63;
then 0 + 0 <= (d1^2 + d4^2) + d7^2 by A10,XREAL_1:7;
then
A11: sqrt(d1^2 + d4^2 + d7^2) <= sqrt((d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)
^2) by A9,SQUARE_1:26;
d8 = |.x3 - y3.| by METRIC_1:def 12;
then
A12: 0 <= d8 by COMPLEX1:46;
d3 = |.y1 - z1.| by METRIC_1:def 12;
then
A13: 0 <= d3 by COMPLEX1:46;
d2 = |.x1 - y1.| by METRIC_1:def 12;
then 0 <= d2 by COMPLEX1:46;
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 A13,A5,A4,A12,A3,Lm2;
then
sqrt(d1^2 + d4^2 + d7^2) <= sqrt(d2^2 + d5^2 + d8^2) + sqrt(d3^2 + d6^2
+ d9^2) by A11,XXREAL_0:2;
then
Eukl_dist3.(x,z) <= sqrt(d2^2 + d5^2 + d8^2) + sqrt(d3^2 + d6^2 + d9^2)
by A1,A6,Def22;
then Eukl_dist3.(x,z) <= Eukl_dist3.(x,y) + sqrt((d3)^2 + (d6)^2 + d9^2) by
A1,A2,Def22;
hence thesis by A2,A6,Def22;
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 x9 = x,y9 = y,z9 = z as Element of [:REAL,REAL,REAL:];
A1: dist(x,y) = Eukl_dist3.(x9,y9) by METRIC_1:def 1;
hence dist(x,y) = 0 iff x = y by Th28;
dist(y,x) = Eukl_dist3.(y9,x9) by METRIC_1:def 1;
hence dist(x,y) = dist(y,x) by A1,Th29;
dist(x,z) = Eukl_dist3.(x9,z9) & dist(y,z) = Eukl_dist3.(y9,z9) by
METRIC_1:def 1;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,Th30;
end;
hence thesis by METRIC_1:6;
end;
end;