let R be Skew-Field; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) ) :: thesis: ( ( 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 ) )

proof

assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent ; :: thesis: for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R )
let a, b be Scalar of R; :: thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0. R & b = 0. R ) )
assume that
A3: (a * v1) + (b * v2) = 0. V and
A4: ( a <> 0. R or b <> 0. R ) ; :: thesis: contradiction

now

per cases ( a <> 0. R or b <> 0. R ) by A4;

suppose A5: a <> 0. R ; :: thesis: contradiction

0. V = (a " ) * ((a * v1) + (b * v2)) by A3, VECTSP_2:88
.= ((a " ) * (a * v1)) + ((a " ) * (b * v2)) by VECTSP_1:def 26
.= (((a " ) * a) * v1) + ((a " ) * (b * v2)) by VECTSP_1:def 26
.= (((a " ) * a) * v1) + (((a " ) * b) * v2) by VECTSP_1:def 26
.= ((1. R) * v1) + (((a " ) * b) * v2) by A5, Lm2
.= v1 + (((a " ) * b) * v2) by VECTSP_1:def 26 ;
then v1 = - (((a " ) * b) * v2) by VECTSP_1:63
.= (- (1. R)) * (((a " ) * b) * v2) by VECTSP_1:59
.= ((- (1. R)) * ((a " ) * b)) * v2 by VECTSP_1:def 26 ;
hence contradiction by A1, A2, Th24; :: thesis: verum

end;

suppose A6: b <> 0. R ; :: thesis: contradiction

0. V = (b " ) * ((a * v1) + (b * v2)) by A3, VECTSP_2:88
.= ((b " ) * (a * v1)) + ((b " ) * (b * v2)) by VECTSP_1:def 26
.= (((b " ) * a) * v1) + ((b " ) * (b * v2)) by VECTSP_1:def 26
.= (((b " ) * a) * v1) + ((1. R) * v2) by A6, Lm2
.= (((b " ) * a) * v1) + v2 by VECTSP_1:def 26 ;
then v2 = - (((b " ) * a) * v1) by VECTSP_1:63
.= (- (1. R)) * (((b " ) * a) * v1) by VECTSP_1:59
.= ((- (1. R)) * ((b " ) * a)) * v1 by VECTSP_1:def 26 ;
hence contradiction by A1, A2, Th24; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

assume A7: for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

A8: now

assume A9: v2 = 0. V ; :: thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:def 7
.= ((0. R) * v1) + (0. V) by VECTSP_2:88
.= ((0. R) * v1) + ((1. R) * v2) by A9, VECTSP_2:88 ;
hence contradiction by A7; :: thesis: verum

end;

now

let a be Scalar of R; :: thesis: not v1 = a * v2
assume v1 = a * v2 ; :: thesis: contradiction
then v1 = (0. V) + (a * v2) by RLVECT_1:def 7;
then 0. V = v1 - (a * v2) by RLSUB_2:78
.= v1 + ((- a) * v2) by VECTSP_1:68
.= ((1. R) * v1) + ((- a) * v2) by VECTSP_1:def 26 ;
hence contradiction by A7; :: thesis: verum

end;

hence ( v1 <> v2 & {v1,v2} is linearly-independent ) by A8, Th24; :: thesis: verum