let u be non zero Element of (TOP-REAL 3); for O being Matrix of 3,REAL
for P being Element of (ProjectiveSpace (TOP-REAL 3))
for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let O be Matrix of 3,REAL; for P being Element of (ProjectiveSpace (TOP-REAL 3))
for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let P be Element of (ProjectiveSpace (TOP-REAL 3)); for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let p be FinSequence of REAL ; ( O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p implies ( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 ) )
assume A1:
( O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p )
; ( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
hereby ( SumAll (QuadraticForm (p,O,p)) = 0 implies P in absolute )
assume
P in absolute
;
SumAll (QuadraticForm (p,O,p)) = 0 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 }
by PASCAL:def 2;
then consider Q being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A2:
P = Q
and A3:
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)
= 0
;
consider u1 being
Element of
(TOP-REAL 3) such that A4:
not
u1 is
zero
and A5:
Q = Dir u1
by ANPROJ_1:26;
reconsider p1 =
u1 as
FinSequence of
REAL by EUCLID:24;
A6:
SumAll (QuadraticForm (p1,O,p1)) =
qfconic (1,1,
(- 1),
(2 * 0),
(2 * 0),
(2 * 0),
u1)
by A1, PASCAL:13
.=
0
by A3, A4, A5
;
are_Prop u1,
u
by A2, A5, A1, A4, ANPROJ_1:22;
then consider a being
Real such that A7:
a <> 0
and A8:
u1 = a * u
by ANPROJ_1:1;
reconsider fa =
a as
Element of
F_Real by XREAL_0:def 1;
u is
Element of
REAL 3
by EUCLID:22;
then
len p = 3
by A1, EUCLID_8:50;
then
SumAll (QuadraticForm (p1,O,p1)) = (fa * fa) * (SumAll (QuadraticForm (p,O,p)))
by A1, A8, Th35;
hence
SumAll (QuadraticForm (p,O,p)) = 0
by A7, A6;
verum
end;
assume
SumAll (QuadraticForm (p,O,p)) = 0
; P in absolute
then 0 =
qfconic (1,1,(- 1),(2 * 0),(2 * 0),(2 * 0),u)
by A1, PASCAL:13
.=
qfconic (1,1,(- 1),0,0,0,u)
;
then
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
by A1, PASCAL:10;
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 in absolute
by PASCAL:def 2; verum