let P be Element of BK_model ; :: thesis: for Q being Element of (ProjectiveSpace (TOP-REAL 3))
for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
let Q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
let v be non zero Element of (TOP-REAL 3); :: thesis: ( P <> Q & Q = Dir v & v . 3 = 1 implies ex P1 being Element of absolute st P,Q,P1 are_collinear )
assume that
A1: P <> Q and
A2: Q = Dir v and
A3: v . 3 = 1 ; :: thesis: ex P1 being Element of absolute st P,Q,P1 are_collinear
consider u being non zero Element of (TOP-REAL 3) such that
A4: ( Dir u = P & u . 3 = 1 & BK_to_REAL2 P = |[(u . 1),(u . 2)]| ) by Def01;
reconsider s = |[(u . 1),(u . 2)]|, t = |[(v . 1),(v . 2)]| as Point of (TOP-REAL 2) ;
set a = 0 ;
set b = 0 ;
set r = 1;
reconsider S = s, T = t, X = |[0,0]| as Element of REAL 2 by EUCLID:22;
reconsider w1 = ((- (2 * |((t - s),(s - |[0,0]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[0,0]|))|),((Sum (sqr (S - X))) - (1 ^2)))))) / (2 * (Sum (sqr (T - S)))) as Real ;
A5: s <> t

proof

assume s = t ; :: thesis: contradiction
then ( u . 1 = v . 1 & u . 2 = v . 2 ) by FINSEQ_1:77;
then ( u `1 = v . 1 & u `2 = v . 2 & u `3 = v . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3, A4, A3;
then A6: ( u `1 = v `1 & u `2 = v `2 & u `3 = v `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u = |[(u `1),(u `2),(u `3)]| by EUCLID_5:3
.= v by A6, EUCLID_5:3 ;
hence contradiction by A4, A1, A2; :: thesis: verum

end;

consider e1 being Point of (TOP-REAL 2) such that
A7: ( {e1} = (halfline (s,t)) /\ (circle (0,0,1)) & e1 = ((1 - w1) * s) + (w1 * t) ) by A5, A4, TOPREAL9:58;
reconsider f = |[(e1 `1),(e1 `2),1]| as Element of (TOP-REAL 3) ;
not f is zero by FINSEQ_1:78, EUCLID_5:4;
then reconsider ee1 = f as non zero Element of (TOP-REAL 3) ;
A8: ( s . 1 = u . 1 & s . 2 = u . 2 & t . 1 = v . 1 & t . 2 = v . 2 ) ;
reconsider P1 = Dir ee1 as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
((1 * ee1) + ((- (1 - w1)) * u)) + ((- w1) * v) = 0. (TOP-REAL 3)

proof

