let a, b be Real; :: thesis: for V being RealLinearSpace
for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds
{u,(a * w),(b * v)} is linearly-independent
let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds
{u,(a * w),(b * v)} is linearly-independent
let u, v, w be VECTOR of V; :: thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 implies {u,(a * w),(b * v)} is linearly-independent )
assume that
A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) and
A2: ( a <> 0 & b <> 0 ) ; :: thesis: {u,(a * w),(b * v)} is linearly-independent
now :: thesis: for c, d, e being Real st ((c * u) + (d * (a * w))) + (e * (b * v)) = 0. V holds
( c = 0 & d = 0 & e = 0 )
let c, d, e be Real; :: thesis: ( ((c * u) + (d * (a * w))) + (e * (b * v)) = 0. V implies ( c = 0 & d = 0 & e = 0 ) )
assume ((c * u) + (d * (a * w))) + (e * (b * v)) = 0. V ; :: thesis: ( c = 0 & d = 0 & e = 0 )
then A3: 0. V = ((c * u) + ((d * a) * w)) + (e * (b * v)) by RLVECT_1:def 7
.= ((c * u) + ((d * a) * w)) + ((e * b) * v) by RLVECT_1:def 7 ;
then ( d * a = 0 & e * b = 0 ) by A1, Th7;
hence ( c = 0 & d = 0 & e = 0 ) by A1, A2, A3, Th7, XCMPLX_1:6; :: thesis: verum
end;
hence {u,(a * w),(b * v)} is linearly-independent by Th7; :: thesis: verum