set TP = TarskiEuclid2Space ;
let a, b, c, x, a1, b1, c1, x1 be POINT of TarskiEuclid2Space; GTARSKI1:def 9 ( a = b or not a,b,c cong a1,b1,c1 or not between a,b,x or not between a1,b1,x1 or not b,x equiv b1,x1 or c,x equiv c1,x1 )
assume that
A1:
a <> b
and
A2:
a,b,c cong a1,b1,c1
and
A3:
between a,b,x
and
A4:
between a1,b1,x1
and
A5:
b,x equiv b1,x1
; c,x equiv c1,x1
A6:
( dist (a,b) = dist (a1,b1) & dist (a,c) = dist (a1,c1) & dist (b,c) = dist (b1,c1) )
by A2, GTARSKI1:def 15;
A7:
dist (a,x) = (dist (a,b)) + (dist (b,x))
by A3, ThConv8;
A8:
dist (a1,x1) = (dist (a1,b1)) + (dist (b1,x1))
by A4, ThConv8;
A9:
dist (b,x) = dist (b1,x1)
by A5, GTARSKI1:def 15;
A10:
(dist (c1,x1)) ^2 = (((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1)))))
by ThLawOfCosines;
(dist (c,x)) ^2 = (dist (c1,x1)) ^2
proof
per cases
( x = b or c = b or ( x <> b & c <> b ) )
;
suppose
x = b
;
(dist (c,x)) ^2 = (dist (c1,x1)) ^2 then A11:
0 = dist (
x,
b)
by ThEgal;
then A12:
dist (
x1,
b1)
= 0
by A5, GTARSKI1:def 15;
A12bis:
(dist (c,x)) ^2 =
((0 ^2) + ((dist (c,b)) ^2)) - (((2 * 0) * (dist (c,b))) * (cos (angle ((Tn2TR x),(Tn2TR b),(Tn2TR c)))))
by A11, ThLawOfCosines
.=
(0 * 0) + ((dist (c,b)) ^2)
by SQUARE_1:def 1
;
(dist (c1,x1)) ^2 =
((0 ^2) + ((dist (c1,b1)) ^2)) - (((2 * 0) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1)))))
by ThLawOfCosines, A12
.=
(0 * 0) + ((dist (c1,b1)) ^2)
by SQUARE_1:def 1
;
hence
(dist (c,x)) ^2 = (dist (c1,x1)) ^2
by A12bis, A2, GTARSKI1:def 15;
verum end; suppose A13:
c = b
;
(dist (c,x)) ^2 = (dist (c1,x1)) ^2 then
0 = dist (
c,
b)
by ThEgal;
then
dist (
c1,
b1)
= 0
by A2, GTARSKI1:def 15;
then
(dist (c1,x1)) ^2 = (0 * 0) + ((dist (x1,b1)) ^2)
by A10, SQUARE_1:def 1;
hence
(dist (c,x)) ^2 = (dist (c1,x1)) ^2
by A13, A5, GTARSKI1:def 15;
verum end; suppose A14:
(
x <> b &
c <> b )
;
(dist (c,x)) ^2 = (dist (c1,x1)) ^2 A15:
a <> x
(
dist (
a,
b)
<> 0 &
dist (
a,
x)
<> 0 &
dist (
b,
x)
<> 0 )
by A1, A14, A15, ThEgal;
then A16:
(
Tn2TR a1 <> Tn2TR b1 &
Tn2TR a1 <> Tn2TR x1 &
Tn2TR b1 <> Tn2TR x1 )
by ThEgal, A6, A7, A8, A9;
Tn2TR b in LSeg (
(Tn2TR a),
(Tn2TR x))
by A3, ThConv6;
then
(
(angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) + (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x))) = PI or
(angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) + (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x))) = 3
* PI )
by A1, A14, EUCLID_6:13;
then
(
cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = cos (PI - (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x)))) or
cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = cos ((3 * PI) - (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x)))) )
;
then A17:
cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = - (cos (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x))))
by Th2, EUCLID10:2;
Tn2TR b1 in LSeg (
(Tn2TR a1),
(Tn2TR x1))
by A4, ThConv6;
then
(
(angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) + (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1))) = PI or
(angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) + (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1))) = 3
* PI )
by A16, EUCLID_6:13;
then
(
cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = cos (PI - (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1)))) or
cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = cos ((3 * PI) - (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1)))) )
;
then A18:
cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = - (cos (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1))))
by Th2, EUCLID10:2;
A19:
(
dist (
a,
b)
<> 0 &
dist (
c,
b)
<> 0 )
by A1, A14, ThEgal;
A20:
(dist (c,a)) ^2 = (((dist (a,b)) ^2) + ((dist (c,b)) ^2)) - (((2 * (dist (a,b))) * (dist (c,b))) * (cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c)))))
by ThLawOfCosines;
A21:
(
dist (
a1,
b1)
<> 0 &
dist (
c1,
b1)
<> 0 )
by A1, A6, A14, ThEgal;
(dist (c1,a1)) ^2 = (((dist (a1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (a1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1)))))
by ThLawOfCosines;
then A22:
cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) =
((((dist (c,a)) ^2) - ((dist (a,b)) ^2)) - ((dist (c,b)) ^2)) / (- ((2 * (dist (a,b))) * (dist (c,b))))
by A6, Th1, A21
.=
cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c)))
by A20, A19, Th1
;
(dist (c,x)) ^2 =
(((dist (x,b)) ^2) + ((dist (c,b)) ^2)) - (((2 * (dist (x,b))) * (dist (c,b))) * (cos (angle ((Tn2TR x),(Tn2TR b),(Tn2TR c)))))
by ThLawOfCosines
.=
(((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (- (cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))))))
by A17, EUCLID_6:3, A6, A9, A22
.=
(((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1)))))
by A18, EUCLID_6:3
.=
(dist (c1,x1)) ^2
by ThLawOfCosines
;
hence
(dist (c,x)) ^2 = (dist (c1,x1)) ^2
;
verum end; end;
end;
hence
c,x equiv c1,x1
by ThConv9; verum