let R be Ring; :: thesis: for V being LeftMod of R

for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

let V be LeftMod of R; :: thesis: for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

let v be Vector of V; :: thesis: ( not R is degenerated & V is Mult-cancelable implies ( {v} is linearly-independent iff v <> 0. V ) )

assume A1: ( not R is degenerated & V is Mult-cancelable ) ; :: 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 )

let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )

A3: Carrier l c= {v} by VECTSP_6:def 4;

assume A4: Sum l = 0. V ; :: thesis: Carrier l = {}

for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

let V be LeftMod of R; :: thesis: for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

let v be Vector of V; :: thesis: ( not R is degenerated & V is Mult-cancelable implies ( {v} is linearly-independent iff v <> 0. V ) )

assume A1: ( not R is degenerated & V is Mult-cancelable ) ; :: 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 A2:
v <> 0. V
; :: thesis: {v} is linearly-independent
assume
{v} is linearly-independent
; :: thesis: v <> 0. V

then not 0. V in {v} by Th57, A1;

hence v <> 0. V by TARSKI:def 1; :: thesis: verum

end;then not 0. V in {v} by Th57, A1;

hence v <> 0. V by TARSKI:def 1; :: thesis: verum

let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )

A3: Carrier l c= {v} by VECTSP_6:def 4;

assume A4: Sum l = 0. V ; :: thesis: Carrier l = {}

now :: thesis: Carrier l = {} end;

hence
Carrier l = {}
; :: thesis: verumper cases
( Carrier l = {} or Carrier l = {v} )
by A3, ZFMISC_1:33;

end;

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

then A6:
0. V = (l . v) * v
by A4, Th24;

end;now :: thesis: not v in Carrier l

hence
Carrier l = {}
by A5, TARSKI:def 1; :: thesis: verumassume
v in Carrier l
; :: thesis: contradiction

then ex u being Vector of V st

( v = u & l . u <> 0. R ) ;

hence contradiction by A2, A6, A1; :: thesis: verum

end;then ex u being Vector of V st

( v = u & l . u <> 0. R ) ;

hence contradiction by A2, A6, A1; :: thesis: verum