let p, q, r, s be Point of (TOP-REAL 3); ( not p is zero & |(p,q)| = 0 & |(p,r)| = 0 & |(p,s)| = 0 implies |{q,r,s}| = 0 )
assume that
A1:
not p is zero
and
A2:
|(p,q)| = 0
and
A3:
|(p,r)| = 0
and
A4:
|(p,s)| = 0
; |{q,r,s}| = 0
A5:
(((p `1) * (q `1)) + ((p `2) * (q `2))) + ((p `3) * (q `3)) = 0
by A2, EUCLID_5:29;
A6:
(((p `1) * (r `1)) + ((p `2) * (r `2))) + ((p `3) * (r `3)) = 0
by A3, EUCLID_5:29;
A7:
(((p `1) * (s `1)) + ((p `2) * (s `2))) + ((p `3) * (s `3)) = 0
by A4, EUCLID_5:29;
per cases
( p `1 <> 0 or p `2 <> 0 or p `3 <> 0 )
by A1, EUCLID_5:3, EUCLID_5:4;
suppose A8:
p `1 <> 0
;
|{q,r,s}| = 0 set l2 =
(p `2) / (p `1);
set l3 =
(p `3) / (p `1);
A9:
q `1 = (- (((p `2) / (p `1)) * (q `2))) - (((p `3) / (p `1)) * (q `3))
by Th11, A8, A5;
A10:
r `1 = (- (((p `2) / (p `1)) * (r `2))) - (((p `3) / (p `1)) * (r `3))
by Th11, A8, A6;
A11:
s `1 = (- (((p `2) / (p `1)) * (s `2))) - (((p `3) / (p `1)) * (s `3))
by Th11, A8, A7;
|{q,r,s}| =
((((((((- (((p `2) / (p `1)) * (q `2))) - (((p `3) / (p `1)) * (q `3))) * (r `2)) * (s `3)) - (((q `3) * (r `2)) * ((- (((p `2) / (p `1)) * (s `2))) - (((p `3) / (p `1)) * (s `3))))) - ((((- (((p `2) / (p `1)) * (q `2))) - (((p `3) / (p `1)) * (q `3))) * (r `3)) * (s `2))) + (((q `2) * (r `3)) * ((- (((p `2) / (p `1)) * (s `2))) - (((p `3) / (p `1)) * (s `3))))) - (((q `2) * ((- (((p `2) / (p `1)) * (r `2))) - (((p `3) / (p `1)) * (r `3)))) * (s `3))) + (((q `3) * ((- (((p `2) / (p `1)) * (r `2))) - (((p `3) / (p `1)) * (r `3)))) * (s `2))
by A9, A10, A11, Th23
.=
0
;
hence
|{q,r,s}| = 0
;
verum end; suppose A12:
p `2 <> 0
;
|{q,r,s}| = 0 set l1 =
(p `1) / (p `2);
set l3 =
(p `3) / (p `2);
A13:
q `2 = (- (((p `1) / (p `2)) * (q `1))) - (((p `3) / (p `2)) * (q `3))
by Th11, A12, A5;
A14:
r `2 = (- (((p `1) / (p `2)) * (r `1))) - (((p `3) / (p `2)) * (r `3))
by Th11, A12, A6;
A15:
s `2 = (- (((p `1) / (p `2)) * (s `1))) - (((p `3) / (p `2)) * (s `3))
by Th11, A12, A7;
|{q,r,s}| =
(((((((q `1) * (r `2)) * (s `3)) - (((q `3) * (r `2)) * (s `1))) - (((q `1) * (r `3)) * (s `2))) + (((q `2) * (r `3)) * (s `1))) - (((q `2) * (r `1)) * (s `3))) + (((q `3) * (r `1)) * (s `2))
by Th23
.=
0
by A13, A14, A15
;
hence
|{q,r,s}| = 0
;
verum end; suppose A16:
p `3 <> 0
;
|{q,r,s}| = 0 set l1 =
(p `1) / (p `3);
set l2 =
(p `2) / (p `3);
(((p `3) * (q `3)) + ((p `1) * (q `1))) + ((p `2) * (q `2)) = 0
by A5;
then A17:
q `3 = (- (((p `1) / (p `3)) * (q `1))) - (((p `2) / (p `3)) * (q `2))
by Th11, A16;
(((p `3) * (r `3)) + ((p `1) * (r `1))) + ((p `2) * (r `2)) = 0
by A6;
then A18:
r `3 = (- (((p `1) / (p `3)) * (r `1))) - (((p `2) / (p `3)) * (r `2))
by Th11, A16;
(((p `1) * (s `1)) + ((p `2) * (s `2))) + ((p `3) * (s `3)) = 0
by A4, EUCLID_5:29;
then
(((p `3) * (s `3)) + ((p `1) * (s `1))) + ((p `2) * (s `2)) = 0
;
then A19:
s `3 = (- (((p `1) / (p `3)) * (s `1))) - (((p `2) / (p `3)) * (s `2))
by Th11, A16;
|{q,r,s}| =
(((((((q `1) * (r `2)) * (s `3)) - (((q `3) * (r `2)) * (s `1))) - (((q `1) * (r `3)) * (s `2))) + (((q `2) * (r `3)) * (s `1))) - (((q `2) * (r `1)) * (s `3))) + (((q `3) * (r `1)) * (s `2))
by Th23
.=
0
by A17, A18, A19
;
hence
|{q,r,s}| = 0
;
verum end;