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

proof

reconsider N0 = 0 , N1 = - 1 as Element of INT by INT_1:def 2;
deffunc H₁( Element of V) -> Element of INT = N0;
assume that
A2: v1 <> v2 and
A3: {v1,v2} is linearly-independent ; :: thesis: ( v2 <> 0. V & ( for a, b being Integer st b <> 0 holds
b * v1 <> a * v2 ) )
thus v2 <> 0. V by A3, Th60; :: thesis: for a, b being Integer st b <> 0 holds
b * v1 <> a * v2
let a, b be Integer; :: thesis: ( b <> 0 implies b * v1 <> a * v2 )
assume A4: b <> 0 ; :: thesis: b * v1 <> a * v2
reconsider Na = a as Element of INT by INT_1:def 2;
reconsider Nb = - b as Element of INT by INT_1:def 2;
consider f being Function of the carrier of V,INT such that
A5: ( f . v1 = Nb & f . v2 = Na ) and
A6: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H₁(v) from FUNCT_2:sch 7(A2);
reconsider f = f as Element of Funcs ( the carrier of V,INT) by FUNCT_2:8;

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

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

end;

then reconsider f = f as Z_Linear_Combination of V by Def18;
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 A7: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in {v1,v2} ; :: thesis: contradiction
then ( x <> v1 & x <> v2 ) by TARSKI:def 2;
hence contradiction by A6, A7; :: thesis: verum

end;

then reconsider f = f as Z_Linear_Combination of {v1,v2} by Def21;
f . v1 <> 0 by A5, A4;
then A8: v1 in Carrier f ;
set w = a * v2;
assume A9: b * v1 = a * v2 ; :: thesis: contradiction
Sum f = (Nb * v1) + (Na * v2) by A2, A5, Th22
.= (b * (- v1)) + (Na * v2) by ZMODUL01:5
.= (- (a * v2)) + (a * v2) by A9, ZMODUL01:6
.= - ((a * v2) - (a * v2)) by RLVECT_1:33
.= - (0. V) by RLVECT_1:15
.= 0. V by RLVECT_1:12 ;
hence contradiction by A3, A8; :: thesis: verum

end;

assume A10: v2 <> 0. V ; :: thesis: ( ex a, b being Integer st
( b <> 0 & not b * v1 <> a * v2 ) or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A11: for a, b being Integer st b <> 0 holds
b * v1 <> a * v2 ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A12: ( 1 * v2 = v2 & 1 * v1 = v1 ) by ZMODUL01:def 5;
hence v1 <> v2 by A11; :: thesis: {v1,v2} is linearly-independent
let l be Z_Linear_Combination of {v1,v2}; :: according to ZMODUL02:def 36 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A13: Sum l = 0. V and
A14: Carrier l <> {} ; :: thesis: contradiction
A15: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A11, A12, A13, Th22;
set x = the Element of Carrier l;
Carrier l c= {v1,v2} by Def21;
then A16: the Element of Carrier l in {v1,v2} by A14;
the Element of Carrier l in Carrier l by A14;
then A17: ex u being VECTOR of V st
( the Element of Carrier l = u & l . u <> 0 ) ;

now :: thesis: contradiction

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

suppose A18: l . v1 <> 0 ; :: thesis: contradiction

(l . v1) * v1 = - ((l . v2) * v2) by A15, RLVECT_1:6
.= (- 1) * ((l . v2) * v2) by ZMODUL01:2
.= ((- 1) * (l . v2)) * v2 by ZMODUL01:def 4 ;
hence contradiction by A11, A18; :: thesis: verum

end;

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

0. V = ((l . v1) * v1) + ((l . v2) * v2) by A11, A12, A13, Th22
.= (0. V) + ((l . v2) * v2) by A19, ZMODUL01:1
.= (l . v2) * v2 by RLVECT_1:4 ;
hence contradiction by A1, A10, A19; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum