let P, Q, R be non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w `3 = 1 holds
( P,Q,R are_collinear iff u,v,w are_collinear )
let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w `3 = 1 implies ( P,Q,R are_collinear iff u,v,w are_collinear ) )
assume that
A1: ( P = Dir u & Q = Dir v & R = Dir w ) and
A2: ( u `3 = 1 & v `3 = 1 & w `3 = 1 ) ; :: thesis: ( P,Q,R are_collinear iff u,v,w are_collinear )
reconsider i = 3 as Nat ;

hereby :: thesis: ( u,v,w are_collinear implies P,Q,R are_collinear )

assume P,Q,R are_collinear ; :: thesis: u,v,w are_collinear
then consider u9, v9, w9 being Element of (TOP-REAL 3) such that
A3: ( P = Dir u9 & Q = Dir v9 & R = Dir w9 & not u9 is zero & not v9 is zero & not w9 is zero ) and
A4: ex a, b, c being Real st
( ((a * u9) + (b * v9)) + (c * w9) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) ) by ANPROJ_8:11;
A5: |{u9,v9,w9}| = 0 by A4, ANPROJ_8:41;
are_Prop u,u9 by A1, A3, ANPROJ_1:22;
then consider a being Real such that
A6: a <> 0 and
A7: u9 = a * u by ANPROJ_1:1;
are_Prop v,v9 by A1, A3, ANPROJ_1:22;
then consider b being Real such that
A8: b <> 0 and
A9: v9 = b * v by ANPROJ_1:1;
are_Prop w,w9 by A1, A3, ANPROJ_1:22;
then consider c being Real such that
A10: c <> 0 and
A11: w9 = c * w by ANPROJ_1:1;
reconsider d = a * (b * c) as non zero Real by A6, A8, A10;
0 = a * |{u,(b * v),(c * w)}| by ANPROJ_8:31, A5, A7, A9, A11
.= a * (b * |{u,v,(c * w)}|) by ANPROJ_8:32
.= a * (b * (c * |{u,v,w}|)) by ANPROJ_8:33
.= d * |{u,v,w}| ;
then |{u,v,w}| = 0 ;
then consider a, b, c being Real such that
A12: ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) and
A13: ( a <> 0 or b <> 0 or c <> 0 ) by ANPROJ_8:43, ANPROJ_1:def 2;
reconsider aubv = (a * u) + (b * v), cw = c * w, au = a * u, bv = b * v as Element of (TOP-REAL 3) ;
A14: cw is Element of REAL 3 by EUCLID:22;
A15: aubv is Element of REAL 3 by EUCLID:22;
( au is Element of REAL 3 & bv is Element of REAL 3 ) by EUCLID:22;
then A16: aubv . 3 = (au . 3) + (bv . 3) by RVSUM_1:11
.= (a * (u . 3)) + (bv . 3) by RVSUM_1:44
.= (a * (u . 3)) + (b * (v . 3)) by RVSUM_1:44 ;
A17: cw . 3 = c * (w . 3) by RVSUM_1:44;
|[((aubv + cw) `1),((aubv + cw) `2),((aubv + cw) `3)]| = |[0,0,0]| by A12, EUCLID_5:3, EUCLID_5:4;
then A18: 0 = (aubv + cw) `3 by FINSEQ_1:78
.= (aubv + cw) . 3 by EUCLID_5:def 3
.= (aubv . 3) + (cw . 3) by A14, A15, RVSUM_1:11
.= ((a * (u `3)) + (b * (v . 3))) + (c * (w . 3)) by A16, A17, EUCLID_5:def 3
.= ((a * (u `3)) + (b * (v `3))) + (c * (w . 3)) by EUCLID_5:def 3
.= ((a * (u `3)) + (b * (v `3))) + (c * (w `3)) by EUCLID_5:def 3
.= (a + b) + c by A2 ;
thus u,v,w are_collinear :: thesis: verum

proof

per cases ( a <> 0 or b <> 0 or c <> 0 ) by A13;

suppose A19: a <> 0 ; :: thesis: u,v,w are_collinear

reconsider L = Line (v,w) as line of (TOP-REAL 3) ;
( u in L & v in L & w in L ) by A18, A12, Th42, A19, RLTOPSP1:72;
hence u,v,w are_collinear by RLTOPSP1:def 16; :: thesis: verum

end;

suppose A20: b <> 0 ; :: thesis: u,v,w are_collinear

A21: ((b * v) + (c * w)) + (a * u) = 0. (TOP-REAL 3) by A12, RVSUM_1:15;
A22: (b + c) + a = 0 by A18;
reconsider L = Line (w,u) as line of (TOP-REAL 3) ;
( v in L & w in L & u in L ) by A22, A20, A21, Th42, RLTOPSP1:72;
hence u,v,w are_collinear by RLTOPSP1:def 16; :: thesis: verum

end;

suppose A23: c <> 0 ; :: thesis: u,v,w are_collinear

A24: ((c * w) + (a * u)) + (b * v) = 0. (TOP-REAL 3) by A12, RVSUM_1:15;
A25: (c + a) + b = 0 by A18;
reconsider L = Line (u,v) as line of (TOP-REAL 3) ;
( w in L & u in L & v in L ) by A25, A23, A24, Th42, RLTOPSP1:72;
hence u,v,w are_collinear by RLTOPSP1:def 16; :: thesis: verum

end;

end;

end;

end;

assume u,v,w are_collinear ; :: thesis: P,Q,R are_collinear

per cases then ( u in LSeg (v,w) or v in LSeg (w,u) or w in LSeg (u,v) ) by TOPREAL9:67;

suppose u in LSeg (v,w) ; :: thesis: P,Q,R are_collinear

then consider r being Real such that
( 0 <= r & r <= 1 ) and
A26: u = ((1 - r) * v) + (r * w) by RLTOPSP1:76;
reconsider a = 1, b = r - 1, c = - r as Real ;
((1 * u) + ((r - 1) * v)) + ((- r) * w) = 0. (TOP-REAL 3)

proof

reconsider vw = v + w as Element of REAL 3 by EUCLID:22;
1 * u = ((1 - r) * v) + (r * w) by A26, RVSUM_1:52;
then ((1 * u) + ((r - 1) * v)) + ((- r) * w) = ((r * w) + (((1 - r) * v) + ((r - 1) * v))) + ((- r) * w) by RVSUM_1:15
.= ((r * w) + (((1 - r) + (r - 1)) * v)) + ((- r) * w) by RVSUM_1:50
.= (0 * v) + ((r * w) + ((- r) * w)) by RVSUM_1:15
.= (0 * v) + ((r + (- r)) * w) by RVSUM_1:50
.= 0 * vw by RVSUM_1:51
.= i |-> 0 by RVSUM_1:53
.= 0. (TOP-REAL 3) by EUCLID_5:4, FINSEQ_2:62 ;
hence ((1 * u) + ((r - 1) * v)) + ((- r) * w) = 0. (TOP-REAL 3) ; :: thesis: verum

end;

hence P,Q,R are_collinear by A1, ANPROJ_8:11; :: thesis: verum

end;

suppose v in LSeg (w,u) ; :: thesis: P,Q,R are_collinear

then consider r being Real such that
( 0 <= r & r <= 1 ) and
A27: v = ((1 - r) * w) + (r * u) by RLTOPSP1:76;
reconsider a = - r, b = 1, c = r - 1 as Real ;
(((- r) * u) + (1 * v)) + ((r - 1) * w) = 0. (TOP-REAL 3)

proof

reconsider uw = u + w as Element of REAL 3 by EUCLID:22;
1 * v = ((1 - r) * w) + (r * u) by A27, RVSUM_1:52;
then (((- r) * u) + (1 * v)) + ((r - 1) * w) = ((((- r) * u) + (r * u)) + ((1 - r) * w)) + ((r - 1) * w) by RVSUM_1:15
.= ((((- r) + r) * u) + ((1 - r) * w)) + ((r - 1) * w) by RVSUM_1:50
.= (0 * u) + (((1 - r) * w) + ((r - 1) * w)) by RVSUM_1:15
.= (0 * u) + (((1 - r) + (r - 1)) * w) by RVSUM_1:50
.= 0 * uw by RVSUM_1:51
.= i |-> 0 by RVSUM_1:53
.= 0. (TOP-REAL 3) by FINSEQ_2:62, EUCLID_5:4 ;
hence (((- r) * u) + (1 * v)) + ((r - 1) * w) = 0. (TOP-REAL 3) ; :: thesis: verum

end;

hence P,Q,R are_collinear by A1, ANPROJ_8:11; :: thesis: verum

end;

suppose w in LSeg (u,v) ; :: thesis: P,Q,R are_collinear

then consider r being Real such that
( 0 <= r & r <= 1 ) and
A28: w = ((1 - r) * u) + (r * v) by RLTOPSP1:76;
reconsider a = r - 1, b = - r, c = 1 as Real ;
(((r - 1) * u) + ((- r) * v)) + (1 * w) = 0. (TOP-REAL 3)

proof

reconsider vu = v + u as Element of REAL 3 by EUCLID:22;
1 * w = ((1 - r) * u) + (r * v) by A28, RVSUM_1:52;
then (((r - 1) * u) + ((- r) * v)) + (1 * w) = ((r - 1) * u) + (((- r) * v) + ((r * v) + ((1 - r) * u))) by RVSUM_1:15
.= ((r - 1) * u) + ((((- r) * v) + (r * v)) + ((1 - r) * u)) by RVSUM_1:15
.= ((r - 1) * u) + ((((- r) + r) * v) + ((1 - r) * u)) by RVSUM_1:50
.= (0 * v) + (((r - 1) * u) + ((1 - r) * u)) by RVSUM_1:15
.= (0 * v) + (((r - 1) + (1 - r)) * u) by RVSUM_1:50
.= 0 * vu by RVSUM_1:51
.= i |-> 0 by RVSUM_1:53
.= 0. (TOP-REAL 3) by FINSEQ_2:62, EUCLID_5:4 ;
hence (((r - 1) * u) + ((- r) * v)) + (1 * w) = 0. (TOP-REAL 3) ; :: thesis: verum

end;

hence P,Q,R are_collinear by A1, ANPROJ_8:11; :: thesis: verum

end;

end;