let GF be Field; :: thesis: for V being VectSp of GF
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
let V be VectSp of GF; :: thesis: for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
let v be Vector of V; :: thesis: ( {v} is linearly-independent iff v <> 0. V )
thus ( {v} is linearly-independent implies v <> 0. V ) :: thesis: ( v <> 0. V implies {v} is linearly-independent )

proof

assume {v} is linearly-independent ; :: thesis: v <> 0. V
then not 0. V in {v} by Th3;
hence v <> 0. V by TARSKI:def 1; :: thesis: verum

end;

assume A1: v <> 0. V ; :: thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A2: Sum l = 0. V ; :: thesis: Carrier l = {}
A3: Carrier l c= {v} by VECTSP_6:def 7;

now

per cases ( Carrier l = {} or Carrier l = {v} ) by A3, ZFMISC_1:39;

suppose Carrier l = {} ; :: thesis: Carrier l = {}

hence Carrier l = {} ; :: thesis: verum

end;

suppose A4: Carrier l = {v} ; :: thesis: Carrier l = {}

A5: 0. V = (l . v) * v by A2, VECTSP_6:43;

now

assume v in Carrier l ; :: thesis: contradiction
then ex u being Vector of V st
( v = u & l . u <> 0. GF ) ;
hence contradiction by A1, A5, VECTSP_1:60; :: thesis: verum

end;

hence Carrier l = {} by A4, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence Carrier l = {} ; :: thesis: verum