A9: 1 * ee1 = |[(1 * (ee1 `1)),(1 * (ee1 `2)),(1 * (ee1 `3))]| by EUCLID_5:7
.= ee1 by EUCLID_5:3 ;
ee1 = ((1 - w1) * u) + (w1 * v)

proof

A10: ((1 - w1) * s) + (w1 * t) = |[((((1 - w1) * s) + (w1 * t)) `1),((((1 - w1) * s) + (w1 * t)) `2)]| by EUCLID:53;
((1 - w1) * s) + (w1 * t) = |[((((1 - w1) * s) `1) + ((w1 * t) `1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:55
.= |[((((1 - w1) * s) . 1) + ((w1 * t) `1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:def 9
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:def 9
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) `2))]| by EUCLID:def 10
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by EUCLID:def 10
.= |[(((1 - w1) * (s . 1)) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (s . 1)) + (w1 * (t . 1))),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (s . 1)) + (w1 * (t . 1))),(((1 - w1) * (s . 2)) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2)))]| by A8, RVSUM_1:44 ;
then A11: ( e1 `1 = ((1 - w1) * (u . 1)) + (w1 * (v . 1)) & e1 `2 = ((1 - w1) * (u . 2)) + (w1 * (v . 2)) ) by A7, A10, FINSEQ_1:77;
((1 - w1) * u) + (w1 * v) = |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2))),(((1 - w1) * (u . 3)) + (w1 * (v . 3)))]|

proof

((1 - w1) * u) `1 = (1 - w1) * (u `1) by EUCLID_5:9
.= (1 - w1) * (u . 1) by EUCLID_5:def 1 ;
then A12: (((1 - w1) * u) `1) + ((w1 * v) `1) = ((1 - w1) * (u . 1)) + ((w1 * v) . 1) by EUCLID_5:def 1
.= ((1 - w1) * (u . 1)) + (w1 * (v . 1)) by RVSUM_1:44 ;
((1 - w1) * u) `2 = (1 - w1) * (u `2) by EUCLID_5:9
.= (1 - w1) * (u . 2) by EUCLID_5:def 2 ;
then A13: (((1 - w1) * u) `2) + ((w1 * v) `2) = ((1 - w1) * (u . 2)) + ((w1 * v) . 2) by EUCLID_5:def 2
.= ((1 - w1) * (u . 2)) + (w1 * (v . 2)) by RVSUM_1:44 ;
((1 - w1) * u) `3 = (1 - w1) * (u `3) by EUCLID_5:9
.= (1 - w1) * (u . 3) by EUCLID_5:def 3 ;
then (((1 - w1) * u) `3) + ((w1 * v) `3) = ((1 - w1) * (u . 3)) + ((w1 * v) . 3) by EUCLID_5:def 3
.= ((1 - w1) * (u . 3)) + (w1 * (v . 3)) by RVSUM_1:44 ;
hence ((1 - w1) * u) + (w1 * v) = |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2))),(((1 - w1) * (u . 3)) + (w1 * (v . 3)))]| by A12, A13, EUCLID_5:5; :: thesis: verum

end;

hence ee1 = ((1 - w1) * u) + (w1 * v) by A11, A4, A3; :: thesis: verum

end;

then (ee1 + ((- (1 - w1)) * u)) + ((- w1) * v) = (((1 - w1) * u) + (w1 * v)) + (((- (1 - w1)) * u) + ((- w1) * v)) by RVSUM_1:15
.= ((1 - w1) * u) + ((w1 * v) + (((- (1 - w1)) * u) + ((- w1) * v))) by RVSUM_1:15
.= ((1 - w1) * u) + (((- (1 - w1)) * u) + ((w1 * v) + ((- w1) * v))) by RVSUM_1:15
.= (((1 - w1) * u) + ((- (1 - w1)) * u)) + ((w1 * v) + ((- w1) * v)) by RVSUM_1:15
.= (0. (TOP-REAL 3)) + ((w1 * v) + ((- w1) * v)) by BKMODEL1:4
.= (0. (TOP-REAL 3)) + (0. (TOP-REAL 3)) by BKMODEL1:4
.= |[(0 + 0),(0 + 0),(0 + 0)]| by EUCLID_5:4, EUCLID_5:6
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence ((1 * ee1) + ((- (1 - w1)) * u)) + ((- w1) * v) = 0. (TOP-REAL 3) by A9; :: thesis: verum

end;

then A14: P1,P,Q are_collinear by A4, A2, ANPROJ_8:11;
e1 in {e1} by TARSKI:def 1;
then A15: e1 in circle (0,0,1) by A7, XBOOLE_0:def 4;

now :: thesis: ( |[(ee1 . 1),(ee1 . 2)]| in circle (0,0,1) & ee1 . 3 = 1 )

thus |[(ee1 . 1),(ee1 . 2)]| in circle (0,0,1) by A15, EUCLID:53; :: thesis: ee1 . 3 = 1
thus ee1 . 3 = 1 ; :: thesis: verum

end;

then P1 is Element of absolute by BKMODEL1:86;
hence ex P1 being Element of absolute st P,Q,P1 are_collinear by A14, COLLSP:8; :: thesis: verum