let a, u, v be non zero Element of (TOP-REAL 3); :: thesis: ( not are_Prop u,v & |(a,u)| = 0 & |(a,v)| = 0 implies are_Prop a,u <X> v )
assume that
A1: not are_Prop u,v and
A2: |(a,u)| = 0 and
A3: |(a,v)| = 0 ; :: thesis: are_Prop a,u <X> v
not u <X> v is zero by A1, ANPROJ_8:51;
then reconsider uv = u <X> v as non zero Element of (TOP-REAL 3) ;
A4: ( (((a `1) * (u `1)) + ((a `2) * (u `2))) + ((a `3) * (u `3)) = 0 & (((a `1) * (v `1)) + ((a `2) * (v `2))) + ((a `3) * (v `3)) = 0 ) by A2, A3, EUCLID_5:29;
per cases ( a `1 <> 0 or a `2 <> 0 or a `3 <> 0 ) by EUCLID_5:3, EUCLID_5:4;
suppose A5: a `1 <> 0 ; :: thesis: are_Prop a,u <X> v
then A6: ( u `1 = (- (((a `2) / (a `1)) * (u `2))) - (((a `3) / (a `1)) * (u `3)) & v `1 = (- (((a `2) / (a `1)) * (v `2))) - (((a `3) / (a `1)) * (v `3)) ) by A4, ANPROJ_8:13;
set p1 = u;
set p2 = v;
now :: thesis: ( u <X> v = ((((u `2) * (v `3)) - ((u `3) * (v `2))) * (1 / (a `1))) * a & (((u `2) * (v `3)) - ((u `3) * (v `2))) * (1 / (a `1)) <> 0 )
reconsider r = a `1 as Real ;
thus A7: u <X> v = |[(1 * (((u `2) * (v `3)) - ((u `3) * (v `2)))),(((a `2) / (a `1)) * (((u `2) * (v `3)) - ((u `3) * (v `2)))),(((a `3) / (a `1)) * ((- ((u `3) * (v `2))) + ((u `2) * (v `3))))]| by A6
.= (((u `2) * (v `3)) - ((u `3) * (v `2))) * |[1,((a `2) / (a `1)),((a `3) / (a `1))]| by EUCLID_5:8
.= (((u `2) * (v `3)) - ((u `3) * (v `2))) * |[((a `1) / r),((a `2) / r),((a `3) / r)]| by A5, XCMPLX_1:60
.= (((u `2) * (v `3)) - ((u `3) * (v `2))) * ((1 / (a `1)) * a) by EUCLID_5:7
.= ((((u `2) * (v `3)) - ((u `3) * (v `2))) * (1 / (a `1))) * a by RVSUM_1:49 ; :: thesis: (((u `2) * (v `3)) - ((u `3) * (v `2))) * (1 / (a `1)) <> 0
((u `2) * (v `3)) - ((u `3) * (v `2)) <> 0
proof
assume ((u `2) * (v `3)) - ((u `3) * (v `2)) = 0 ; :: thesis: contradiction
then u <X> v = |[(0 * (a `1)),(0 * (a `2)),(0 * (a `3))]| by A7, EUCLID_5:7
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A1, ANPROJ_8:51; :: thesis: verum
end;
hence (((u `2) * (v `3)) - ((u `3) * (v `2))) * (1 / (a `1)) <> 0 by A5; :: thesis: verum
end;
hence are_Prop a,u <X> v by ANPROJ_1:1; :: thesis: verum
end;
suppose A8: a `2 <> 0 ; :: thesis: are_Prop a,u <X> v
then A9: ( u `2 = (- (((a `1) / (a `2)) * (u `1))) - (((a `3) / (a `2)) * (u `3)) & v `2 = (- (((a `1) / (a `2)) * (v `1))) - (((a `3) / (a `2)) * (v `3)) ) by A4, ANPROJ_8:13;
set p1 = u;
set p2 = v;
now :: thesis: ( u <X> v = ((((u `3) * (v `1)) - ((u `1) * (v `3))) * (1 / (a `2))) * a & (((u `3) * (v `1)) - ((u `1) * (v `3))) * (1 / (a `2)) <> 0 )
reconsider r = a `2 as Real ;
thus A10: u <X> v = |[(((a `1) / (a `2)) * (((u `3) * (v `1)) - ((u `1) * (v `3)))),(1 * (((u `3) * (v `1)) - ((u `1) * (v `3)))),(((a `3) / (a `2)) * (((u `3) * (v `1)) - ((u `1) * (v `3))))]| by A9
.= (((u `3) * (v `1)) - ((u `1) * (v `3))) * |[((a `1) / (a `2)),1,((a `3) / (a `2))]| by EUCLID_5:8
.= (((u `3) * (v `1)) - ((u `1) * (v `3))) * |[((a `1) / r),(r / r),((a `3) / r)]| by A8, XCMPLX_1:60
.= (((u `3) * (v `1)) - ((u `1) * (v `3))) * ((1 / (a `2)) * a) by EUCLID_5:7
.= ((((u `3) * (v `1)) - ((u `1) * (v `3))) * (1 / (a `2))) * a by RVSUM_1:49 ; :: thesis: (((u `3) * (v `1)) - ((u `1) * (v `3))) * (1 / (a `2)) <> 0
((u `3) * (v `1)) - ((u `1) * (v `3)) <> 0
proof
assume ((u `3) * (v `1)) - ((u `1) * (v `3)) = 0 ; :: thesis: contradiction
then u <X> v = |[(0 * (a `1)),(0 * (a `2)),(0 * (a `3))]| by A10, EUCLID_5:7
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A1, ANPROJ_8:51; :: thesis: verum
end;
hence (((u `3) * (v `1)) - ((u `1) * (v `3))) * (1 / (a `2)) <> 0 by A8; :: thesis: verum
end;
hence are_Prop a,u <X> v by ANPROJ_1:1; :: thesis: verum
end;
suppose A11: a `3 <> 0 ; :: thesis: are_Prop a,u <X> v
( (((a `3) * (u `3)) + ((a `1) * (u `1))) + ((a `2) * (u `2)) = 0 & (((a `3) * (v `3)) + ((a `1) * (v `1))) + ((a `2) * (v `2)) = 0 ) by A4;
then A12: ( u `3 = (- (((a `1) / (a `3)) * (u `1))) - (((a `2) / (a `3)) * (u `2)) & v `3 = (- (((a `1) / (a `3)) * (v `1))) - (((a `2) / (a `3)) * (v `2)) ) by A11, ANPROJ_8:13;
set p1 = u;
set p2 = v;
now :: thesis: ( u <X> v = ((((u `1) * (v `2)) - ((u `2) * (v `1))) * (1 / (a `3))) * a & (((u `1) * (v `2)) - ((u `2) * (v `1))) * (1 / (a `3)) <> 0 )
reconsider r = a `3 as Real ;
thus A13: u <X> v = |[(((a `1) / (a `3)) * (((u `1) * (v `2)) - ((u `2) * (v `1)))),(((a `2) / (a `3)) * (((u `1) * (v `2)) - ((u `2) * (v `1)))),(1 * (((u `1) * (v `2)) - ((u `2) * (v `1))))]| by A12
.= (((u `1) * (v `2)) - ((u `2) * (v `1))) * |[((a `1) / (a `3)),((a `2) / (a `3)),1]| by EUCLID_5:8
.= (((u `1) * (v `2)) - ((u `2) * (v `1))) * |[((a `1) / r),((a `2) / r),(r / r)]| by A11, XCMPLX_1:60
.= (((u `1) * (v `2)) - ((u `2) * (v `1))) * ((1 / (a `3)) * a) by EUCLID_5:7
.= ((((u `1) * (v `2)) - ((u `2) * (v `1))) * (1 / (a `3))) * a by RVSUM_1:49 ; :: thesis: (((u `1) * (v `2)) - ((u `2) * (v `1))) * (1 / (a `3)) <> 0
((u `1) * (v `2)) - ((u `2) * (v `1)) <> 0
proof
assume ((u `1) * (v `2)) - ((u `2) * (v `1)) = 0 ; :: thesis: contradiction
then u <X> v = |[(0 * (a `1)),(0 * (a `2)),(0 * (a `3))]| by A13, EUCLID_5:7
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A1, ANPROJ_8:51; :: thesis: verum
end;
hence (((u `1) * (v `2)) - ((u `2) * (v `1))) * (1 / (a `3)) <> 0 by A11; :: thesis: verum
end;
hence are_Prop a,u <X> v by ANPROJ_1:1; :: thesis: verum
end;
end;