let P be Element of BK_model ; for Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
let Q be Element of (ProjectiveSpace (TOP-REAL 3)); ( P <> Q implies ex P1 being Element of absolute st P,Q,P1 are_collinear )
assume
P <> Q
; ex P1 being Element of absolute st P,Q,P1 are_collinear
then
Line (P,Q) is LINE of real_projective_plane
by COLLSP:def 7;
then reconsider L = Line (P,Q) as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
consider R being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A1:
P <> R
and
A2:
R in L
and
A3:
for u being non zero Element of (TOP-REAL 3) st R = Dir u holds
u . 3 <> 0
by COLLSP:10, Th10;
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;
consider v9 being Element of (TOP-REAL 3) such that
A5:
not v9 is zero
and
A6:
Dir v9 = R
by ANPROJ_1:26;
A7:
v9 . 3 <> 0
by A5, A6, A3;
then A8:
v9 `3 <> 0
by EUCLID_5:def 3;
then reconsider k = 1 / (v9 `3) as non zero Real ;
not k * v9 is zero
then reconsider v = k * v9 as non zero Element of (TOP-REAL 3) ;
A9:
( Dir v = R & v . 3 = 1 )
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 ;
s <> t
proof
assume
s = t
;
contradiction
then
(
u . 1
= v . 1 &
u . 2
= v . 2 &
u . 3
= v . 3 )
by A4, A9, 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;
then A11:
(
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 A11, EUCLID_5:3
;
hence
contradiction
by A4, A9, A1;
verum
end;
then consider e1 being Point of (TOP-REAL 2) such that
A12:
( {e1} = (halfline (s,t)) /\ (circle (0,0,1)) & e1 = ((1 - w1) * s) + (w1 * t) )
by A4, TOPREAL9:58;
reconsider w2 = ((- (2 * |((s - t),(t - |[0,0]|))|)) + (sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),(t - |[0,0]|))|),((Sum (sqr (T - X))) - (1 ^2)))))) / (2 * (Sum (sqr (S - T)))) as Real ;
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 A13:
( 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
A14: 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
A15:
((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 A13, RVSUM_1:44
;
then A16:
(
e1 `1 = ((1 - w1) * (u . 1)) + (w1 * (v . 1)) &
e1 `2 = ((1 - w1) * (u . 2)) + (w1 * (v . 2)) )
by A12, A15, 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 A16, A4, A9;
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,0,0]| + |[0,0,0]|
by BKMODEL1:4, EUCLID_5:4
.=
|[(0 + 0),(0 + 0),(0 + 0)]|
by EUCLID_5:6
.=
0. (TOP-REAL 3)
by EUCLID_5:4
;
hence
((1 * ee1) + ((- (1 - w1)) * u)) + ((- w1) * v) = 0. (TOP-REAL 3)
by A14;
verum
end;
then A19:
P1,P,R are_collinear
by A4, A9, ANPROJ_8:11;
e1 in {e1}
by TARSKI:def 1;
then A20:
e1 in circle (0,0,1)
by A12, XBOOLE_0:def 4;
then A22:
P1 is Element of absolute
by BKMODEL1:86;
A23:
P,R,P1 are_collinear
by COLLSP:8, A19;
P,Q,R are_collinear
by A2, COLLSP:11;
then
P,R,Q are_collinear
by ANPROJ_8:57, HESSENBE:1;
hence
ex P1 being Element of absolute st P,Q,P1 are_collinear
by A22, A23, A1, HESSENBE:2, ANPROJ_8:57; verum