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;

per cases ( fr1 = 0 or fr1 <> 0 ) ;

suppose A14: fr1 = 0 ; :: thesis: R = pole_infty P

then A15: fr2 <> 0 by A12, EUCLID_5:4, A3;
then A16: fp2 = 0 by A14, A11, A13;
A17: w . 1 = v . 1 by A4, A5, BKMODEL1:43
.= fp1 by EUCLID_5:def 1 ;
A18: w . 2 = v . 2 by A4, A5, BKMODEL1:43
.= 0 by A15, A14, A11, A13 ;

now :: thesis: ( not |[0,fp1,0]| is zero & are_Prop u,|[0,fp1,0]| )

A19: fp1 <> 0 by A5, A16, A11;
thus not |[0,fp1,0]| is zero by A5, A16, A11, FINSEQ_1:78, EUCLID_5:4; :: thesis: are_Prop u,|[0,fp1,0]|
thus are_Prop u,|[0,fp1,0]| :: thesis: verum

proof

u = |[((fr2 / fp1) * 0),((fr2 / fp1) * fp1),((fr2 / fp1) * 0)]| by A16, A11, A5, XCMPLX_1:87, A12, A14
.= (fr2 / fp1) * |[0,fp1,0]| by EUCLID_5:8 ;
hence are_Prop u,|[0,fp1,0]| by A15, A19, ANPROJ_1:1; :: thesis: verum

end;

end;

hence R = pole_infty P by A2, ANPROJ_1:22, A4, A17, A18; :: thesis: verum

end;

suppose A20: fr1 <> 0 ; :: thesis: R = pole_infty P

A21: fp2 <> 0

proof

assume A22: fp2 = 0 ; :: thesis: contradiction
then fp1 = 0 by A13, A11, A20;
hence contradiction by A22, A11, A5; :: thesis: verum

end;

then A23: fr2 = (fp1 * (- fr1)) / fp2 by A13, A11, XCMPLX_1:89
.= fp1 * ((- fr1) / fp2) by XCMPLX_1:74 ;
reconsider l = (- fr1) / fp2 as non zero Real by A20, A21;

A24: now :: thesis: ( not |[(- fp2),fp1,0]| is zero & are_Prop u,|[(- fp2),fp1,0]| )

thus not |[(- fp2),fp1,0]| is zero by A21, FINSEQ_1:78, EUCLID_5:4; :: thesis: are_Prop u,|[(- fp2),fp1,0]|
fr1 = - (- fr1)
.= - (l * fp2) by A21, XCMPLX_1:87 ;
then fr = |[(l * (- fp2)),(l * fp1),(l * 0)]| by A23, A12, A3
.= l * |[(- fp2),fp1,0]| by EUCLID_5:8 ;
hence are_Prop u,|[(- fp2),fp1,0]| by ANPROJ_1:1; :: thesis: verum

end;

w = v by BKMODEL1:43, A4, A5;
hence R = pole_infty P by A24, A2, ANPROJ_1:22, A4, A11; :: thesis: verum

end;

end;