let V be Z_Module; :: thesis: for A being Subset of V st A is linearly-independent holds

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

let A be Subset of V; :: thesis: ( A is linearly-independent implies for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B )

assume A1: A is linearly-independent ; :: thesis: for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

let v be Vector of V; :: thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds

not v in Lin B )

assume v in A ; :: thesis: for B being Subset of V st B = A \ {v} holds

not v in Lin B

then A2: {v} is Subset of A by SUBSET_1:41;

v in {v} by TARSKI:def 1;

then v in Lin {v} by ZMODUL02:65;

then consider K being Linear_Combination of {v} such that

A3: v = Sum K by ZMODUL02:64;

let B be Subset of V; :: thesis: ( B = A \ {v} implies not v in Lin B )

assume A4: B = A \ {v} ; :: thesis: not v in Lin B

B c= A by A4, XBOOLE_1:36;

then A5: B \/ {v} c= A \/ A by A2, XBOOLE_1:13;

assume v in Lin B ; :: thesis: contradiction

then consider L being Linear_Combination of B such that

A6: v = Sum L by ZMODUL02:64;

A7: ( Carrier L c= B & Carrier K c= {v} ) by VECTSP_6:def 4;

then (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13;

then ( Carrier (L - K) c= (Carrier L) \/ (Carrier K) & (Carrier L) \/ (Carrier K) c= A ) by A5, ZMODUL02:40;

then A8: L - K is Linear_Combination of A by XBOOLE_1:1, VECTSP_6:def 4;

A9: for x being Vector of V st x in Carrier L holds

K . x = 0

then not Carrier L is empty by A6, ZMODUL02:23;

then ex w being object st w in Carrier L by XBOOLE_0:def 1;

then A14: not Carrier (L - K) is empty by A10;

0. V = (Sum L) + (- (Sum K)) by A6, A3, RLVECT_1:5

.= (Sum L) + (Sum (- K)) by ZMODUL02:54

.= Sum (L - K) by ZMODUL02:52 ;

hence contradiction by A1, A8, A14; :: thesis: verum

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

let A be Subset of V; :: thesis: ( A is linearly-independent implies for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B )

assume A1: A is linearly-independent ; :: thesis: for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

let v be Vector of V; :: thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds

not v in Lin B )

assume v in A ; :: thesis: for B being Subset of V st B = A \ {v} holds

not v in Lin B

then A2: {v} is Subset of A by SUBSET_1:41;

v in {v} by TARSKI:def 1;

then v in Lin {v} by ZMODUL02:65;

then consider K being Linear_Combination of {v} such that

A3: v = Sum K by ZMODUL02:64;

let B be Subset of V; :: thesis: ( B = A \ {v} implies not v in Lin B )

assume A4: B = A \ {v} ; :: thesis: not v in Lin B

B c= A by A4, XBOOLE_1:36;

then A5: B \/ {v} c= A \/ A by A2, XBOOLE_1:13;

assume v in Lin B ; :: thesis: contradiction

then consider L being Linear_Combination of B such that

A6: v = Sum L by ZMODUL02:64;

A7: ( Carrier L c= B & Carrier K c= {v} ) by VECTSP_6:def 4;

then (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13;

then ( Carrier (L - K) c= (Carrier L) \/ (Carrier K) & (Carrier L) \/ (Carrier K) c= A ) by A5, ZMODUL02:40;

then A8: L - K is Linear_Combination of A by XBOOLE_1:1, VECTSP_6:def 4;

A9: for x being Vector of V st x in Carrier L holds

K . x = 0

proof

let x be Vector of V; :: thesis: ( x in Carrier L implies K . x = 0 )

assume x in Carrier L ; :: thesis: K . x = 0

then not x in Carrier K by A4, A7, XBOOLE_0:def 5;

hence K . x = 0 ; :: thesis: verum

end;assume x in Carrier L ; :: thesis: K . x = 0

then not x in Carrier K by A4, A7, XBOOLE_0:def 5;

hence K . x = 0 ; :: thesis: verum

A10: now :: thesis: for x being set st x in Carrier L holds

x in Carrier (L - K)

v <> 0. V
by A1, A2, ZMODUL02:56;x in Carrier (L - K)

let x be set ; :: thesis: ( x in Carrier L implies x in Carrier (L - K) )

assume that

A11: x in Carrier L and

A12: not x in Carrier (L - K) ; :: thesis: contradiction

reconsider x = x as Vector of V by A11;

A13: L . x <> 0 by A11, ZMODUL02:8;

(L - K) . x = (L . x) - (K . x) by ZMODUL02:39

.= (L . x) - (0. INT.Ring) by A9, A11

.= L . x ;

hence contradiction by A12, A13; :: thesis: verum

end;assume that

A11: x in Carrier L and

A12: not x in Carrier (L - K) ; :: thesis: contradiction

reconsider x = x as Vector of V by A11;

A13: L . x <> 0 by A11, ZMODUL02:8;

(L - K) . x = (L . x) - (K . x) by ZMODUL02:39

.= (L . x) - (0. INT.Ring) by A9, A11

.= L . x ;

hence contradiction by A12, A13; :: thesis: verum

then not Carrier L is empty by A6, ZMODUL02:23;

then ex w being object st w in Carrier L by XBOOLE_0:def 1;

then A14: not Carrier (L - K) is empty by A10;

0. V = (Sum L) + (- (Sum K)) by A6, A3, RLVECT_1:5

.= (Sum L) + (Sum (- K)) by ZMODUL02:54

.= Sum (L - K) by ZMODUL02:52 ;

hence contradiction by A1, A8, A14; :: thesis: verum