let R be Ring; for V being LeftMod of R
for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
let V be LeftMod of R; for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
let v1, v2 be Vector of V; ( R = INT.Ring & V is Mult-cancelable implies ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ) )
assume A1:
( R = INT.Ring & V is Mult-cancelable )
; ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
thus
( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
( ( for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A7:
for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R )
; ( v1 <> v2 & {v1,v2} is linearly-independent )
hence
( v1 <> v2 & {v1,v2} is linearly-independent )
by A8, A1, Th62; verum