let P be Element of absolute ; :: thesis: ex Q being Element of absolute st P <> Q
P in conic (1,1,(- 1),0,0,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
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) = 0 ;
consider u being Element of (TOP-REAL 3) such that
A3: not u is zero and
A4: Dir u = P by ANPROJ_1:26;
A5: qfconic (1,1,(- 1),0,0,0,u) = 0 by A1, A2, A3, A4;
A6: u . 3 <> 0 by A3, A4, Th67;
not |[(u . 1),(u . 2),(- (u . 3))]| is zero
proof
assume |[(u . 1),(u . 2),(- (u . 3))]| is zero ; :: thesis: contradiction
then u . 3 = 0 by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A3, A4, Th67; :: thesis: verum
end;
then reconsider v = |[(u . 1),(u . 2),(- (u . 3))]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir v as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
take R ; :: thesis: ( R is Element of absolute & P <> R )
A7: R <> P
proof
assume R = P ; :: thesis: contradiction
then are_Prop v,u by A3, A4, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A8: v = a * u by ANPROJ_1:1;
A9: - (u . 3) = v `3 by EUCLID_5:2
.= (a * u) . 3 by A8, EUCLID_5:def 3
.= a * (u . 3) by RVSUM_1:44 ;
(a + 1) * (u . 3) = 0 by A9;
then a + 1 = 0 by A6;
then A10: a = - 1 ;
A11: u . 1 = v `1 by EUCLID_5:2
.= (a * u) . 1 by A8, EUCLID_5:def 1
.= a * (u . 1) by RVSUM_1:44 ;
A12: u . 2 = v `2 by EUCLID_5:2
.= (a * u) . 2 by A8, EUCLID_5:def 2
.= a * (u . 2) by RVSUM_1:44 ;
0 = ((((((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 A5, PASCAL:def 1
.= (- 1) * ((u . 3) ^2) by A11, A10, A12 ;
hence contradiction by A6; :: thesis: verum
end;
for w being Element of (TOP-REAL 3) st not w is zero & R = Dir w holds
qfconic (1,1,(- 1),0,0,0,w) = 0
proof
let w be Element of (TOP-REAL 3); :: thesis: ( not w is zero & R = Dir w implies qfconic (1,1,(- 1),0,0,0,w) = 0 )
assume that
A13: not w is zero and
A14: R = Dir w ; :: thesis: qfconic (1,1,(- 1),0,0,0,w) = 0
are_Prop v,w by A13, A14, ANPROJ_1:22;
then consider b being Real such that
b <> 0 and
A15: w = b * v by ANPROJ_1:1;
A16: w . 1 = b * (v . 1) by A15, RVSUM_1:44
.= b * (v `1) by EUCLID_5:def 1
.= b * (u . 1) by EUCLID_5:2 ;
A17: w . 2 = b * (v . 2) by A15, RVSUM_1:44
.= b * (v `2) by EUCLID_5:def 2
.= b * (u . 2) by EUCLID_5:2 ;
A18: w . 3 = b * (v . 3) by A15, RVSUM_1:44
.= b * (v `3) by EUCLID_5:def 3
.= b * (- (u . 3)) by EUCLID_5:2 ;
qfconic (1,1,(- 1),0,0,0,w) = ((((((1 * (w . 1)) * (w . 1)) + ((1 * (w . 2)) * (w . 2))) + (((- 1) * (w . 3)) * (w . 3))) + ((0 * (w . 1)) * (w . 2))) + ((0 * (w . 1)) * (w . 3))) + ((0 * (w . 2)) * (w . 3)) by PASCAL:def 1
.= (b * b) * (((((((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 A16, A17, A18
.= (b * b) * (qfconic (1,1,(- 1),0,0,0,u)) by PASCAL:def 1
.= 0 by A5 ;
hence qfconic (1,1,(- 1),0,0,0,w) = 0 ; :: thesis: verum
end;
then R 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 ( R is Element of absolute & P <> R ) by A7, PASCAL:def 2; :: thesis: verum