let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let V be finite-dimensional VectSp of F; :: thesis: for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let W1, W2 be Subspace of V; :: thesis: ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k) )
assume A1: W1 is Subspace of W2 ; :: thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let k be Nat; :: thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 implies for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k) )
assume that
A2: (dim W1) + 1 = k and
A3: dim W2 = k + 1 ; :: thesis: for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let v be Vector of V; :: thesis: ( v in W2 & not v in W1 implies W1 + (Lin {v}) in pencil (W1,W2,k) )
assume that
A4: v in W2 and
A5: not v in W1 ; :: thesis: W1 + (Lin {v}) in pencil (W1,W2,k)
set W = W1 + (Lin {v});
A6: dim (W1 + (Lin {v})) = k by A2, A5, Th13;
then A7: W1 + (Lin {v}) in k Subspaces_of V by VECTSP_9:def 2;
v in the carrier of W2 by A4;
then {v} c= the carrier of W2 by ZFMISC_1:31;
then Lin {v} is Subspace of W2 by VECTSP_9:16;
then ( W1 is Subspace of W1 + (Lin {v}) & W1 + (Lin {v}) is Subspace of W2 ) by A1, VECTSP_5:7, VECTSP_5:34;
then A8: W1 + (Lin {v}) in segment (W1,W2) by A1, Def1;
dim ((Omega). W2) = k + 1 by A3, VECTSP_9:27;
then A9: W1 + (Lin {v}) <> (Omega). W2 by A6;
(dim ((Omega). W1)) + 1 = k by A2, VECTSP_9:27;
then W1 + (Lin {v}) <> (Omega). W1 by A6;
then not W1 + (Lin {v}) in {((Omega). W1),((Omega). W2)} by A9, TARSKI:def 2;
then W1 + (Lin {v}) in pencil (W1,W2) by A8, XBOOLE_0:def 5;
hence W1 + (Lin {v}) in pencil (W1,W2,k) by A7, XBOOLE_0:def 4; :: thesis: verum