let p, q be Point of (TOP-REAL 3); :: thesis: ( not p is zero & not q is zero & p <X> q = 0. (TOP-REAL 3) implies are_Prop p,q )
assume that
A1: not p is zero and
A2: not q is zero and
A3: p <X> q = 0. (TOP-REAL 3) ; :: thesis: are_Prop p,q
A4: |[(((p `2) * (q `3)) - ((p `3) * (q `2))),(((p `3) * (q `1)) - ((p `1) * (q `3))),(((p `1) * (q `2)) - ((p `2) * (q `1)))]| = |[0,0,0]| by A3, EUCLID_5:def 4, EUCLID_5:4;
then A5: ( ((p `2) * (q `3)) - ((p `3) * (q `2)) = |[0,0,0]| `1 & ((p `3) * (q `1)) - ((p `1) * (q `3)) = |[0,0,0]| `2 & ((p `1) * (q `2)) - ((p `2) * (q `1)) = |[0,0,0]| `3 ) by EUCLID_5:14;
then A6: ( ((p `2) * (q `3)) - ((p `3) * (q `2)) = 0 & ((p `3) * (q `1)) - ((p `1) * (q `3)) = 0 & ((p `1) * (q `2)) - ((p `2) * (q `1)) = 0 ) by EUCLID_5:14;
per cases ( ( p `1 <> 0 & p `2 <> 0 & p `3 <> 0 ) or p `1 = 0 or p `2 = 0 or p `3 = 0 ) ;
suppose A7: ( p `1 <> 0 & p `2 <> 0 & p `3 <> 0 ) ; :: thesis: are_Prop p,q
A8: ( q `1 <> 0 & q `2 <> 0 & q `3 <> 0 )
proof
assume ( q `1 = 0 or q `2 = 0 or q `3 = 0 ) ; :: thesis: contradiction
per cases then ( q `1 = 0 or q `2 = 0 or q `3 = 0 ) ;
end;
end;
reconsider l = (p `2) / (q `2) as Real ;
p = l * q
proof
A15: p `1 = ((p `3) * (q `1)) / (q `3) by A8, A6, XCMPLX_1:89
.= ((p `3) / (q `3)) * (q `1) by XCMPLX_1:74 ;
A16: p `2 = l * (q `2) by A8, XCMPLX_1:87;
p `3 = ((p `1) * (q `3)) / (q `1) by A8, A6, XCMPLX_1:89
.= ((p `1) / (q `1)) * (q `3) by XCMPLX_1:74 ;
then A17: p `3 = l * (q `3) by A8, A6, XCMPLX_1:94;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(l * (q `1)),(l * (q `2)),(l * (q `3))]| by A16, A17, A15, A8, A4, XCMPLX_1:94
.= l * q by EUCLID_5:7 ;
hence p = l * q ; :: thesis: verum
end;
hence are_Prop p,q by A7, A8, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
suppose A18: p `1 = 0 ; :: thesis: are_Prop p,q
per cases then ( p `2 <> 0 or p `3 <> 0 ) by EUCLID_5:3, A1, EUCLID_5:4;
suppose A19: p `2 <> 0 ; :: thesis: are_Prop p,q
then A20: q `1 = 0 by A18, A6, XCMPLX_1:6;
A21: q `2 <> 0 set l = (p `2) / (q `2);
p = ((p `2) / (q `2)) * q
proof
p `3 = ((p `2) * (q `3)) / (q `2) by A6, A21, XCMPLX_1:89;
then A22: p `3 = ((p `2) / (q `2)) * (q `3) by XCMPLX_1:74;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `2) / (q `2)) * (q `1)),(((p `2) / (q `2)) * (q `2)),(((p `2) / (q `2)) * (q `3))]| by A20, A18, A21, XCMPLX_1:87, A22
.= ((p `2) / (q `2)) * q by EUCLID_5:7 ;
hence p = ((p `2) / (q `2)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A21, A19, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
suppose A23: p `3 <> 0 ; :: thesis: are_Prop p,q
A24: q `1 = 0
proof
(p `3) * (q `1) = 0 by A18, A5, EUCLID_5:14;
hence q `1 = 0 by A23, XCMPLX_1:6; :: thesis: verum
end;
A25: q `3 <> 0 set l = (p `3) / (q `3);
p = ((p `3) / (q `3)) * q
proof
A27: ((p `3) / (q `3)) * (q `2) = ((p `2) * (q `3)) / (q `3) by A6, XCMPLX_1:74
.= p `2 by A25, XCMPLX_1:89 ;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `3) / (q `3)) * (q `1)),(((p `3) / (q `3)) * (q `2)),(((p `3) / (q `3)) * (q `3))]| by A24, A18, A27, A25, XCMPLX_1:87
.= ((p `3) / (q `3)) * q by EUCLID_5:7 ;
hence p = ((p `3) / (q `3)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A23, A25, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
end;
end;
suppose A28: p `2 = 0 ; :: thesis: are_Prop p,q
per cases then ( p `1 <> 0 or p `3 <> 0 ) by A1, EUCLID_5:3, EUCLID_5:4;
suppose A29: p `1 <> 0 ; :: thesis: are_Prop p,q
A30: q `2 = 0
proof
(p `1) * (q `2) = 0 by A28, A5, EUCLID_5:14;
hence q `2 = 0 by A29, XCMPLX_1:6; :: thesis: verum
end;
A31: q `1 <> 0 set l = (p `1) / (q `1);
p = ((p `1) / (q `1)) * q
proof
p `3 = ((p `1) * (q `3)) / (q `1) by A6, A31, XCMPLX_1:89;
then A33: p `3 = ((p `1) / (q `1)) * (q `3) by XCMPLX_1:74;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `1) / (q `1)) * (q `1)),(((p `1) / (q `1)) * (q `2)),(((p `1) / (q `1)) * (q `3))]| by A28, A30, A31, XCMPLX_1:87, A33
.= ((p `1) / (q `1)) * q by EUCLID_5:7 ;
hence p = ((p `1) / (q `1)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A31, A29, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
suppose A34: p `3 <> 0 ; :: thesis: are_Prop p,q
then A35: q `2 = 0 by A28, A6, XCMPLX_1:6;
A36: q `3 <> 0 set l = (p `3) / (q `3);
p = ((p `3) / (q `3)) * q
proof
A38: ((p `3) / (q `3)) * (q `1) = ((q `3) * (p `1)) / (q `3) by A6, XCMPLX_1:74
.= p `1 by A36, XCMPLX_1:89 ;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `3) / (q `3)) * (q `1)),(((p `3) / (q `3)) * (q `2)),(((p `3) / (q `3)) * (q `3))]| by A28, A35, A38, A36, XCMPLX_1:87
.= ((p `3) / (q `3)) * q by EUCLID_5:7 ;
hence p = ((p `3) / (q `3)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A34, A36, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
end;
end;
suppose A39: p `3 = 0 ; :: thesis: are_Prop p,q
per cases then ( p `2 <> 0 or p `1 <> 0 ) by A1, EUCLID_5:3, EUCLID_5:4;
suppose A40: p `2 <> 0 ; :: thesis: are_Prop p,q
A41: q `3 = 0
proof
(p `2) * (q `3) = 0 by A39, A5, EUCLID_5:14;
hence q `3 = 0 by A40, XCMPLX_1:6; :: thesis: verum
end;
A42: q `2 <> 0 set l = (p `2) / (q `2);
p = ((p `2) / (q `2)) * q
proof
p `1 = ((p `2) * (q `1)) / (q `2) by A6, A42, XCMPLX_1:89;
then A44: p `1 = ((p `2) / (q `2)) * (q `1) by XCMPLX_1:74;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `2) / (q `2)) * (q `1)),(((p `2) / (q `2)) * (q `2)),(((p `2) / (q `2)) * (q `3))]| by A39, A41, A42, XCMPLX_1:87, A44
.= ((p `2) / (q `2)) * q by EUCLID_5:7 ;
hence p = ((p `2) / (q `2)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A42, A40, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
suppose A45: p `1 <> 0 ; :: thesis: are_Prop p,q
then A46: q `3 = 0 by A39, A6, XCMPLX_1:6;
A47: q `1 <> 0 set l = (p `1) / (q `1);
p = ((p `1) / (q `1)) * q
proof
A49: ((p `1) / (q `1)) * (q `2) = ((q `1) * (p `2)) / (q `1) by A6, XCMPLX_1:74
.= p `2 by A47, XCMPLX_1:89 ;
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3
.= |[(((p `1) / (q `1)) * (q `1)),(((p `1) / (q `1)) * (q `2)),(((p `1) / (q `1)) * (q `3))]| by A39, A46, A49, A47, XCMPLX_1:87
.= ((p `1) / (q `1)) * q by EUCLID_5:7 ;
hence p = ((p `1) / (q `1)) * q ; :: thesis: verum
end;
hence are_Prop p,q by A45, A47, XCMPLX_1:50, ANPROJ_1:1; :: thesis: verum
end;
end;
end;
end;