let V be RealLinearSpace; :: thesis: for v, u, w, y being VECTOR of V
for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
let v, u, w, y be VECTOR of V; :: thesis: for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
let a, b be Real; :: thesis: ( a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y implies u,v // y,w )
assume that
A1: a * (v - u) = b * (w - y) and
A2: ( a <> 0 or b <> 0 ) ; :: thesis: ( u,v // w,y or u,v // y,w )
A3: now
assume A4: a = 0 ; :: thesis: u,v // w,y
then 0. V = b * (w - y) by A1, RLVECT_1:23;
then w - y = 0. V by A2, A4, RLVECT_1:24;
then w = y by RLVECT_1:35;
hence u,v // w,y by Def1; :: thesis: verum
end;
A5: now
assume A6: b = 0 ; :: thesis: u,v // w,y
then 0. V = a * (v - u) by A1, RLVECT_1:23;
then v - u = 0. V by A2, A6, RLVECT_1:24;
then u = v by RLVECT_1:35;
hence u,v // w,y by Def1; :: thesis: verum
end;
now
assume A7: ( a <> 0 & b <> 0 ) ; :: thesis: ( u,v // w,y or u,v // y,w )
A8: now
assume ( a < 0 & b < 0 ) ; :: thesis: u,v // y,w
then A9: ( 0 < - a & 0 < - b ) by XREAL_1:60;
(- a) * (v - u) = a * (- (v - u)) by RLVECT_1:38
.= - (b * (w - y)) by A1, RLVECT_1:39
.= b * (- (w - y)) by RLVECT_1:39
.= (- b) * (w - y) by RLVECT_1:38 ;
hence u,v // y,w by A9, Def1; :: thesis: verum
end;
A10: now
assume ( a < 0 & 0 < b ) ; :: thesis: u,v // w,y
then A11: ( 0 < - a & 0 < b ) by XREAL_1:60;
(- a) * (v - u) = a * (- (v - u)) by RLVECT_1:38
.= - (b * (w - y)) by A1, RLVECT_1:39
.= b * (- (w - y)) by RLVECT_1:39
.= b * (y - w) by RLVECT_1:47 ;
hence u,v // w,y by A11, Def1; :: thesis: verum
end;
now
assume ( 0 < a & b < 0 ) ; :: thesis: u,v // w,y
then A12: ( 0 < a & 0 < - b ) by XREAL_1:60;
a * (v - u) = - (- (b * (w - y))) by A1, RLVECT_1:30
.= - (b * (- (w - y))) by RLVECT_1:39
.= - (b * (y - w)) by RLVECT_1:47
.= b * (- (y - w)) by RLVECT_1:39
.= (- b) * (y - w) by RLVECT_1:38 ;
hence u,v // w,y by A12, Def1; :: thesis: verum
end;
hence ( u,v // w,y or u,v // y,w ) by A1, A7, A8, A10, Def1; :: thesis: verum
end;
hence ( u,v // w,y or u,v // y,w ) by A3, A5; :: thesis: verum