let p, q be Point of real_projective_plane; :: thesis: ( p <> q implies ( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) ) )
assume A1: p <> q ; :: thesis: ( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) )
then consider u1, v1 being non zero Element of (TOP-REAL 3) such that
A2: p = Dir u1 and
A3: q = Dir v1 and
A4: L2P (p,q) = Dir (u1 <X> v1) by Def01;
consider u2, v2 being non zero Element of (TOP-REAL 3) such that
A5: q = Dir u2 and
A6: p = Dir v2 and
A7: L2P (q,p) = Dir (u2 <X> v2) by A1, Def01;
are_Prop u1,v2 by A2, A6, ANPROJ_1:22;
then consider a being Real such that
A8: a <> 0 and
A9: u1 = a * v2 by ANPROJ_1:1;
are_Prop u2,v1 by A3, A5, ANPROJ_1:22;
then consider b being Real such that
A10: b <> 0 and
A11: v1 = b * u2 by ANPROJ_1:1;
(a * v2) <X> (b * u2) = (- (a * b)) * (u2 <X> v2)
proof
reconsider p1 = a * v2, p2 = b * u2 as Element of (TOP-REAL 3) ;
A12: p1 `1 = (a * v2) . 1 by EUCLID_5:def 1
.= a * (v2 . 1) by RVSUM_1:44 ;
A13: p1 `2 = (a * v2) . 2 by EUCLID_5:def 2
.= a * (v2 . 2) by RVSUM_1:44 ;
A14: p1 `3 = (a * v2) . 3 by EUCLID_5:def 3
.= a * (v2 . 3) by RVSUM_1:44 ;
A15: p2 `1 = (b * u2) . 1 by EUCLID_5:def 1
.= b * (u2 . 1) by RVSUM_1:44 ;
A16: p2 `2 = (b * u2) . 2 by EUCLID_5:def 2
.= b * (u2 . 2) by RVSUM_1:44 ;
A17: p2 `3 = (b * u2) . 3 by EUCLID_5:def 3
.= b * (u2 . 3) by RVSUM_1:44 ;
A18: (a * v2) <X> (b * u2) = |[(((a * (v2 . 2)) * (b * (u2 . 3))) - ((a * (v2 . 3)) * (b * (u2 . 2)))),(((a * (v2 . 3)) * (b * (u2 . 1))) - ((a * (v2 . 1)) * (b * (u2 . 3)))),(((a * (v2 . 1)) * (b * (u2 . 2))) - ((a * (v2 . 2)) * (b * (u2 . 1))))]| by A12, A13, A14, A15, A16, A17, EUCLID_5:def 4;
( u2 `1 = u2 . 1 & u2 `2 = u2 . 2 & u2 `3 = u2 . 3 & v2 `1 = v2 . 1 & v2 `2 = v2 . 2 & v2 `3 = v2 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then (- (a * b)) * (u2 <X> v2) = (- (a * b)) * |[(((u2 . 2) * (v2 . 3)) - ((u2 . 3) * (v2 . 2))),(((u2 . 3) * (v2 . 1)) - ((u2 . 1) * (v2 . 3))),(((u2 . 1) * (v2 . 2)) - ((u2 . 2) * (v2 . 1)))]| by EUCLID_5:def 4
.= |[((- (a * b)) * (((u2 . 2) * (v2 . 3)) - ((u2 . 3) * (v2 . 2)))),((- (a * b)) * (((u2 . 3) * (v2 . 1)) - ((u2 . 1) * (v2 . 3)))),((- (a * b)) * (((u2 . 1) * (v2 . 2)) - ((u2 . 2) * (v2 . 1))))]| by EUCLID_5:8 ;
hence (a * v2) <X> (b * u2) = (- (a * b)) * (u2 <X> v2) by A18; :: thesis: verum
end;
then A19: are_Prop u1 <X> v1,u2 <X> v2 by A8, A10, A9, A11, ANPROJ_1:1;
A20: not u1 <X> v1 is zero
proof
assume u1 <X> v1 is zero ; :: thesis: contradiction
then are_Prop u1,v1 by ANPROJ_8:51;
hence contradiction by A1, A2, A3, ANPROJ_1:22; :: thesis: verum
end;
not u2 <X> v2 is zero
proof
assume u2 <X> v2 is zero ; :: thesis: contradiction
then are_Prop u2,v2 by ANPROJ_8:51;
hence contradiction by A1, A5, A6, ANPROJ_1:22; :: thesis: verum
end;
hence L2P (q,p) = L2P (p,q) by A19, A20, A4, A7, ANPROJ_1:22; :: thesis: p <> L2P (p,q)
thus p <> L2P (p,q) :: thesis: verum
proof
assume p = L2P (p,q) ; :: thesis: contradiction
then are_Prop u1,u1 <X> v1 by A2, A4, A20, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A21: u1 = a * (u1 <X> v1) by ANPROJ_1:1;
|(u1,(a * (u1 <X> v1)))| = a * |(u1,(u1 <X> v1))| by Th19
.= a * 0 by ANPROJ_8:44
.= 0 ;
then u1 = 0. (TOP-REAL 3) by A21, EUCLID_2:43;
hence contradiction ; :: thesis: verum
end;