let V be RealLinearSpace; :: thesis: ( ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w ) )
given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; :: thesis: ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w )
A2: ( u <> 0. V & v <> 0. V ) by A1, Th19;
A3: not 0. V,u // v, 0. V
proof
A4: now :: thesis: for a, b being Real holds
( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * ((0. V) - v) )
given a, b being Real such that A5: 0 < a and
0 < b and
A6: a * (u - (0. V)) = b * ((0. V) - v) ; :: thesis: contradiction
( a * u = a * (u - (0. V)) & b * ((0. V) - v) = b * (- v) ) by RLVECT_1:13, RLVECT_1:14;
then a * u = - (b * v) by A6, RLVECT_1:25;
then (a * u) + (b * v) = 0. V by RLVECT_1:5;
hence contradiction by A1, A5; :: thesis: verum
end;
assume 0. V,u // v, 0. V ; :: thesis: contradiction
hence contradiction by A2, A4; :: thesis: verum
end;
not 0. V,u // 0. V,v
proof
A7: now :: thesis: for a, b being Real holds
( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * (v - (0. V)) )
given a, b being Real such that A8: 0 < a and
0 < b and
A9: a * (u - (0. V)) = b * (v - (0. V)) ; :: thesis: contradiction
( a * u = a * (u - (0. V)) & b * (v - (0. V)) = b * v ) by RLVECT_1:13;
then 0. V = (a * u) - (b * v) by A9, RLVECT_1:15
.= (a * u) + (b * (- v)) by RLVECT_1:25
.= (a * u) + ((- b) * v) by RLVECT_1:24 ;
hence contradiction by A1, A8; :: thesis: verum
end;
assume 0. V,u // 0. V,v ; :: thesis: contradiction
hence contradiction by A2, A7; :: thesis: verum
end;
hence ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w ) by A3; :: thesis: verum