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;

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

suppose A14: fr2 = 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

then fr1 <> 0 by A10, EUCLID_5:4, A1;
then A15: ( fp1 = 0 & fq1 = 0 ) by A14, A13, A11, A12;
then ( ( fp2 = 1 or fp2 = - 1 ) & ( fq2 = 1 or fq2 = - 1 ) ) by SQUARE_1:41, A9, A3;
hence ( u . 1 = - (v . 1) & u . 2 = - (v . 2) ) by A1, A2, A15, A10; :: thesis: verum

end;

suppose A16: fr2 <> 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

( fq1 * ((fr1 * fp1) + (fr2 * fp2)) = 0 & fp1 * ((fr1 * fq1) + (fr2 * fq2)) = 0 ) by A13, A11, A12;
then fr2 * ((fq1 * fp2) - (fp1 * fq2)) = 0 ;
then A17: (fq1 * fp2) - (fp1 * fq2) = 0 by A16;

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

suppose A18: fp2 = 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

then ( fp1 = 0 or fq2 = 0 ) by A17;
then ( ( fq1 = 1 or fq1 = - 1 ) & ( fp1 = 1 or fp1 = - 1 ) ) by SQUARE_1:41, A3, A9, A18;
hence ( u . 1 = - (v . 1) & u . 2 = - (v . 2) ) by A1, A2, A10, A17; :: thesis: verum

end;

suppose A20: fp2 <> 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

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

suppose fp1 = 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

hence ( u . 1 = - (v . 1) & u . 2 = - (v . 2) ) by A9, A11, A16, A20; :: thesis: verum

end;

suppose A21: fp1 <> 0 ; :: thesis: ( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

reconsider l = fq1 / fp1 as Real ;
A22: l = fq2 / fp2

proof

fq1 = fq1 * (fp2 / fp2) by XCMPLX_1:88, A20
.= (fp1 * fq2) / fp2 by A17, XCMPLX_1:74
.= fp1 * (fq2 / fp2) by XCMPLX_1:74 ;
hence l = fq2 / fp2 by A21, XCMPLX_1:89; :: thesis: verum

end;

then A23: ( fq1 = l * fp1 & fq2 = l * fp2 ) by A21, A20, XCMPLX_1:87;
( v . 1 = l * fp1 & v . 2 = l * fp2 ) by A22, A9, A21, A20, XCMPLX_1:87;
then ( l = 1 or l = - 1 ) by A9, A3, BKMODEL1:3;
hence ( u . 1 = - (v . 1) & u . 2 = - (v . 2) ) by A1, A2, A10, A23; :: thesis: verum

end;

end;

end;

end;

end;

end;