let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( |.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 ; :: thesis: |.(p1 - p2).| = |.c1.|
thus |.(p1 - p2).| = |.c1.| by A1, EUCLID_3:25; :: thesis: verum