P in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative }
;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A1:
P = Q
and
A2:
for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative
;
consider u being Element of (TOP-REAL 3) such that
A3:
not u is zero
and
A4:
P = Dir u
by ANPROJ_1:26;
reconsider u1 = u . 1, u2 = u . 2, u3 = u . 3 as Real ;
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 . 2))) + ((0 * (u . 2)) * (u . 3))
by PASCAL:def 1
.=
(((u . 1) ^2) + ((u . 2) ^2)) - ((u . 3) ^2)
;
then
((u1 ^2) + (u2 ^2)) - (u3 ^2) < 0
by A1, A3, A4, A2;
then A5:
(((u1 ^2) + (u2 ^2)) - (u3 ^2)) + (u3 ^2) < 0 + (u3 ^2)
by XREAL_1:6;
A6:
u . 3 <> 0
proof
assume A7:
u . 3
= 0
;
contradiction
A8:
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 . 2))) + ((0 * (u . 2)) * (u . 3))
by PASCAL:def 1
.=
(u1 ^2) + (u2 ^2)
by A7
;
0 ^2 = 0
;
then
(
0 <= u1 ^2 &
0 <= u2 ^2 )
by SQUARE_1:12;
hence
contradiction
by A1, A3, A4, A2, A8;
verum
end;
reconsider k = 1 / (u3 ^2) as Real ;
0 < u3 ^2
by A6, SQUARE_1:12;
then A10:
((u1 ^2) + (u2 ^2)) * k < (u3 ^2) * k
by A5, XREAL_1:68;
A11:
( (u1 ^2) * k = (u1 / u3) ^2 & (u2 ^2) * k = (u2 / u3) ^2 )
by BKMODEL1:12;
|[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| <> 0. (TOP-REAL 3)
then
not |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| is zero
;
then reconsider v = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| as non zero Element of (TOP-REAL 3) ;
A12: v . 1 =
v `1
by EUCLID_5:def 1
.=
(u . 1) / (u . 3)
by EUCLID_5:2
;
A13: v . 2 =
v `2
by EUCLID_5:def 2
.=
(u . 2) / (u . 3)
by EUCLID_5:2
;
A14:
( (u . 3) * ((u . 1) / (u . 3)) = u . 1 & (u . 3) * ((u . 2) / (u . 3)) = u . 2 )
by A6, 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 `1),(u . 2),(u . 3)]|
by A14, EUCLID_5:def 1
.=
|[(u `1),(u `2),(u . 3)]|
by EUCLID_5:def 2
.=
|[(u `1),(u `2),(u `3)]|
by EUCLID_5:def 3
.=
u
by EUCLID_5:3
;
then
are_Prop v,u
by A6, ANPROJ_1:1;
then A15:
P = Dir v
by A3, A4, ANPROJ_1:22;
|[(v . 1),(v . 2)]| in inside_of_circle (0,0,1)
proof
reconsider t =
|[(v . 1),(v . 2)]| as
Element of
(TOP-REAL 2) ;
|.(t - |[0,0]|).| < 1
proof
A16:
|.(t - |[0,0]|).| =
|.|[((v . 1) - 0),((v . 2) - 0)]|.|
by EUCLID:62
.=
|.t.|
;
A17:
(
v . 1
= t `1 &
v . 2
= t `2 )
by EUCLID:52;
|.t.| ^2 = ((u1 ^2) * k) + ((u2 ^2) * k)
by A17, JGRAPH_1:29, A12, A13, A11;
then
|.t.| ^2 < 1
^2
by A10, A6, XCMPLX_1:106;
hence
|.(t - |[0,0]|).| < 1
by A16, SQUARE_1:48;
verum
end;
hence
|[(v . 1),(v . 2)]| in inside_of_circle (
0,
0,1)
;
verum
end;
then reconsider w = |[(v . 1),(v . 2)]| as Element of inside_of_circle (0,0,1) ;
take
w
; ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & w = |[(u . 1),(u . 2)]| )
v . 3 =
v `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
hence
ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & w = |[(u . 1),(u . 2)]| )
by A15; verum