let p1, p2, p3 be Point of (TOP-REAL 2); for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
( Re (c1 .|. c2) = (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2))) & Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1))) & |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| )
let c1, c2 be Element of COMPLEX ; ( c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) implies ( Re (c1 .|. c2) = (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2))) & Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1))) & |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| ) )
assume that
A1:
c1 = euc2cpx (p1 - p2)
and
A2:
c2 = euc2cpx (p3 - p2)
; ( Re (c1 .|. c2) = (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2))) & Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1))) & |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| )
A3: Re c2 =
(p3 - p2) `1
by A2, COMPLEX1:12
.=
(p3 `1) - (p2 `1)
by Lm15
;
A4: Im c2 =
(p3 - p2) `2
by A2, COMPLEX1:12
.=
(p3 `2) - (p2 `2)
by Lm15
;
A5: Im c1 =
(p1 - p2) `2
by A1, COMPLEX1:12
.=
(p1 `2) - (p2 `2)
by Lm15
;
A6: Re c1 =
(p1 - p2) `1
by A1, COMPLEX1:12
.=
(p1 `1) - (p2 `1)
by Lm15
;
hence
Re (c1 .|. c2) = (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2)))
by A3, A5, A4, EUCLID_3:39; ( Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1))) & |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| )
thus
Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1)))
by A6, A3, A5, A4, EUCLID_3:40; ( |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| )
thus |.c1.| =
sqrt ((((p1 - p2) `1) ^2) + ((Im c1) ^2))
by A1, COMPLEX1:12
.=
sqrt ((((p1 - p2) `1) ^2) + (((p1 - p2) `2) ^2))
by A1, COMPLEX1:12
.=
sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 - p2) `2) ^2))
by Lm15
.=
sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
by Lm15
; |.(p1 - p2).| = |.c1.|
thus
|.(p1 - p2).| = |.c1.|
by A1, EUCLID_3:25; verum