let V be Z_Module; :: thesis: for v1, v2 being VECTOR of V st V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
let v1, v2 be VECTOR of V; :: thesis: ( V is Mult-cancelable implies ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) )
assume A1: V is Mult-cancelable ; :: thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) :: thesis: ( ( for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

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

now :: thesis: contradiction

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

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

a * v1 = - (b * v2) by A3, RLVECT_1:6
.= (- 1) * (b * v2) by ZMODUL01:2
.= ((- 1) * b) * v2 by ZMODUL01:def 4 ;
hence contradiction by A1, A2, A5, Th62; :: thesis: verum

end;

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

b * v2 = - (a * v1) by A3, RLVECT_1:6
.= (- 1) * (a * v1) by ZMODUL01:2
.= ((- 1) * a) * v1 by ZMODUL01:def 4 ;
hence contradiction by A1, A2, A6, Th62; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A8: now :: thesis: for a, b being Integer st b <> 0 holds
not b * v1 = a * v2

let a, b be Integer; :: thesis: ( b <> 0 implies not b * v1 = a * v2 )
assume A9: b <> 0 ; :: thesis: not b * v1 = a * v2
assume b * v1 = a * v2 ; :: thesis: contradiction
then b * v1 = (0. V) + (a * v2) by RLVECT_1:4;
then 0. V = (b * v1) - (a * v2) by RLSUB_2:61
.= (b * v1) + (a * (- v2)) by ZMODUL01:6
.= (b * v1) + ((- a) * v2) by ZMODUL01:5 ;
hence contradiction by A9, A7; :: thesis: verum

end;

now :: thesis: not v2 = 0. V

assume A10: v2 = 0. V ; :: thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:4
.= (0 * v1) + (0. V) by ZMODUL01:1
.= (0 * v1) + (1 * v2) by A10, ZMODUL01:1 ;
hence contradiction by A7; :: thesis: verum

end;

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