:: METRIC_3 semantic presentation

scheme :: METRIC_3:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set , set , set ) -> Element of F3() } :
ex b1 being Function of [:[:F1(),F2():],[:F1(),F2():]:],F3() st
for b2, b3 being Element of F1()
for b4, b5 being Element of F2()
for b6, b7 being Element of [:F1(),F2():] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . [b6,b7] = F4(b2,b3,b4,b5)
proof end;

definition
let c1, c2 be non empty MetrSpace;
func dist_cart2 c1,c2 -> Function of [:[:the carrier of a1,the carrier of a2:],[:the carrier of a1,the carrier of a2:]:], REAL means :Def1: :: METRIC_3:def 1
for b1, b2 being Element of a1
for b3, b4 being Element of a2
for b5, b6 being Element of [:the carrier of a1,the carrier of a2:] st b5 = [b1,b3] & b6 = [b2,b4] holds
a3 . b5,b6 = (dist b1,b2) + (dist b3,b4);
existence
ex b1 being Function of [:[:the carrier of c1,the carrier of c2:],[:the carrier of c1,the carrier of c2:]:], REAL st
for b2, b3 being Element of c1
for b4, b5 being Element of c2
for b6, b7 being Element of [:the carrier of c1,the carrier of c2:] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = (dist b2,b3) + (dist b4,b5)
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of c1,the carrier of c2:],[:the carrier of c1,the carrier of c2:]:], REAL st ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of [:the carrier of c1,the carrier of c2:] st b7 = [b3,b5] & b8 = [b4,b6] holds
b1 . b7,b8 = (dist b3,b4) + (dist b5,b6) ) & ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of [:the carrier of c1,the carrier of c2:] st b7 = [b3,b5] & b8 = [b4,b6] holds
b2 . b7,b8 = (dist b3,b4) + (dist b5,b6) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines dist_cart2 METRIC_3:def 1 :
for b1, b2 being non empty MetrSpace
for b3 being Function of [:[:the carrier of b1,the carrier of b2:],[:the carrier of b1,the carrier of b2:]:], REAL holds
( b3 = dist_cart2 b1,b2 iff for b4, b5 being Element of b1
for b6, b7 being Element of b2
for b8, b9 being Element of [:the carrier of b1,the carrier of b2:] st b8 = [b4,b6] & b9 = [b5,b7] holds
b3 . b8,b9 = (dist b4,b5) + (dist b6,b7) );

theorem Th1: :: METRIC_3:1
canceled;

theorem Th2: :: METRIC_3:2
canceled;

theorem Th3: :: METRIC_3:3
canceled;

theorem Th4: :: METRIC_3:4
canceled;

theorem Th5: :: METRIC_3:5
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds
( (dist_cart2 b1,b2) . b3,b4 = 0 iff b3 = b4 )
proof end;

theorem Th6: :: METRIC_3:6
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds (dist_cart2 b1,b2) . b3,b4 = (dist_cart2 b1,b2) . b4,b3
proof end;

theorem Th7: :: METRIC_3:7
for b1, b2 being non empty MetrSpace
for b3, b4, b5 being Element of [:the carrier of b1,the carrier of b2:] holds (dist_cart2 b1,b2) . b3,b5 <= ((dist_cart2 b1,b2) . b3,b4) + ((dist_cart2 b1,b2) . b4,b5)
proof end;

definition
let c1, c2 be non empty MetrSpace;
let c3, c4 be Element of [:the carrier of c1,the carrier of c2:];
func dist2 c3,c4 -> Real equals :: METRIC_3:def 2
(dist_cart2 a1,a2) . a3,a4;
coherence
(dist_cart2 c1,c2) . c3,c4 is Real ;
end;

:: deftheorem Def2 defines dist2 METRIC_3:def 2 :
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds dist2 b3,b4 = (dist_cart2 b1,b2) . b3,b4;

