let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
let v1, v2 be Vector of V; :: thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) ) :: thesis: ( ( for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

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

now :: thesis: contradiction

per cases ( a <> 0. GF or b <> 0. GF ) by A3;

suppose A4: a <> 0. GF ; :: thesis: contradiction

0. V = (a ") * ((a * v1) + (b * v2)) by A2, VECTSP_1:15
.= ((a ") * (a * v1)) + ((a ") * (b * v2)) by VECTSP_1:def 14
.= (((a ") * a) * v1) + ((a ") * (b * v2)) by VECTSP_1:def 16
.= (((a ") * a) * v1) + (((a ") * b) * v2) by VECTSP_1:def 16
.= ((1_ GF) * v1) + (((a ") * b) * v2) by A4, VECTSP_1:def 10
.= v1 + (((a ") * b) * v2) ;
then v1 = - (((a ") * b) * v2) by VECTSP_1:16
.= (- (1_ GF)) * (((a ") * b) * v2) by VECTSP_1:14
.= ((- (1_ GF)) * ((a ") * b)) * v2 by VECTSP_1:def 16 ;
hence contradiction by A1, Th5; :: thesis: verum

end;

suppose A5: b <> 0. GF ; :: thesis: contradiction

0. V = (b ") * ((a * v1) + (b * v2)) by A2, VECTSP_1:15
.= ((b ") * (a * v1)) + ((b ") * (b * v2)) by VECTSP_1:def 14
.= (((b ") * a) * v1) + ((b ") * (b * v2)) by VECTSP_1:def 16
.= (((b ") * a) * v1) + (((b ") * b) * v2) by VECTSP_1:def 16
.= (((b ") * a) * v1) + ((1_ GF) * v2) by A5, VECTSP_1:def 10
.= (((b ") * a) * v1) + v2 ;
then v2 = - (((b ") * a) * v1) by VECTSP_1:16
.= (- (1_ GF)) * (((b ") * a) * v1) by VECTSP_1:14
.= ((- (1_ GF)) * ((b ") * a)) * v1 by VECTSP_1:def 16 ;
hence contradiction by A1, Th5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A7: now :: thesis: for a being Element of GF holds not v1 = a * v2

let a be Element of GF; :: thesis: not v1 = a * v2
assume v1 = a * v2 ; :: thesis: contradiction
then v1 = (0. V) + (a * v2) by RLVECT_1:4;
then 0. V = v1 - (a * v2) by VECTSP_2:2
.= v1 + ((- a) * v2) by VECTSP_1:21
.= ((1. GF) * v1) + ((- a) * v2) ;
hence contradiction by A6; :: thesis: verum

end;

now :: thesis: not v2 = 0. V

assume A8: v2 = 0. V ; :: thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:4
.= ((0. GF) * v1) + (0. V) by VECTSP_1:15
.= ((0. GF) * v1) + ((1. GF) * v2) by A8 ;
hence contradiction by A6; :: thesis: verum

end;

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