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:28
.= (p3 `1 ) - (p2 `1 ) by Lm15 ;
A4: Im c2 = (p3 - p2) `2 by A2, COMPLEX1:28
.= (p3 `2 ) - (p2 `2 ) by Lm15 ;
A5: Im c1 = (p1 - p2) `2 by A1, COMPLEX1:28
.= (p1 `2 ) - (p2 `2 ) by Lm15 ;
A6: Re c1 = (p1 - p2) `1 by A1, COMPLEX1:28
.= (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:48; :: 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:49; :: 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:28
.= sqrt ((((p1 - p2) `1 ) ^2 ) + (((p1 - p2) `2 ) ^2 )) by A1, COMPLEX1:28
.= 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:31; :: thesis: verum