A subspace of a finite-dimensional vector space $V$ is finite-dimensional (Alternative proof)

Question

I have looked at several proofs of the following theorem:

Let $W$ be a subspace of a finite-dimensional vector space $V$, then $W$ is finite-dimensional.

But all of them use a similar argument to prove it:

Proof. Let $dim(V)=n$. If $W =\{0\}$, then $W$ is finite-dimensional. Otherwhise, W contains a nonzero element $x_1$; so $\{x_1\}$ is a linearly independent set. Continuing in this way, choose $x_1,...,x_k$ in $W$ such that $\{x_1,...,x_k\}$ is linearly independet. Since no linearly independent subset of $V$ can contain more than $n$ elements, this process must stop at a stage where $k\leq n$ and $\{x_1,...,x_k\}$ is linearly independet but adjoining any other element of $W$ produces a linearly dependent set, this implies that $\{x_1,...,x_k\}$ generates $W$, and hence it is a basis for $W$.

I'm fine with this proof, but also I'm looking for a proof that doesn't use the argument of "continuing in this way a finite number of times" or "perform this algorithm", my first attempt was to prove the following inductively:

P(n) : If $W$ is a subspace of a n-dimensional vector space $V$, then $W$ is finite-dimensional.

but I'm not sure how to prove that $P(n)\rightarrow P(n+1)$.

EDIT: At this point, I can't use the fact that every vector space has a basis.

Answer 1

First, the base case $n = 0$ is very easy (and this is a usable base case, we don't even need to do $n = 1$). Next, as you say, if $W = 0$ then the statement is clear. Otherwise $W$ contains some nonzero vector $w$. Then $W/w$ is a subspace of the $(n-1)$-dimensional quotient $V/w$, so by the inductive hypothesis $W/w$ is finite-dimensional, hence has some basis. Let $w_1, \dots w_k \in W$ be any lift of this basis to $W$; then $\{ w, w_1, \dots w_k \}$ is a basis of $W$, so $W$ is also finite-dimensional.

(If the statement that $V/w$ is $(n-1)$-dimensional also needs proof, the easiest argument is to extend $\{ w \}$ to a basis of $V$. If you want to avoid that argument then I guess we can talk about that too.)