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