let P, PP1, PP2 be Element of real_projective_plane; for P1, P2 being Element of absolute
for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )
let P1, P2 be Element of absolute ; for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )
let Q be Element of real_projective_plane; ( P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 implies ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear ) )
assume that
A1:
P1 <> P2
and
A2:
PP1 = P1
and
A3:
PP2 = P2
and
A4:
P in BK_model
and
A5:
P,PP1,PP2 are_collinear
and
A6:
Q in tangent P1
and
A7:
Q in tangent P2
; ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )
A8:
P <> Q
consider u being Element of (TOP-REAL 3) such that
A9:
not u is zero
and
A10:
Dir u = Q
by ANPROJ_1:26;
per cases
( u `3 <> 0 or u `3 = 0 )
;
suppose A11:
u `3 <> 0
;
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )reconsider v =
|[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non
zero Element of
(TOP-REAL 3) by BKMODEL1:41;
A12:
v . 3 =
v `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
A13:
(
(u `3) * ((u `1) / (u `3)) = u `1 &
(u `3) * ((u `2) / (u `3)) = u `2 )
by A11, XCMPLX_1:87;
(u `3) * v =
|[((u `3) * ((u `1) / (u `3))),((u `3) * ((u `2) / (u `3))),((u `3) * 1)]|
by EUCLID_5:8
.=
u
by A13, EUCLID_5:3
;
then
are_Prop v,
u
by A11, ANPROJ_1:1;
then A14:
(
Dir v = Q &
v . 3
= 1 )
by A10, A12, A9, ANPROJ_1:22;
reconsider PP =
P as
Element of
BK_model by A4;
reconsider QQ =
Q as
Element of
(ProjectiveSpace (TOP-REAL 3)) ;
consider R being
Element of
absolute such that A15:
PP,
QQ,
R are_collinear
by A8, A14, Th03;
reconsider R =
R as
Element of
real_projective_plane ;
take
R
;
( R in absolute & P,Q,R are_collinear )thus
(
R in absolute &
P,
Q,
R are_collinear )
by A15;
verum end; suppose
u `3 = 0
;
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )then A16:
u . 3
= 0
by EUCLID_5:def 3;
then
(
Q = pole_infty P1 &
Q = pole_infty P2 )
by A6, A7, A9, A10, Th28;
then consider up being non
zero Element of
(TOP-REAL 3) such that A17:
P1 = Dir up
and A18:
P2 = Dir |[(- (up `1)),(- (up `2)),1]|
and A19:
up `3 = 1
by A1, Th20;
consider up1 being non
zero Element of
(TOP-REAL 3) such that A20:
((up1 . 1) ^2) + ((up1 . 2) ^2) = 1
and A21:
up1 . 3
= 1
and A22:
P1 = Dir up1
by BKMODEL1:89;
up . 3
= 1
by A19, EUCLID_5:def 3;
then A23:
up = up1
by A17, A21, A22, BKMODEL1:43;
reconsider PP =
P as
Element of
BK_model by A4;
consider w being non
zero Element of
(TOP-REAL 3) such that A24:
Dir w = PP
and A25:
w . 3
= 1
and
BK_to_REAL2 PP = |[(w . 1),(w . 2)]|
by Def01;
reconsider up2 =
|[(- (up `1)),(- (up `2)),1]| as non
zero Element of
(TOP-REAL 3) by BKMODEL1:41;
A26:
up2 . 1 =
up2 `1
by EUCLID_5:def 1
.=
- (up `1)
by EUCLID_5:2
;
A27:
up2 . 2 =
up2 `2
by EUCLID_5:def 2
.=
- (up `2)
by EUCLID_5:2
;
A28:
up2 . 3 =
up2 `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
(
P1 is
Element of
absolute &
P2 is
Element of
absolute &
PP is
Element of
BK_model & not
up1 is
zero & not
up2 is
zero & not
w is
zero &
P1 = Dir up1 &
P2 = Dir up2 &
PP = Dir w &
up1 . 3
= 1 &
up2 . 3
= 1 &
w . 3
= 1 &
up2 . 1
= - (up1 . 1) &
up2 . 2
= - (up1 . 2) &
P1,
PP,
P2 are_collinear )
by A22, A18, A24, A21, A28, A25, A23, A26, A27, A2, A3, A5, COLLSP:4, EUCLID_5:def 1, EUCLID_5:def 2;
then consider a being
Real such that A29:
(
- 1
< a &
a < 1 )
and A30:
(
w . 1
= a * (up1 . 1) &
w . 2
= a * (up1 . 2) )
by Th18;
consider d,
e,
f being
Real such that A31:
e = ((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2)))
and A32:
f = ((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1))
and A33:
(e ^2) + (f ^2) = d ^2
by A29, A20, BKMODEL1:16;
d <> 0
by A20, A31, A32, A33;
then
not
|[e,f,d]| is
zero
by FINSEQ_1:78, EUCLID_5:4;
then reconsider ur =
|[e,f,d]| as non
zero Element of
(TOP-REAL 3) ;
reconsider S =
Dir ur as
Element of
real_projective_plane by ANPROJ_1:26;
take
S
;
( S in absolute & P,Q,S are_collinear )A35:
qfconic (1,1,
(- 1),
0,
0,
0,
ur)
= 0
proof
A36:
ur . 1 =
ur `1
by EUCLID_5:def 1
.=
e
by EUCLID_5:2
;
A37:
ur . 2 =
ur `2
by EUCLID_5:def 2
.=
f
by EUCLID_5:2
;
A38:
ur . 3 =
ur `3
by EUCLID_5:def 3
.=
d
by EUCLID_5:2
;
qfconic (1,1,
(- 1),
0,
0,
0,
ur) =
((((((1 * (ur . 1)) * (ur . 1)) + ((1 * (ur . 2)) * (ur . 2))) + (((- 1) * (ur . 3)) * (ur . 3))) + ((0 * (ur . 1)) * (ur . 2))) + ((0 * (ur . 1)) * (ur . 3))) + ((0 * (ur . 2)) * (ur . 3))
by PASCAL:def 1
.=
((e ^2) + (f ^2)) - (d ^2)
by A36, A37, A38
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
ur)
= 0
by A33;
verum
end;
|{w,u,ur}| = 0
proof
consider u9 being non
zero Element of
(TOP-REAL 3) such that A39:
(
P1 = Dir u9 &
u9 . 3
= 1 &
((u9 . 1) ^2) + ((u9 . 2) ^2) = 1 &
pole_infty P1 = Dir |[(- (u9 . 2)),(u9 . 1),0]| )
by Def03;
up . 3
= 1
by A19, EUCLID_5:def 3;
then A40:
u9 = up
by A39, A17, BKMODEL1:43;
A41:
Q = Dir |[(- (up . 2)),(up . 1),0]|
by A39, A40, A16, A6, A9, A10, Th28;
not
|[(- (up . 2)),(up . 1),0]| is
zero
then
are_Prop u,
|[(- (up . 2)),(up . 1),0]|
by A41, A10, A9, ANPROJ_1:22;
then consider g being
Real such that
g <> 0
and A42:
u = g * |[(- (up . 2)),(up . 1),0]|
by ANPROJ_1:1;
|[(u `1),(u `2),(u `3)]| =
u
by EUCLID_5:3
.=
|[(g * (- (up . 2))),(g * (up . 1)),(g * 0)]|
by A42, EUCLID_5:8
;
then A43:
(
u `1 = g * (- (up . 2)) &
u `2 = g * (up . 1) &
u `3 = g * 0 )
by FINSEQ_1:78;
A44:
w `3 = 1
by A25, EUCLID_5:def 3;
A45:
(
w `1 = a * (up1 . 1) &
w `2 = a * (up1 . 2) )
by A30, EUCLID_5:def 1, EUCLID_5:def 2;
(
ur `1 = e &
ur `2 = f &
ur `3 = d )
by EUCLID_5:2;
then |{w,u,ur}| =
(((((((a * (up1 . 1)) * (g * (up . 1))) * d) - ((1 * (g * (up . 1))) * (((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2)))))) - (((a * (up1 . 1)) * 0) * (((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1))))) + (((a * (up1 . 2)) * 0) * (((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2)))))) - (((a * (up1 . 2)) * (g * (- (up . 2)))) * d)) + ((1 * (g * (- (up . 2)))) * (((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1))))
by A43, A44, A45, A31, A32, ANPROJ_8:27
.=
0
by A23
;
hence
|{w,u,ur}| = 0
;
verum
end; hence
(
S in absolute &
P,
Q,
S are_collinear )
by A35, PASCAL:11, A9, A24, A10, BKMODEL1:1;
verum end;