let u be non zero Element of (TOP-REAL 3); for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) holds
P is Element of absolute
let P be Point of (ProjectiveSpace (TOP-REAL 3)); ( P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) implies P is Element of absolute )
assume that
A1:
P = Dir u
and
A2:
u . 3 = 1
and
A3:
|[(u . 1),(u . 2)]| in circle (0,0,1)
; P is Element of absolute
reconsider u1 = u . 1, u2 = u . 2, u3 = u . 3 as Real ;
A4: (u1 ^2) + (u2 ^2) =
|.|[(u1 - 0),(u2 - 0)]|.| ^2
by TOPGEN_5:9
.=
|.(|[u1,u2]| - |[0,0]|).| ^2
by EUCLID:62
.=
1 ^2
by A3, TOPREAL9:43
.=
1
;
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) = 0 let v be
Element of
(TOP-REAL 3);
( not v is zero & P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) = 0 )assume that A5:
not
v is
zero
and A6:
P = Dir v
;
qfconic (1,1,(- 1),0,0,0,v) = 0
are_Prop u,
v
by A1, A5, A6, ANPROJ_1:22;
then consider a being
Real such that A7:
a <> 0
and A8:
u = a * v
by ANPROJ_1:1;
reconsider v1 =
v . 1,
v2 =
v . 2,
v3 =
v . 3 as
Real ;
(
u1 = a * v1 &
u2 = a * v2 &
u3 = a * v3 )
by A8, RVSUM_1:44;
then A9:
(
v1 = u1 / a &
v2 = u2 / a &
v3 = u3 / a )
by A7, XCMPLX_1:89;
qfconic (1,1,
(- 1),
0,
0,
0,
v) =
((((((1 * v1) * v1) + ((1 * v2) * v2)) + (((- 1) * v3) * v3)) + ((0 * v1) * v2)) + ((0 * v1) * v3)) + ((0 * v2) * v3)
by PASCAL:def 1
.=
(((u1 / a) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))
by A9
.=
((((1 / a) * u1) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))
by XCMPLX_1:99
.=
((((1 / a) * u1) * ((1 / a) * u1)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))
by XCMPLX_1:99
.=
(((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * (u2 / a))) - ((u3 / a) * (u3 / a))
by XCMPLX_1:99
.=
(((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * ((1 / a) * u2))) - ((u3 / a) * (u3 / a))
by XCMPLX_1:99
.=
(((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * (u3 / a))
by XCMPLX_1:99
.=
(((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * ((1 / a) * u3))
by XCMPLX_1:99
.=
((1 / a) * (1 / a)) * (((u1 ^2) + (u2 * u2)) - (u3 * u3))
.=
0
by A2, A4
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
v)
= 0
;
verum end;
then
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) = 0 }
;
hence
P is Element of absolute
by PASCAL:def 2; verum