let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( (p1 - p2) `1 = (p1 `1 ) - (p2 `1 ) & (p1 - p2) `2 = (p1 `2 ) - (p2 `2 ) )
A1: euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2) by EUCLID_3:19
.= (euc2cpx p1) + (- (euc2cpx p2))
.= (euc2cpx p1) + (euc2cpx (- p2)) by EUCLID_3:17 ;
- p2 is complex-valued Function ;
reconsider pp = p2 as Element of REAL 2 by EUCLID:25;
A2: (- p2) `1 = (- pp) . 1 by EUCLID:72
.= - (pp . 1) by VALUED_1:8
.= - (p2 `1 ) ;
A3: (- p2) `2 = (- pp) . 2 by EUCLID:72
.= - (pp . 2) by VALUED_1:8
.= - (p2 `2 ) ;
thus (p1 - p2) `1 = Re ((euc2cpx p1) + (euc2cpx (- p2))) by A1, COMPLEX1:28
.= (Re (euc2cpx p1)) + (Re (euc2cpx (- p2))) by COMPLEX1:19
.= (p1 `1 ) + (Re (euc2cpx (- p2))) by COMPLEX1:28
.= (p1 `1 ) + ((- p2) `1 ) by COMPLEX1:28
.= (p1 `1 ) - (p2 `1 ) by A2 ; :: thesis: (p1 - p2) `2 = (p1 `2 ) - (p2 `2 )
thus (p1 - p2) `2 = Im ((euc2cpx p1) + (euc2cpx (- p2))) by A1, COMPLEX1:28
.= (Im (euc2cpx p1)) + (Im (euc2cpx (- p2))) by COMPLEX1:19
.= (p1 `2 ) + (Im (euc2cpx (- p2))) by COMPLEX1:28
.= (p1 `2 ) + ((- p2) `2 ) by COMPLEX1:28
.= (p1 `2 ) - (p2 `2 ) by A3 ; :: thesis: verum