let R be Skew-Field; for V being LeftMod of R
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar 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 holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
let v1, v2 be Vector of V; ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar 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 Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
( ( for a, b being Scalar 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 A6:
for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R )
; ( v1 <> v2 & {v1,v2} is linearly-independent )
A7:
now for a being Scalar of R holds not v1 = a * v2end;
hence
( v1 <> v2 & {v1,v2} is linearly-independent )
by A7, Th16; verum