let V be Z_Module; 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; ( 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
; 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; ( v in A implies for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume
v in A
; 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; ( B = A \ {v} implies not v in Lin B )
assume A4:
B = A \ {v}
; 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
; 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
v <> 0. V
by A1, A2, ZMODUL02:56;
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; verum