let F be Field; :: thesis: for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let V be VectSp of F; :: thesis: for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let A be Subset of V; :: thesis: for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let x be Element of V; :: thesis: ( x in Lin A & not x in A implies A \/ {x} is linearly-dependent )
assume that
A1: x in Lin A and
A2: not x in A ; :: thesis: A \/ {x} is linearly-dependent
per cases ( A is linearly-independent or A is linearly-dependent ) ;
suppose A3: A is linearly-independent ; :: thesis: A \/ {x} is linearly-dependent
x in [#] (Lin A) by A1;
then reconsider X = {x} as Subset of (Lin A) by SUBSET_1:41;
reconsider A9 = A as Basis of (Lin A) by A3, Th20;
reconsider B = A9 \/ X as Subset of (Lin A) ;
X misses A9
proof
assume X meets A9 ; :: thesis: contradiction
then ex y being object st
( y in X & y in A9 ) by XBOOLE_0:3;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;
then B is linearly-dependent by VECTSP_9:15;
hence A \/ {x} is linearly-dependent by VECTSP_9:12; :: thesis: verum
end;
suppose A is linearly-dependent ; :: thesis: A \/ {x} is linearly-dependent
hence A \/ {x} is linearly-dependent by VECTSP_7:1, XBOOLE_1:7; :: thesis: verum
end;
end;