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

for A being finite Subset of V holds

( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

let V be LeftMod of K; :: thesis: for A being finite Subset of V holds

( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

let A be finite Subset of V; :: thesis: ( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} ; :: thesis: A is linearly-independent

for L being Linear_Combination of A st Sum L = 0. V holds

Carrier L = {}

for A being finite Subset of V holds

( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

let V be LeftMod of K; :: thesis: for A being finite Subset of V holds

( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

let A be finite Subset of V; :: thesis: ( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} )

hereby :: thesis: ( ( for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} ) implies A is linearly-independent )

assume AS:
for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} ) implies A is linearly-independent )

assume BS:
A is linearly-independent
; :: thesis: for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {}

let L be Linear_Combination of A; :: thesis: ( ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) implies Carrier L = {} )

given F being FinSequence of the carrier of V such that BS2: ( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) ; :: thesis: Carrier L = {}

reconsider B = Carrier L as finite Subset of V ;

set F0 = canFS B;

BS3: rng (canFS B) = B by FUNCT_2:def 3;

rng (canFS B) c= the carrier of V by TARSKI:def 3;

then reconsider F0 = canFS B as FinSequence of the carrier of V by FINSEQ_1:def 4;

reconsider C = A \ B as finite Subset of V ;

set G0 = canFS C;

BS4: rng (canFS C) = C by FUNCT_2:def 3;

rng (canFS C) c= the carrier of V by TARSKI:def 3;

then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;

BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by BS3, FUNCT_2:def 3

.= (B /\ A) \ B by XBOOLE_1:49

.= {} by XBOOLE_1:37, XBOOLE_1:17 ;

then BS6: F0 ^ G0 is one-to-one by LMBASE2A;

BS7: rng (F0 ^ G0) = B \/ (A \ B) by BS3, BS4, BS5, LMBASE2A

.= A \/ B by XBOOLE_1:39

.= A by VECTSP_6:def 4, XBOOLE_1:12 ;

(rng G0) /\ (Carrier L) = {} by BS5, FUNCT_2:def 3;

then BS10: L (#) G0 = (dom G0) --> (0. V) by LMBASE2C;

then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;

BS12: Sum (L (#) F) = Sum (L (#) (F0 ^ G0)) by EQSUMLF, BS6, BS7, BS2

.= Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13

.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41

.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa

.= Sum (L (#) F0) ;

Sum L = 0. V by BS2, BS3, BS12, VECTSP_6:def 6;

hence Carrier L = {} by VECTSP_7:def 1, BS; :: thesis: verum

end;( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {}

let L be Linear_Combination of A; :: thesis: ( ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) implies Carrier L = {} )

given F being FinSequence of the carrier of V such that BS2: ( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) ; :: thesis: Carrier L = {}

reconsider B = Carrier L as finite Subset of V ;

set F0 = canFS B;

BS3: rng (canFS B) = B by FUNCT_2:def 3;

rng (canFS B) c= the carrier of V by TARSKI:def 3;

then reconsider F0 = canFS B as FinSequence of the carrier of V by FINSEQ_1:def 4;

reconsider C = A \ B as finite Subset of V ;

set G0 = canFS C;

BS4: rng (canFS C) = C by FUNCT_2:def 3;

rng (canFS C) c= the carrier of V by TARSKI:def 3;

then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;

BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by BS3, FUNCT_2:def 3

.= (B /\ A) \ B by XBOOLE_1:49

.= {} by XBOOLE_1:37, XBOOLE_1:17 ;

then BS6: F0 ^ G0 is one-to-one by LMBASE2A;

BS7: rng (F0 ^ G0) = B \/ (A \ B) by BS3, BS4, BS5, LMBASE2A

.= A \/ B by XBOOLE_1:39

.= A by VECTSP_6:def 4, XBOOLE_1:12 ;

(rng G0) /\ (Carrier L) = {} by BS5, FUNCT_2:def 3;

then BS10: L (#) G0 = (dom G0) --> (0. V) by LMBASE2C;

then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;

BS12: Sum (L (#) F) = Sum (L (#) (F0 ^ G0)) by EQSUMLF, BS6, BS7, BS2

.= Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13

.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41

.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa

.= Sum (L (#) F0) ;

Sum L = 0. V by BS2, BS3, BS12, VECTSP_6:def 6;

hence Carrier L = {} by VECTSP_7:def 1, BS; :: thesis: verum

( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds

Carrier L = {} ; :: thesis: A is linearly-independent

for L being Linear_Combination of A st Sum L = 0. V holds

Carrier L = {}

proof

hence
A is linearly-independent
by VECTSP_7:def 1; :: thesis: verum
let L be Linear_Combination of A; :: thesis: ( Sum L = 0. V implies Carrier L = {} )

assume BS: Sum L = 0. V ; :: thesis: Carrier L = {}

consider F0 being FinSequence of the carrier of V such that

P3: ( F0 is one-to-one & rng F0 = Carrier L & Sum L = Sum (L (#) F0) ) by VECTSP_6:def 6;

reconsider B = Carrier L as finite Subset of V ;

reconsider C = A \ B as finite Subset of V ;

set G0 = canFS C;

BS4: rng (canFS C) = C by FUNCT_2:def 3;

rng (canFS C) c= the carrier of V by TARSKI:def 3;

then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;

set F = F0 ^ G0;

BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by P3, FUNCT_2:def 3

.= (B /\ A) \ B by XBOOLE_1:49

.= {} by XBOOLE_1:37, XBOOLE_1:17 ;

then BS6: F0 ^ G0 is one-to-one by LMBASE2A, P3;

BS7: rng (F0 ^ G0) = B \/ (A \ B) by P3, BS4, BS5, LMBASE2A

.= A \/ B by XBOOLE_1:39

.= A by VECTSP_6:def 4, XBOOLE_1:12 ;

BS10: L (#) G0 = (dom G0) --> (0. V) by BS5, P3, LMBASE2C;

then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;

Sum (L (#) (F0 ^ G0)) = Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13

.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41

.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa

.= Sum (L (#) F0) ;

hence Carrier L = {} by AS, BS, BS6, BS7, P3; :: thesis: verum

end;assume BS: Sum L = 0. V ; :: thesis: Carrier L = {}

consider F0 being FinSequence of the carrier of V such that

P3: ( F0 is one-to-one & rng F0 = Carrier L & Sum L = Sum (L (#) F0) ) by VECTSP_6:def 6;

reconsider B = Carrier L as finite Subset of V ;

reconsider C = A \ B as finite Subset of V ;

set G0 = canFS C;

BS4: rng (canFS C) = C by FUNCT_2:def 3;

rng (canFS C) c= the carrier of V by TARSKI:def 3;

then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;

set F = F0 ^ G0;

BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by P3, FUNCT_2:def 3

.= (B /\ A) \ B by XBOOLE_1:49

.= {} by XBOOLE_1:37, XBOOLE_1:17 ;

then BS6: F0 ^ G0 is one-to-one by LMBASE2A, P3;

BS7: rng (F0 ^ G0) = B \/ (A \ B) by P3, BS4, BS5, LMBASE2A

.= A \/ B by XBOOLE_1:39

.= A by VECTSP_6:def 4, XBOOLE_1:12 ;

BS10: L (#) G0 = (dom G0) --> (0. V) by BS5, P3, LMBASE2C;

then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;

Sum (L (#) (F0 ^ G0)) = Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13

.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41

.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa

.= Sum (L (#) F0) ;

hence Carrier L = {} by AS, BS, BS6, BS7, P3; :: thesis: verum