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