let R be Ring; :: thesis: for V being LeftMod of R

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

let V be LeftMod of R; :: thesis: for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

let v1, v2 be Vector of V; :: thesis: ( R = INT.Ring & V is Mult-cancelable implies ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) ) )

assume A1: ( R = INT.Ring & V is Mult-cancelable ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

thus ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) ) :: thesis: ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

( b <> 0. R & not b * v1 <> a * v2 ) or ( v1 <> v2 & {v1,v2} is linearly-independent ) )

assume A11: for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

A12: ( (1. R) * v2 = v2 & (1. R) * v1 = v1 ) by VECTSP_1:def 17;

hence v1 <> v2 by A11, A1; :: thesis: {v1,v2} is linearly-independent

let l be Linear_Combination of {v1,v2}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or 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, A1;

set x = the Element of Carrier l;

Carrier l c= {v1,v2} by VECTSP_6:def 4;

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. R ) ;

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

let V be LeftMod of R; :: thesis: for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

let v1, v2 be Vector of V; :: thesis: ( R = INT.Ring & V is Mult-cancelable implies ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) ) )

assume A1: ( R = INT.Ring & V is Mult-cancelable ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

thus ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) ) :: thesis: ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

assume A10:
v2 <> 0. V
; :: thesis: ( ex a, b being Element of R st
set N0 = 0. R;

set N1 = - (1. R);

deffunc H_{1}( Element of V) -> Element of the carrier of R = 0. R;

assume that

A2: v1 <> v2 and

A3: {v1,v2} is linearly-independent ; :: thesis: ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) )

thus v2 <> 0. V by A3, Th60, A1; :: thesis: for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2

let a, b be Element of R; :: thesis: ( b <> 0. R implies b * v1 <> a * v2 )

assume A4: b <> 0. R ; :: thesis: b * v1 <> a * v2

set Na = a;

set Nb = - b;

consider f being Function of V,R such that

A5: ( f . v1 = - b & f . v2 = a ) and

A6: for v being Element of V st v <> v1 & v <> v2 holds

f . v = H_{1}(v)
from FUNCT_2:sch 7(A2);

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;

Carrier f c= {v1,v2}

- b <> 0. R by A4, VECTSP_1:28;

then f . v1 <> 0. R by A5;

then A8: v1 in Carrier f ;

set w = a * v2;

assume A9: b * v1 = a * v2 ; :: thesis: contradiction

Sum f = ((- b) * v1) + (a * v2) by A2, A5, Th22

.= (b * (- v1)) + (a * v2) by ZMODUL01:5, A1

.= (- (a * v2)) + (a * v2) by A9, ZMODUL01:6, A1

.= - ((a * v2) - (a * v2)) by RLVECT_1:33

.= - (0. V) by RLVECT_1:15

.= 0. V by RLVECT_1:12 ;

then Carrier f = {} by VECTSP_7:def 1, A3;

hence contradiction by A8; :: thesis: verum

end;set N1 = - (1. R);

deffunc H

assume that

A2: v1 <> v2 and

A3: {v1,v2} is linearly-independent ; :: thesis: ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) )

thus v2 <> 0. V by A3, Th60, A1; :: thesis: for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2

let a, b be Element of R; :: thesis: ( b <> 0. R implies b * v1 <> a * v2 )

assume A4: b <> 0. R ; :: thesis: b * v1 <> a * v2

set Na = a;

set Nb = - b;

consider f being Function of V,R such that

A5: ( f . v1 = - b & f . v2 = a ) and

A6: for v being Element of V st v <> v1 & v <> v2 holds

f . v = H

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;

now :: thesis: for v being Vector of V st not v in {v1,v2} holds

f . v = 0. R

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;f . v = 0. R

let v be Vector of V; :: thesis: ( not v in {v1,v2} implies f . v = 0. R )

assume not v in {v1,v2} ; :: thesis: f . v = 0. R

then ( v <> v1 & v <> v2 ) by TARSKI:def 2;

hence f . v = 0. R by A6; :: thesis: verum

end;assume not v in {v1,v2} ; :: thesis: f . v = 0. R

then ( v <> v1 & v <> v2 ) by TARSKI:def 2;

hence f . v = 0. R by A6; :: thesis: verum

Carrier f c= {v1,v2}

proof

then reconsider f = f as Linear_Combination of {v1,v2} by VECTSP_6:def 4;
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. R ) ;

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;assume x in Carrier f ; :: thesis: x in {v1,v2}

then A7: ex u being Vector of V st

( x = u & f . u <> 0. R ) ;

assume not x in {v1,v2} ; :: thesis: contradiction

then ( x <> v1 & x <> v2 ) by TARSKI:def 2;

hence contradiction by A6, A7; :: thesis: verum

- b <> 0. R by A4, VECTSP_1:28;

then f . v1 <> 0. R by A5;

then A8: v1 in Carrier f ;

set w = a * v2;

assume A9: b * v1 = a * v2 ; :: thesis: contradiction

Sum f = ((- b) * v1) + (a * v2) by A2, A5, Th22

.= (b * (- v1)) + (a * v2) by ZMODUL01:5, A1

.= (- (a * v2)) + (a * v2) by A9, ZMODUL01:6, A1

.= - ((a * v2) - (a * v2)) by RLVECT_1:33

.= - (0. V) by RLVECT_1:15

.= 0. V by RLVECT_1:12 ;

then Carrier f = {} by VECTSP_7:def 1, A3;

hence contradiction by A8; :: thesis: verum

( b <> 0. R & not b * v1 <> a * v2 ) or ( v1 <> v2 & {v1,v2} is linearly-independent ) )

assume A11: for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

A12: ( (1. R) * v2 = v2 & (1. R) * v1 = v1 ) by VECTSP_1:def 17;

hence v1 <> v2 by A11, A1; :: thesis: {v1,v2} is linearly-independent

let l be Linear_Combination of {v1,v2}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or 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, A1;

set x = the Element of Carrier l;

Carrier l c= {v1,v2} by VECTSP_6:def 4;

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. R ) ;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( l . v1 <> 0. R or ( l . v2 <> 0. R & l . v1 = 0. R ) )
by A17, A16, TARSKI:def 2;

end;

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

(l . v1) * v1 =
- ((l . v2) * v2)
by A15, RLVECT_1:6

.= (- (1. R)) * ((l . v2) * v2) by ZMODUL01:2

.= ((- (1. R)) * (l . v2)) * v2 by VECTSP_1:def 16 ;

hence contradiction by A11, A18; :: thesis: verum

end;.= (- (1. R)) * ((l . v2) * v2) by ZMODUL01:2

.= ((- (1. R)) * (l . v2)) * v2 by VECTSP_1:def 16 ;

hence contradiction by A11, A18; :: thesis: verum