[Math] Prove: In a finite dimensional vector space, every spanning set contains a basis.

linear algebraproof-verificationvector-spaces

The following quoted text is from Evar D. Nering's Linear Algebra and Matrix Theory, 2nd Ed.

Theorem 3.5. In a finite dimensional vector space, every spanning set
contains a basis.

Proof: Let $\mathcal{B}$ be a set spanning $\mathcal{V}$. If
$\mathcal{V}=\{0\}$, then $\emptyset\subset\mathcal{B}$ is a basis of
$\{0\}$. If $\mathcal{V}\ne\{0\}$ then $\mathcal{B}$ must contain at
least one non-zero vector $\alpha_{1}$. We now search for another
vector in $\mathcal{B}$ which is not dependent on $\{\alpha_{1}\}$. We
call this vector $\alpha_{2}$ and search for another vector in
$\mathcal{B}$ which is not dependent on the linearly independent set
$\{\alpha_{1},\alpha_{2}\}$. We continue in this way as long as we
can, but the process must terminate as we cannot find more than $n$
linearly independent vectors in $\mathcal{B}$. Thus suppose we have
obtained the set $\mathcal{A}=\{\alpha_{1},\dots,\alpha_{n}\}$ with
the property that every vector in $\mathcal{B}$ is linearly dependent
on $\mathcal{A}$. Then because of Theorem 2.1 the set $\mathcal{A}$
must also span $\mathcal{V}$ and it is a basis.

The reasoning in the proof seems circular. "Seek, and ye shall find." isn't very rigorous. I certainly believe that I could find such linearly independent vectors, but that's because I believe the theorem to be true.

Is the proof satisfactory?

I might be able to come up with my own proof, but I would still like to know if Nering's proof is satisfactory to mathematicians.

Best Answer

Yes, the proof is fine. You need not believe that you can find such linearly independent vectors. At each step, there either still exists another vector in $\mathcal B$ that is independent of what you already have (and then you can proceed), or there does not exist such a vector (and the process terminates). If you already know that a linearly independent set cannot have more than $\dim V$ elements, the process is doomed to terminate with some number $n\le \dim V$ vectors picked that way. By revisiting the termination condition, those $n$ vectors span $V$, hence must be a basis.