let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( (p1 - p2) `1 = (p1 `1) - (p2 `1) & (p1 - p2) `2 = (p1 `2) - (p2 `2) )
reconsider pp = p2 as Element of REAL 2 by EUCLID:22;
A1: (- p2) `1 = (- pp) . 1
.= - (pp . 1) by VALUED_1:8
.= - (p2 `1) ;
A2: euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2) by EUCLID_3:15
.= (euc2cpx p1) + (- (euc2cpx p2))
.= (euc2cpx p1) + (euc2cpx (- p2)) by EUCLID_3:13 ;
hence (p1 - p2) `1 = Re ((euc2cpx p1) + (euc2cpx (- p2))) by COMPLEX1:12
.= (Re (euc2cpx p1)) + (Re (euc2cpx (- p2))) by COMPLEX1:8
.= (p1 `1) + (Re (euc2cpx (- p2))) by COMPLEX1:12
.= (p1 `1) + ((- p2) `1) by COMPLEX1:12
.= (p1 `1) - (p2 `1) by A1 ;
:: thesis: (p1 - p2) `2 = (p1 `2) - (p2 `2)
A3: (- p2) `2 = (- pp) . 2
.= - (pp . 2) by VALUED_1:8
.= - (p2 `2) ;
thus (p1 - p2) `2 = Im ((euc2cpx p1) + (euc2cpx (- p2))) by A2, COMPLEX1:12
.= (Im (euc2cpx p1)) + (Im (euc2cpx (- p2))) by COMPLEX1:8
.= (p1 `2) + (Im (euc2cpx (- p2))) by COMPLEX1:12
.= (p1 `2) + ((- p2) `2) by COMPLEX1:12
.= (p1 `2) - (p2 `2) by A3 ; :: thesis: verum