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 for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds

( a = 0. R & b = 0. R ) )

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 for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds

( a = 0. R & b = 0. R ) )

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

( a = 0. R & b = 0. R ) ) )

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

( a = 0. R & b = 0. R ) )

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

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

( a = 0. R & b = 0. R ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

( a = 0. R & b = 0. R ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

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

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

( a = 0. R & b = 0. R ) )

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 for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds

( a = 0. R & b = 0. R ) )

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

( a = 0. R & b = 0. R ) ) )

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

( a = 0. R & b = 0. R ) )

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

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

( a = 0. R & b = 0. R ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

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

( a = 0. R & b = 0. R )

let a, b be Element of R; :: thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0. R & b = 0. R ) )

assume that

A3: (a * v1) + (b * v2) = 0. V and

A4: ( a <> 0. R or b <> 0. R ) ; :: thesis: contradiction

end;( a = 0. R & b = 0. R )

let a, b be Element of R; :: thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0. R & b = 0. R ) )

assume that

A3: (a * v1) + (b * v2) = 0. V and

A4: ( a <> 0. R or b <> 0. R ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( a <> 0. R or b <> 0. R )
by A4;

end;

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

a * v1 =
- (b * v2)
by A3, RLVECT_1:6

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

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

hence contradiction by A1, A2, A5, Th62; :: thesis: verum

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

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

hence contradiction by A1, A2, A5, Th62; :: thesis: verum

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

b * v2 =
- (a * v1)
by A3, RLVECT_1:6

.= (- (1. R)) * (a * v1) by ZMODUL01:2

.= ((- (1. R)) * a) * v1 by VECTSP_1:def 16 ;

hence contradiction by A1, A2, A6, Th62; :: thesis: verum

end;.= (- (1. R)) * (a * v1) by ZMODUL01:2

.= ((- (1. R)) * a) * v1 by VECTSP_1:def 16 ;

hence contradiction by A1, A2, A6, Th62; :: thesis: verum

( a = 0. R & b = 0. R ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

A8: now :: thesis: for a, b being Element of R st b <> 0. R holds

not b * v1 = a * v2

not b * v1 = a * v2

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

assume A9: b <> 0. R ; :: 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 A1, ZMODUL01:6

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

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

end;assume A9: b <> 0. R ; :: 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 A1, ZMODUL01:6

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

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

now :: thesis: not v2 = 0. V

hence
( v1 <> v2 & {v1,v2} is linearly-independent )
by A8, A1, Th62; :: thesis: verumassume A10:
v2 = 0. V
; :: thesis: contradiction

0. V = (0. V) + (0. V) by RLVECT_1:4

.= ((0. R) * v1) + (0. V) by ZMODUL01:1, A1

.= ((0. R) * v1) + ((1. R) * v2) by A1, A10, ZMODUL01:1 ;

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

end;0. V = (0. V) + (0. V) by RLVECT_1:4

.= ((0. R) * v1) + (0. V) by ZMODUL01:1, A1

.= ((0. R) * v1) + ((1. R) * v2) by A1, A10, ZMODUL01:1 ;

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