Dir101 in conic (1,1,(- 1),0,0,0)
proof
Dir101 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 }
proof
now for u being Element of (TOP-REAL 3) st not u is zero & Dir101 = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 let u be
Element of
(TOP-REAL 3);
( not u is zero & Dir101 = Dir u implies qfconic (1,1,(- 1),0,0,0,u) = 0 )assume A1:
( not
u is
zero &
Dir101 = Dir u )
;
qfconic (1,1,(- 1),0,0,0,u) = 0
not
|[1,0,1]| is
zero
by EUCLID_5:4, FINSEQ_1:78;
then
are_Prop u,
|[1,0,1]|
by A1, ANPROJ_1:22;
then consider a being
Real such that
a <> 0
and A2:
u = a * |[1,0,1]|
by ANPROJ_1:1;
u =
|[(a * 1),(a * 0),(a * 1)]|
by A2, EUCLID_5:8
.=
|[a,0,a]|
;
then
(
u `1 = a &
u `2 = 0 &
u `3 = a )
by EUCLID_5:2;
then A3:
(
u . 1
= a &
u . 2
= 0 &
u . 3
= a )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
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
.=
0
by A3
;
verum end;
hence
Dir101 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 }
;
verum
end;
hence
Dir101 in conic (1,1,
(- 1),
0,
0,
0)
by PASCAL:def 2;
verum
end;
hence
conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3))
; verum