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 ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
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 ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
let v1, v2 be Vector of V; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) ) :: thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

deffunc H₁( set ) -> Element of the carrier of GF = 0. GF;
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent ; :: thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) )
thus v2 <> 0. V by A2, Th4; :: thesis: for a being Element of GF holds v1 <> a * v2
let a be Element of GF; :: thesis: v1 <> a * v2
consider f being Function of V,GF such that
A3: ( f . v1 = - (1_ GF) & f . v2 = a ) and
A4: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H₁(v) from FUNCT_2:sch 7(A1);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

now :: thesis: for v being Vector of V st not v in {v1,v2} holds
f . v = 0. GF

let v be Vector of V; :: thesis: ( not v in {v1,v2} implies f . v = 0. GF )
assume not v in {v1,v2} ; :: thesis: f . v = 0. GF
then ( v <> v1 & v <> v2 ) by TARSKI:def 2;
hence f . v = 0. GF by A4; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= {v1,v2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v1,v2} )
assume x in Carrier f ; :: thesis: x in {v1,v2}
then A5: ex u being Vector of V st
( x = u & f . u <> 0. GF ) ;
assume not x in {v1,v2} ; :: thesis: contradiction
then ( x <> v1 & x <> v2 ) by TARSKI:def 2;
hence contradiction by A4, A5; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v1,v2} by VECTSP_6:def 4;

A6: now :: thesis: v1 in Carrier f

assume not v1 in Carrier f ; :: thesis: contradiction
then 0. GF = - (1_ GF) by A3;
hence contradiction by VECTSP_6:49; :: thesis: verum

end;

set w = a * v2;
assume v1 = a * v2 ; :: thesis: contradiction
then Sum f = ((- (1_ GF)) * (a * v2)) + (a * v2) by A1, A3, VECTSP_6:18
.= (- (a * v2)) + (a * v2) by VECTSP_1:14
.= - ((a * v2) - (a * v2)) by VECTSP_1:17
.= - (0. V) by VECTSP_1:19
.= 0. V by RLVECT_1:12 ;
hence contradiction by A2, A6; :: thesis: verum

end;

assume A7: v2 <> 0. V ; :: thesis: ( ex a being Element of GF st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A8: for a being Element of GF holds v1 <> a * v2 ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A9: (1_ GF) * v2 = v2 ;
hence v1 <> v2 by A8; :: thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; :: thesis: contradiction
A12: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A8, A9, A10, VECTSP_6:18;
set x = the Element of Carrier l;
Carrier l c= {v1,v2} by VECTSP_6:def 4;
then A13: the Element of Carrier l in {v1,v2} by A11;
the Element of Carrier l in Carrier l by A11;
then A14: ex u being Vector of V st
( the Element of Carrier l = u & l . u <> 0. GF ) ;

now :: thesis: contradiction

per cases ( l . v1 <> 0. GF or ( l . v2 <> 0. GF & l . v1 = 0. GF ) ) by A14, A13, TARSKI:def 2;

suppose A15: l . v1 <> 0. GF ; :: thesis: contradiction

0. V = ((l . v1) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, VECTSP_1:15
.= (((l . v1) ") * ((l . v1) * v1)) + (((l . v1) ") * ((l . v2) * v2)) by VECTSP_1:def 14
.= ((((l . v1) ") * (l . v1)) * v1) + (((l . v1) ") * ((l . v2) * v2)) by VECTSP_1:def 16
.= ((((l . v1) ") * (l . v1)) * v1) + ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:def 16
.= ((1_ GF) * v1) + ((((l . v1) ") * (l . v2)) * v2) by A15, VECTSP_1:def 10
.= v1 + ((((l . v1) ") * (l . v2)) * v2) ;
then v1 = - ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:16
.= (- (1_ GF)) * ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:14
.= ((- (1_ GF)) * (((l . v1) ") * (l . v2))) * v2 by VECTSP_1:def 16 ;
hence contradiction by A8; :: thesis: verum

end;

suppose A16: ( l . v2 <> 0. GF & l . v1 = 0. GF ) ; :: thesis: contradiction

0. V = ((l . v2) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, VECTSP_1:15
.= (((l . v2) ") * ((l . v1) * v1)) + (((l . v2) ") * ((l . v2) * v2)) by VECTSP_1:def 14
.= ((((l . v2) ") * (l . v1)) * v1) + (((l . v2) ") * ((l . v2) * v2)) by VECTSP_1:def 16
.= ((((l . v2) ") * (l . v1)) * v1) + ((((l . v2) ") * (l . v2)) * v2) by VECTSP_1:def 16
.= ((((l . v2) ") * (l . v1)) * v1) + ((1_ GF) * v2) by A16, VECTSP_1:def 10
.= ((((l . v2) ") * (l . v1)) * v1) + v2
.= ((0. GF) * v1) + v2 by A16
.= (0. V) + v2 by VECTSP_1:15
.= v2 by RLVECT_1:4 ;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum