let P be Element of absolute ; :: thesis: for R being Element of real_projective_plane
for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds
R = pole_infty P
let R be Element of real_projective_plane; :: thesis: for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds
R = pole_infty P
let u be non zero Element of (TOP-REAL 3); :: thesis: ( R in tangent P & R = Dir u & u . 3 = 0 implies R = pole_infty P )
assume that
A1: R in tangent P and
A2: R = Dir u and
A3: u . 3 = 0 ; :: thesis: R = pole_infty P
consider w being non zero Element of (TOP-REAL 3) such that
A4: ( P = Dir w & w . 3 = 1 & ((w . 1) ^2) + ((w . 2) ^2) = 1 & pole_infty P = Dir |[(- (w . 2)),(w . 1),0]| ) by Def03;
consider v being non zero Element of (TOP-REAL 3) such that
A5: ( ((v . 1) ^2) + ((v . 2) ^2) = 1 & v . 3 = 1 & P = Dir v ) by BKMODEL1:89;
reconsider M = symmetric_3 (1,1,(- 1),0,0,0) as Matrix of 3,REAL ;
reconsider fp = v, fr = u as FinSequence of REAL by EUCLID:24;
reconsider fr1 = u `1 , fr2 = u `2 , fr3 = u `3 as Element of REAL by XREAL_0:def 1;
A6: fr = <*fr1,fr2,fr3*> by EUCLID_5:3;
A7: SumAll (QuadraticForm (fr,M,fp)) = 0 by A2, A1, A5, Th26;
( u is Element of REAL 3 & v is Element of REAL 3 ) by EUCLID:22;
then A8: ( len fp = 3 & len fr = 3 ) by EUCLID_8:50;
( len M = 3 & width M = 3 ) by MATRIX_0:24;
then A9: |(fr,(M * fp))| = 0 by A7, A8, MATRPROB:44;
reconsider m1 = 1, m2 = 0 , m3 = 0 , m4 = 0 , m5 = 1, m6 = 0 , m7 = 0 , m8 = 0 , m9 = - 1 as Element of REAL by XREAL_0:def 1;
A10: M = <*<*m1,m2,m3*>,<*m4,m5,m6*>,<*m7,m8,m9*>*> by PASCAL:def 3;
reconsider fp1 = v `1 , fp2 = v `2 , fp3 = v `3 as Element of REAL by XREAL_0:def 1;
A11: ( v . 1 = fp1 & v . 2 = fp2 & fp3 = 1 & fr3 = 0 ) by A3, A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A12: ( fp = <*fp1,fp2,fp3*> & fr = <*fr1,fr2,fr3*> ) by EUCLID_5:3;
then M * fp = <*(((1 * fp1) + (0 * fp2)) + (0 * fp3)),(((0 * fp1) + (1 * fp2)) + (0 * fp3)),(((0 * fp1) + (0 * fp2)) + ((- 1) * fp3))*> by A10, PASCAL:9
.= <*fp1,fp2,(- fp3)*> ;
then A13: ((fr1 * fp1) + (fr2 * fp2)) + (fr3 * (- fp3)) = 0 by A9, A6, EUCLID_5:30;