let p, q be Point of (TOP-REAL 2); for r being Real st p `1 = q `2 & - (p `2) = q `1 & p = r * q holds
( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
let r be Real; ( p `1 = q `2 & - (p `2) = q `1 & p = r * q implies ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) ) )
A1:
1 + (r * r) > 0 + 0
by XREAL_1:8, XREAL_1:63;
assume
( p `1 = q `2 & - (p `2) = q `1 & p = r * q )
; ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
then A2:
p = |[(r * (- (p `2))),(r * (p `1))]|
by EUCLID:57;
then
p `2 = r * (p `1)
by EUCLID:52;
then p `1 =
- (r * (r * (p `1)))
by A2, EUCLID:52
.=
- ((r * r) * (p `1))
;
then
(1 + (r * r)) * (p `1) = 0
;
hence A3:
p `1 = 0
by A1, XCMPLX_1:6; ( p `2 = 0 & p = 0. (TOP-REAL 2) )
p `1 = r * (- (p `2))
by A2, EUCLID:52;
then
p `2 = - ((r * r) * (p `2))
by A2, EUCLID:52;
then
(1 + (r * r)) * (p `2) = 0
;
hence
p `2 = 0
by A1, XCMPLX_1:6; p = 0. (TOP-REAL 2)
hence
p = 0. (TOP-REAL 2)
by A3, EUCLID:53, EUCLID:54; verum