let V be RealLinearSpace; :: thesis: for u, v, 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 u, v, 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 :: thesis: ( b = 0 implies u,v // w,y )
assume A4: b = 0 ; :: thesis: u,v // w,y
then 0. V = a * (v - u) by A1, RLVECT_1:10;
then v - u = 0. V by A2, A4, RLVECT_1:11;
then u = v by RLVECT_1:21;
hence u,v // w,y ; :: thesis: verum
end;
A5: now :: thesis: ( a <> 0 & b <> 0 & not u,v // w,y implies u,v // y,w )
A6: now :: thesis: ( 0 < a & b < 0 implies u,v // w,y )
A7: a * (v - u) = - (- (b * (w - y))) by A1, RLVECT_1:17
.= - (b * (- (w - y))) by RLVECT_1:25
.= - (b * (y - w)) by RLVECT_1:33
.= b * (- (y - w)) by RLVECT_1:25
.= (- b) * (y - w) by RLVECT_1:24 ;
assume that
A8: 0 < a and
A9: b < 0 ; :: thesis: u,v // w,y
0 < - b by A9, XREAL_1:58;
hence u,v // w,y by A8, A7; :: thesis: verum
end;
A10: now :: thesis: ( a < 0 & 0 < b implies u,v // w,y )
A11: (- a) * (v - u) = a * (- (v - u)) by RLVECT_1:24
.= - (b * (w - y)) by A1, RLVECT_1:25
.= b * (- (w - y)) by RLVECT_1:25
.= b * (y - w) by RLVECT_1:33 ;
assume that
A12: a < 0 and
A13: 0 < b ; :: thesis: u,v // w,y
0 < - a by A12, XREAL_1:58;
hence u,v // w,y by A13, A11; :: thesis: verum
end;
A14: now :: thesis: ( a < 0 & b < 0 implies u,v // y,w )
assume ( a < 0 & b < 0 ) ; :: thesis: u,v // y,w
then A15: ( 0 < - a & 0 < - b ) by XREAL_1:58;
(- a) * (v - u) = a * (- (v - u)) by RLVECT_1:24
.= - (b * (w - y)) by A1, RLVECT_1:25
.= b * (- (w - y)) by RLVECT_1:25
.= (- b) * (w - y) by RLVECT_1:24 ;
hence u,v // y,w by A15; :: 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; :: thesis: verum
end;
now :: thesis: ( a = 0 implies u,v // w,y )
assume A16: a = 0 ; :: thesis: u,v // w,y
then 0. V = b * (w - y) by A1, RLVECT_1:10;
then w - y = 0. V by A2, A16, RLVECT_1:11;
then w = y by RLVECT_1:21;
hence u,v // w,y ; :: thesis: verum
end;
hence ( u,v // w,y or u,v // y,w ) by A3, A5; :: thesis: verum