registration
let c1 be non empty set ;
let c2 be Function of [:c1,c1:], REAL ;
cluster MetrStruct(# a1,a2 #) -> non empty ;
coherence
not MetrStruct(# c1,c2 #) is empty by STRUCT_0:def 1;
end;

definition
let c1, c2 be non empty MetrSpace;
func MetrSpaceCart2 c1,c2 -> non empty strict MetrSpace equals :: METRIC_3:def 3
 MetrStruct(# [:the carrier of a1,the carrier of a2:],(dist_cart2 a1,a2) #);
coherence
MetrStruct(# [:the carrier of c1,the carrier of c2:],(dist_cart2 c1,c2) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def3 defines MetrSpaceCart2 METRIC_3:def 3 :
for b1, b2 being non empty MetrSpace holds MetrSpaceCart2 b1,b2 = MetrStruct(# [:the carrier of b1,the carrier of b2:],(dist_cart2 b1,b2) #);

scheme :: METRIC_3:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5( set , set , set , set , set , set ) -> Element of F4() } :
ex b1 being Function of [:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4() st
for b2, b3 being Element of F1()
for b4, b5 being Element of F2()
for b6, b7 being Element of F3()
for b8, b9 being Element of [:F1(),F2(),F3():] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . [b8,b9] = F5(b2,b3,b4,b5,b6,b7)
proof end;

definition
let c1, c2, c3 be non empty MetrSpace;
func dist_cart3 c1,c2,c3 -> Function of [:[:the carrier of a1,the carrier of a2,the carrier of a3:],[:the carrier of a1,the carrier of a2,the carrier of a3:]:], REAL means :Def4: :: METRIC_3:def 4
for b1, b2 being Element of a1
for b3, b4 being Element of a2
for b5, b6 being Element of a3
for b7, b8 being Element of [:the carrier of a1,the carrier of a2,the carrier of a3:] st b7 = [b1,b3,b5] & b8 = [b2,b4,b6] holds
a4 . b7,b8 = ((dist b1,b2) + (dist b3,b4)) + (dist b5,b6);
existence
ex b1 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3:],[:the carrier of c1,the carrier of c2,the carrier of c3:]:], REAL st
for b2, b3 being Element of c1
for b4, b5 being Element of c2
for b6, b7 being Element of c3
for b8, b9 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = ((dist b2,b3) + (dist b4,b5)) + (dist b6,b7)
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3:],[:the carrier of c1,the carrier of c2,the carrier of c3:]:], REAL st ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b1 . b9,b10 = ((dist b3,b4) + (dist b5,b6)) + (dist b7,b8) ) & ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b2 . b9,b10 = ((dist b3,b4) + (dist b5,b6)) + (dist b7,b8) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist_cart3 METRIC_3:def 4 :
for b1, b2, b3 being non empty MetrSpace
for b4 being Function of [:[:the carrier of b1,the carrier of b2,the carrier of b3:],[:the carrier of b1,the carrier of b2,the carrier of b3:]:], REAL holds
( b4 = dist_cart3 b1,b2,b3 iff for b5, b6 being Element of b1
for b7, b8 being Element of b2
for b9, b10 being Element of b3
for b11, b12 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] st b11 = [b5,b7,b9] & b12 = [b6,b8,b10] holds
b4 . b11,b12 = ((dist b5,b6) + (dist b7,b8)) + (dist b9,b10) );

theorem Th8: :: METRIC_3:8
canceled;

theorem Th9: :: METRIC_3:9
canceled;

theorem Th10: :: METRIC_3:10
canceled;

theorem Th11: :: METRIC_3:11
canceled;

theorem Th12: :: METRIC_3:12
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds
( (dist_cart3 b1,b2,b3) . b4,b5 = 0 iff b4 = b5 )
proof end;

theorem Th13: :: METRIC_3:13
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds (dist_cart3 b1,b2,b3) . b4,b5 = (dist_cart3 b1,b2,b3) . b5,b4
proof end;

theorem Th14: :: METRIC_3:14
for b1, b2, b3 being non empty MetrSpace
for b4, b5, b6 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds (dist_cart3 b1,b2,b3) . b4,b6 <= ((dist_cart3 b1,b2,b3) . b4,b5) + ((dist_cart3 b1,b2,b3) . b5,b6)
proof end;

