let P be Point of (ProjectiveSpace (TOP-REAL 3)); ( not P in BK_model \/ absolute implies ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute ) )
assume A1:
not P in BK_model \/ absolute
; ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )
then A2:
( not P in BK_model & not P in absolute )
by XBOOLE_0:def 3;
consider u9 being Element of (TOP-REAL 3) such that
A3:
not u9 is zero
and
A4:
P = Dir u9
by ANPROJ_1:26;
per cases
( u9 . 3 = 0 or u9 . 3 <> 0 )
;
suppose A5:
u9 . 3
= 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )
(
u9 . 1
<> 0 or
u9 . 2
<> 0 )
proof
assume A6:
(
u9 . 1
= 0 &
u9 . 2
= 0 )
;
contradiction
u9 =
|[(u9 `1),(u9 `2),(u9 `3)]|
by EUCLID_5:3
.=
|[0,(u9 `2),(u9 `3)]|
by A6, EUCLID_5:def 1
.=
|[0,0,(u9 `3)]|
by A6, EUCLID_5:def 2
.=
0. (TOP-REAL 3)
by A5, EUCLID_5:def 3, EUCLID_5:4
;
hence
contradiction
by A3;
verum
end; per cases then
( u9 . 1 <> 0 or u9 . 2 <> 0 )
;
suppose A7:
u9 . 1
<> 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )then reconsider v =
|[(- (u9 . 2)),(u9 . 1),0]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir v as
Point of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
P <> Q
proof
assume
P = Q
;
contradiction
then
are_Prop u9,
v
by A3, A4, ANPROJ_1:22;
then consider a being
Real such that
a <> 0
and A9:
u9 = a * v
by ANPROJ_1:1;
A10:
|[(a * (- (u9 . 2))),(a * (u9 . 1)),(a * 0)]| =
a * v
by EUCLID_5:8
.=
|[(u9 `1),(u9 `2),(u9 `3)]|
by A9, EUCLID_5:3
;
now ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )end;
then
(
u9 . 1
= 0 &
u9 . 2
= 0 )
by Th10;
then
(
u9 `1 = 0 &
u9 `2 = 0 &
u9 `3 = 0 )
by A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence
contradiction
by A3, EUCLID_5:3, EUCLID_5:4;
verum
end; then reconsider l9 =
Line (
P,
Q) as
LINE of
real_projective_plane by COLLSP:def 7;
reconsider l =
l9 as
Element of the
Lines of
(IncProjSp_of real_projective_plane) by INCPROJ:4;
take
l
;
( P in l & l misses absolute )
l misses absolute
proof
assume
not
l misses absolute
;
contradiction
then consider R being
object such that A11:
R in l /\ absolute
by XBOOLE_0:7;
A12:
(
R in l &
R in absolute )
by A11, XBOOLE_0:def 4;
reconsider R =
R as
Element of
(ProjectiveSpace (TOP-REAL 3)) by A11;
consider w being non
zero Element of
(TOP-REAL 3) such that A13:
w . 3
= 1
and A14:
R = Dir w
by A12, Th25;
reconsider R9 =
R as
POINT of
(IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 =
l as
LINE of
(IncProjSp_of real_projective_plane) ;
A15:
w `3 = 1
by A13, EUCLID_5:def 3;
A16:
u9 `3 = 0
by A5, EUCLID_5:def 3;
A17:
v `1 =
- (u9 . 2)
by EUCLID_5:2
.=
- (u9 `2)
by EUCLID_5:def 2
;
A18:
v `2 =
u9 . 1
by EUCLID_5:2
.=
u9 `1
by EUCLID_5:def 1
;
A19:
v `3 = 0
by EUCLID_5:2;
R9 on l2
by A12, INCPROJ:5;
then
|{u9,v,w}| = 0
by A3, A4, A14, BKMODEL1:77;
then 0 =
(((((((u9 `1) * (v `2)) * 1) - (((u9 `3) * (v `2)) * (w `1))) - (((u9 `1) * (v `3)) * (w `2))) + (((u9 `2) * (v `3)) * (w `1))) - (((u9 `2) * (v `1)) * 1)) + (((u9 `3) * (v `1)) * (w `2))
by A15, ANPROJ_8:27
.=
((u9 `1) ^2) + ((u9 `2) ^2)
by A16, A17, A18, A19
;
then
(
u9 `1 = 0 &
u9 `2 = 0 )
;
hence
contradiction
by A7, EUCLID_5:def 1;
verum
end; hence
(
P in l &
l misses absolute )
by COLLSP:10;
verum end; suppose A20:
u9 . 2
<> 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )then reconsider v =
|[(- (u9 . 2)),(u9 . 1),0]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir v as
Point of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
P <> Q
proof
assume
P = Q
;
contradiction
then
are_Prop u9,
v
by A3, A4, ANPROJ_1:22;
then consider a being
Real such that
a <> 0
and A22:
u9 = a * v
by ANPROJ_1:1;
A23:
|[(a * (- (u9 . 2))),(a * (u9 . 1)),(a * 0)]| =
a * v
by EUCLID_5:8
.=
|[(u9 `1),(u9 `2),(u9 `3)]|
by A22, EUCLID_5:3
;
now ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )end;
then
(
u9 . 1
= 0 &
u9 . 2
= 0 )
by Th10;
then
(
u9 `1 = 0 &
u9 `2 = 0 &
u9 `3 = 0 )
by A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence
contradiction
by A3, EUCLID_5:3, EUCLID_5:4;
verum
end; then reconsider l9 =
Line (
P,
Q) as
LINE of
real_projective_plane by COLLSP:def 7;
reconsider l =
l9 as
Element of the
Lines of
(IncProjSp_of real_projective_plane) by INCPROJ:4;
take
l
;
( P in l & l misses absolute )
l misses absolute
proof
assume
not
l misses absolute
;
contradiction
then consider R being
object such that A24:
R in l /\ absolute
by XBOOLE_0:7;
A25:
(
R in l &
R in absolute )
by A24, XBOOLE_0:def 4;
reconsider R =
R as
Element of
(ProjectiveSpace (TOP-REAL 3)) by A24;
consider w being non
zero Element of
(TOP-REAL 3) such that A26:
w . 3
= 1
and A27:
R = Dir w
by A25, Th25;
reconsider R9 =
R as
POINT of
(IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 =
l as
LINE of
(IncProjSp_of real_projective_plane) ;
A28:
w `3 = 1
by A26, EUCLID_5:def 3;
A29:
u9 `3 = 0
by A5, EUCLID_5:def 3;
A30:
v `1 =
- (u9 . 2)
by EUCLID_5:2
.=
- (u9 `2)
by EUCLID_5:def 2
;
A31:
v `2 =
u9 . 1
by EUCLID_5:2
.=
u9 `1
by EUCLID_5:def 1
;
A32:
v `3 = 0
by EUCLID_5:2;
R9 on l2
by A25, INCPROJ:5;
then
|{u9,v,w}| = 0
by A3, A4, A27, BKMODEL1:77;
then 0 =
(((((((u9 `1) * (v `2)) * 1) - (((u9 `3) * (v `2)) * (w `1))) - (((u9 `1) * (v `3)) * (w `2))) + (((u9 `2) * (v `3)) * (w `1))) - (((u9 `2) * (v `1)) * 1)) + (((u9 `3) * (v `1)) * (w `2))
by A28, ANPROJ_8:27
.=
((u9 `1) ^2) + ((u9 `2) ^2)
by A29, A30, A31, A32
;
then
(
u9 `1 = 0 &
u9 `2 = 0 )
;
hence
contradiction
by A20, EUCLID_5:def 2;
verum
end; hence
(
P in l &
l misses absolute )
by COLLSP:10;
verum end; suppose A33:
u9 . 3
<> 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )reconsider u =
|[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| as non
zero Element of
(TOP-REAL 3) ;
A34:
u `3 = 1
by EUCLID_5:2;
then A35:
u . 3
= 1
by EUCLID_5:def 3;
(u9 . 3) * u =
|[(u9 . 1),(u9 . 2),(u9 . 3)]|
by A33, Th22
.=
|[(u9 `1),(u9 . 2),(u9 . 3)]|
by EUCLID_5:def 1
.=
|[(u9 `1),(u9 `2),(u9 . 3)]|
by EUCLID_5:def 2
.=
|[(u9 `1),(u9 `2),(u9 `3)]|
by EUCLID_5:def 3
.=
u9
by EUCLID_5:3
;
then A36:
are_Prop u,
u9
by A33, ANPROJ_1:1;
then A37:
P = Dir u
by A3, A4, ANPROJ_1:22;
(
u . 1
<> 0 or
u . 2
<> 0 )
proof
assume A38:
(
u . 1
= 0 &
u . 2
= 0 )
;
contradiction
now for v being Element of (TOP-REAL 3) st not v is zero & P = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative let v be
Element of
(TOP-REAL 3);
( not v is zero & P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )assume A39:
not
v is
zero
;
( P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )assume
P = Dir v
;
qfconic (1,1,(- 1),0,0,0,v) is negative then A40:
Dir u = Dir v
by A36, A3, A4, ANPROJ_1:22;
now ( 0 < (u . 3) ^2 & qfconic (1,1,(- 1),0,0,0,u) = (- 1) * ((u . 3) ^2) )thus
0 < (u . 3) ^2
by A35;
qfconic (1,1,(- 1),0,0,0,u) = (- 1) * ((u . 3) ^2)thus qfconic (1,1,
(- 1),
0,
0,
0,
u) =
((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + (((- 1) * (u . 3)) * (u . 3))) + ((0 * (u . 1)) * (u . 2))) + ((0 * (u . 1)) * (u . 3))) + ((0 * (u . 2)) * (u . 3))
by PASCAL:def 1
.=
(- 1) * ((u . 3) ^2)
by A38
;
verum end; hence
qfconic (1,1,
(- 1),
0,
0,
0,
v) is
negative
by A39, A40, BKMODEL1:81;
verum end;
hence
contradiction
by A2, BKMODEL2:def 1;
verum
end; per cases then
( u . 1 <> 0 or u . 2 <> 0 )
;
suppose A41:
u . 1
<> 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )then reconsider u1 =
u . 1 as non
zero Real ;
reconsider u2 =
u . 2 as
Real ;
reconsider v =
|[(- u2),u1,0]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir v as
Element of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider l9 =
Line (
P,
Q) as
LINE of
real_projective_plane by Th26, A37, COLLSP:def 7;
reconsider l =
l9 as
Element of the
Lines of
(IncProjSp_of real_projective_plane) by INCPROJ:4;
take
l
;
( P in l & l misses absolute )
l misses absolute
proof
assume
not
l misses absolute
;
contradiction
then consider R being
object such that A42:
R in l /\ absolute
by XBOOLE_0:7;
A43:
(
R in l &
R in absolute )
by A42, XBOOLE_0:def 4;
reconsider R =
R as
Element of
(ProjectiveSpace (TOP-REAL 3)) by A42;
consider w being non
zero Element of
(TOP-REAL 3) such that A44:
w . 3
= 1
and A45:
R = Dir w
by A43, Th25;
|[(w . 1),(w . 2)]| in circle (
0,
0,1)
by A43, A44, A45, BKMODEL1:84;
then
((w . 1) ^2) + ((w . 2) ^2) = 1
by BKMODEL1:13;
then
((w `1) ^2) + ((w . 2) ^2) = 1
by EUCLID_5:def 1;
then A46:
((w `1) ^2) + ((w `2) ^2) = 1
by EUCLID_5:def 2;
now ( u `1 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
u `1 <> 0
by A41, EUCLID_5:def 1;
( u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
u `3 = 1
by EUCLID_5:2;
( v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `1 = - u2
by EUCLID_5:2;
hence
v `1 = - (u `2)
by EUCLID_5:def 2;
( v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `2 = u . 1
by EUCLID_5:2;
hence
v `2 = u `1
by EUCLID_5:def 1;
( v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
v `3 = 0
by EUCLID_5:2;
( w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
w `3 = 1
by A44, EUCLID_5:def 3;
( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )reconsider R9 =
R as
POINT of
(IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 =
l as
LINE of
(IncProjSp_of real_projective_plane) ;
R9 on l2
by A43, INCPROJ:5;
hence
|{u,v,w}| = 0
by A37, A45, BKMODEL1:77;
1 < ((u `1) ^2) + ((u `2) ^2)thus
1
< ((u `1) ^2) + ((u `2) ^2)
verum end;
hence
contradiction
by A46, Th23;
verum
end; hence
(
P in l &
l misses absolute )
by COLLSP:10;
verum end; suppose A47:
u . 2
<> 0
;
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )then reconsider u2 =
u . 2 as non
zero Real ;
reconsider u1 =
u . 1 as
Real ;
reconsider v =
|[(- u2),u1,0]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir v as
Element of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider l9 =
Line (
P,
Q) as
LINE of
real_projective_plane by A37, Th26, COLLSP:def 7;
reconsider l =
l9 as
Element of the
Lines of
(IncProjSp_of real_projective_plane) by INCPROJ:4;
take
l
;
( P in l & l misses absolute )
l misses absolute
proof
assume
l meets absolute
;
contradiction
then consider R being
object such that A48:
R in l /\ absolute
by XBOOLE_0:7;
A49:
(
R in l &
R in absolute )
by A48, XBOOLE_0:def 4;
reconsider R =
R as
Element of
(ProjectiveSpace (TOP-REAL 3)) by A48;
consider w being non
zero Element of
(TOP-REAL 3) such that A50:
w . 3
= 1
and A51:
R = Dir w
by A49, Th25;
|[(w . 1),(w . 2)]| in circle (
0,
0,1)
by A49, A50, A51, BKMODEL1:84;
then
((w . 1) ^2) + ((w . 2) ^2) = 1
by BKMODEL1:13;
then
((w `1) ^2) + ((w . 2) ^2) = 1
by EUCLID_5:def 1;
then A53:
((w `1) ^2) + ((w `2) ^2) = 1
by EUCLID_5:def 2;
now ( u `2 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
u `2 <> 0
by A47, EUCLID_5:def 2;
( u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
u `3 = 1
by EUCLID_5:2;
( v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `1 = - u2
by EUCLID_5:2;
hence
v `1 = - (u `2)
by EUCLID_5:def 2;
( v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `2 = u . 1
by EUCLID_5:2;
hence
v `2 = u `1
by EUCLID_5:def 1;
( v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
v `3 = 0
by EUCLID_5:2;
( w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )thus
w `3 = 1
by A50, EUCLID_5:def 3;
( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )reconsider R9 =
R as
POINT of
(IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 =
l as
LINE of
(IncProjSp_of real_projective_plane) ;
R9 on l2
by A49, INCPROJ:5;
hence
|{u,v,w}| = 0
by A37, A51, BKMODEL1:77;
1 < ((u `1) ^2) + ((u `2) ^2)thus
1
< ((u `1) ^2) + ((u `2) ^2)
verum end;
hence
contradiction
by A53, Th24;
verum
end; hence
(
P in l &
l misses absolute )
by COLLSP:10;
verum end; end;