let P be Element of BK_model ; 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)); 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); ( 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
; 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
;
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;
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) ;
( |[(s `1),(s `2)]| = |[(u . 1),(u . 2)]| & |[(t `1),(t `2)]| = |[(v . 1),(v . 2)]| )
by EUCLID:53;
then
( s `1 = u . 1 & s `2 = u . 2 & t `1 = v . 1 & t `2 = v . 2 )
by FINSEQ_1:77;
then A8:
( s . 1 = u . 1 & s . 2 = u . 2 & t . 1 = v . 1 & t . 2 = v . 2 )
by EUCLID:def 9, EUCLID:def 10;
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)))]|
hence
ee1 = ((1 - w1) * u) + (w1 * v)
by A11, A4, A3;
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;
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;
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; verum