let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let V be finite-dimensional VectSp of F; :: thesis: for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let W be Subspace of V; :: thesis: for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let v be Vector of V; :: thesis: ( not v in W implies dim (W + (Lin {v})) = (dim W) + 1 )
assume A1: not v in W ; :: thesis: dim (W + (Lin {v})) = (dim W) + 1
the carrier of ((Omega). (W /\ (Lin {v}))) = {(0. (W /\ (Lin {v})))}

proof

thus the carrier of ((Omega). (W /\ (Lin {v}))) c= {(0. (W /\ (Lin {v})))} :: according to XBOOLE_0:def 10 :: thesis: {(0. (W /\ (Lin {v})))} c= the carrier of ((Omega). (W /\ (Lin {v})))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of ((Omega). (W /\ (Lin {v}))) or a in {(0. (W /\ (Lin {v})))} )
assume a in the carrier of ((Omega). (W /\ (Lin {v}))) ; :: thesis: a in {(0. (W /\ (Lin {v})))}
then A2: a in the carrier of W /\ the carrier of (Lin {v}) by VECTSP_5:def 2;
then a in the carrier of (Lin {v}) by XBOOLE_0:def 4;
then a in Lin {v} ;
then consider e being Element of F such that
A3: a = e * v by VECTSP10:3;
a in the carrier of W by A2, XBOOLE_0:def 4;
then A4: a in W ;

now :: thesis: not e <> 0. F

assume e <> 0. F ; :: thesis: contradiction
then v = (e ") * (e * v) by VECTSP_1:20;
hence contradiction by A1, A4, A3, VECTSP_4:21; :: thesis: verum

end;

then a = 0. V by A3, VECTSP_1:14;
then a = 0. (W /\ (Lin {v})) by VECTSP_4:11;
hence a in {(0. (W /\ (Lin {v})))} by TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(0. (W /\ (Lin {v})))} or a in the carrier of ((Omega). (W /\ (Lin {v}))) )
assume a in {(0. (W /\ (Lin {v})))} ; :: thesis: a in the carrier of ((Omega). (W /\ (Lin {v})))
then a = 0. (W /\ (Lin {v})) by TARSKI:def 1;
then a = 0. V by VECTSP_4:11;
then a in W /\ (Lin {v}) by VECTSP_4:17;
hence a in the carrier of ((Omega). (W /\ (Lin {v}))) ; :: thesis: verum

end;

then (Omega). (W /\ (Lin {v})) = (0). (W /\ (Lin {v})) by VECTSP_4:def 3;
then A5: dim (W /\ (Lin {v})) = 0 by VECTSP_9:29;
A6: (dim (W + (Lin {v}))) + (dim (W /\ (Lin {v}))) = (dim W) + (dim (Lin {v})) by VECTSP_9:32;
v <> 0. V by A1, VECTSP_4:17;
hence dim (W + (Lin {v})) = (dim W) + 1 by A5, A6, Th12; :: thesis: verum