definition
let c1, c2, c3 be non empty MetrSpace;
func MetrSpaceCart3 c1,c2,c3 -> non empty strict MetrSpace equals :: METRIC_3:def 5
 MetrStruct(# [:the carrier of a1,the carrier of a2,the carrier of a3:],(dist_cart3 a1,a2,a3) #);
coherence
MetrStruct(# [:the carrier of c1,the carrier of c2,the carrier of c3:],(dist_cart3 c1,c2,c3) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def5 defines MetrSpaceCart3 METRIC_3:def 5 :
for b1, b2, b3 being non empty MetrSpace holds MetrSpaceCart3 b1,b2,b3 = MetrStruct(# [:the carrier of b1,the carrier of b2,the carrier of b3:],(dist_cart3 b1,b2,b3) #);

definition
let c1, c2, c3 be non empty MetrSpace;
let c4, c5 be Element of [:the carrier of c1,the carrier of c2,the carrier of c3:];
func dist3 c4,c5 -> Real equals :: METRIC_3:def 6
(dist_cart3 a1,a2,a3) . a4,a5;
coherence
(dist_cart3 c1,c2,c3) . c4,c5 is Real ;
end;

:: deftheorem Def6 defines dist3 METRIC_3:def 6 :
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds dist3 b4,b5 = (dist_cart3 b1,b2,b3) . b4,b5;

scheme :: METRIC_3:sch 3
s3{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> non empty set , F6( set , set , set , set , set , set , set , set ) -> Element of F5() } :
ex b1 being Function of [:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5() st
for b2, b3 being Element of F1()
for b4, b5 being Element of F2()
for b6, b7 being Element of F3()
for b8, b9 being Element of F4()
for b10, b11 being Element of [:F1(),F2(),F3(),F4():] st b10 = [b2,b4,b6,b8] & b11 = [b3,b5,b7,b9] holds
b1 . [b10,b11] = F6(b2,b3,b4,b5,b6,b7,b8,b9)
proof end;

definition
let c1, c2, c3, c4 be non empty MetrSpace;
func dist_cart4 c1,c2,c3,c4 -> Function of [:[:the carrier of a1,the carrier of a2,the carrier of a3,the carrier of a4:],[:the carrier of a1,the carrier of a2,the carrier of a3,the carrier of a4:]:], REAL means :Def7: :: METRIC_3:def 7
for b1, b2 being Element of a1
for b3, b4 being Element of a2
for b5, b6 being Element of a3
for b7, b8 being Element of a4
for b9, b10 being Element of [:the carrier of a1,the carrier of a2,the carrier of a3,the carrier of a4:] st b9 = [b1,b3,b5,b7] & b10 = [b2,b4,b6,b8] holds
a5 . b9,b10 = ((dist b1,b2) + (dist b3,b4)) + ((dist b5,b6) + (dist b7,b8));
existence
ex b1 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:],[:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:]:], REAL st
for b2, b3 being Element of c1
for b4, b5 being Element of c2
for b6, b7 being Element of c3
for b8, b9 being Element of c4
for b10, b11 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:] st b10 = [b2,b4,b6,b8] & b11 = [b3,b5,b7,b9] holds
b1 . b10,b11 = ((dist b2,b3) + (dist b4,b5)) + ((dist b6,b7) + (dist b8,b9))
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:],[:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:]:], REAL st ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of c4
for b11, b12 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:] st b11 = [b3,b5,b7,b9] & b12 = [b4,b6,b8,b10] holds
b1 . b11,b12 = ((dist b3,b4) + (dist b5,b6)) + ((dist b7,b8) + (dist b9,b10)) ) & ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of c4
for b11, b12 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:] st b11 = [b3,b5,b7,b9] & b12 = [b4,b6,b8,b10] holds
b2 . b11,b12 = ((dist b3,b4) + (dist b5,b6)) + ((dist b7,b8) + (dist b9,b10)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines dist_cart4 METRIC_3:def 7 :
for b1, b2, b3, b4 being non empty MetrSpace
for b5 being Function of [:[:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:],[:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:]:], REAL holds
( b5 = dist_cart4 b1,b2,b3,b4 iff for b6, b7 being Element of b1
for b8, b9 being Element of b2
for b10, b11 being Element of b3
for b12, b13 being Element of b4
for b14, b15 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:] st b14 = [b6,b8,b10,b12] & b15 = [b7,b9,b11,b13] holds
b5 . b14,b15 = ((dist b6,b7) + (dist b8,b9)) + ((dist b10,b11) + (dist b12,b13)) );

theorem Th15: :: METRIC_3:15
canceled;

theorem Th16: :: METRIC_3:16
canceled;

theorem Th17: :: METRIC_3:17
canceled;

theorem Th18: :: METRIC_3:18
canceled;

theorem Th19: :: METRIC_3:19
for b1, b2, b3, b4 being non empty MetrSpace
for b5, b6 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:] holds
( (dist_cart4 b1,b2,b3,b4) . b5,b6 = 0 iff b5 = b6 )
proof end;

theorem Th20: :: METRIC_3:20
for b1, b2, b3, b4 being non empty MetrSpace
for b5, b6 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:] holds (dist_cart4 b1,b2,b3,b4) . b5,b6 = (dist_cart4 b1,b2,b3,b4) . b6,b5
proof end;

theorem Th21: :: METRIC_3:21
for b1, b2, b3, b4 being non empty MetrSpace
for b5, b6, b7 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:] holds (dist_cart4 b1,b2,b3,b4) . b5,b7 <= ((dist_cart4 b1,b2,b3,b4) . b5,b6) + ((dist_cart4 b1,b2,b3,b4) . b6,b7)
proof end;

definition
let c1, c2, c3, c4 be non empty MetrSpace;
func MetrSpaceCart4 c1,c2,c3,c4 -> non empty strict MetrSpace equals :: METRIC_3:def 8
 MetrStruct(# [:the carrier of a1,the carrier of a2,the carrier of a3,the carrier of a4:],(dist_cart4 a1,a2,a3,a4) #);
coherence
MetrStruct(# [:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:],(dist_cart4 c1,c2,c3,c4) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def8 defines MetrSpaceCart4 METRIC_3:def 8 :
for b1, b2, b3, b4 being non empty MetrSpace holds MetrSpaceCart4 b1,b2,b3,b4 = MetrStruct(# [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:],(dist_cart4 b1,b2,b3,b4) #);

definition
let c1, c2, c3, c4 be non empty MetrSpace;
let c5, c6 be Element of [:the carrier of c1,the carrier of c2,the carrier of c3,the carrier of c4:];
func dist4 c5,c6 -> Real equals :: METRIC_3:def 9
(dist_cart4 a1,a2,a3,a4) . a5,a6;
coherence
(dist_cart4 c1,c2,c3,c4) . c5,c6 is Real ;
end;

:: deftheorem Def9 defines dist4 METRIC_3:def 9 :
for b1, b2, b3, b4 being non empty MetrSpace
for b5, b6 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3,the carrier of b4:] holds dist4 b5,b6 = (dist_cart4 b1,b2,b3,b4) . b5,b6;