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: 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, A4, RLVECT_1:24;
then u = v by RLVECT_1:35;
hence u,v // w,y by Def1; :: thesis: verum
end;
A5: now
A6: now
A7: 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 ;
assume that
A8: 0 < a and
A9: b < 0 ; :: thesis: u,v // w,y
0 < - b by A9, XREAL_1:60;
hence u,v // w,y by A8, A7, Def1; :: thesis: verum
end;
A10: now
A11: (- 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 ;
assume that
A12: a < 0 and
A13: 0 < b ; :: thesis: u,v // w,y
0 < - a by A12, XREAL_1:60;
hence u,v // w,y by A13, A11, Def1; :: thesis: verum
end;
A14: now
assume ( a < 0 & b < 0 ) ; :: thesis: u,v // y,w
then A15: ( 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 A15, Def1; :: thesis: verum
end;
assume ( a <> 0 & b <> 0 ) ; :: thesis: ( u,v // w,y or u,v // y,w )
hence ( u,v // w,y or u,v // y,w ) by A1, A14, A10, A6, Def1; :: thesis: verum
end;
now
assume A16: 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, A16, RLVECT_1:24;
then w = y by RLVECT_1:35;
hence u,v // w,y by Def1; :: thesis: verum
end;
hence ( u,v // w,y or u,v // y,w ) by A3, A5; :: thesis: verum