Proof of A Finite Spanning Family Contains a Basis

Routine facts about equality of tuples are used without comment (Toolkit for AL2). We prove the claim by induction on $n\in\mathbb{N}_{0}$ (Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula (ii)), for all spanning $n$-tuples at once: the statement proved for $n$ is that (i) holds for every $n$-tuple in $V$ that spans $V$. In both the base case and the induction step, a spanning family $v$ that is linearly independent is itself a basis (Finite Basis of a Vector Space (i)), and we may take $m=n$ and $k=\mathrm{id}_{[n]}$.

For $n=0$ this always applies: the empty family is linearly independent by Elementary Properties of Linear Independence (vi), so, as it spans $V$, it is a basis, and we take $m=0$ and $k$ the empty map.

For the induction step, assume the claim for $n$, and let $v\in V^{n+1}$ span $V$. By the remark above we may assume that $v$ is linearly dependent. Then Elementary Properties of Linear Independence (iv) gives $j\in[n+1]$ with $v_{j}\in\operatorname{span}(v_{1},\dots,v_{j-1})$. Let $v^{(j)}$ be the $n$-tuple of the other vectors of $v$, as in Dropping a Redundant Vector Does Not Change the Span. For $i<j$ we have $g_{j}(i)=i$ (Bijections between Intervals: the Gap Map and the Reversal (i)), so $v_{i}=v^{(j)}_{i}$; hence $\operatorname{span}(v_{1},\dots,v_{j-1})\subseteq\operatorname{span}(v^{(j)})$ by The Span of a Finite Family is the Smallest Subspace Containing It (ii) and The Span of a Finite Family is the Smallest Subspace Containing It (iii). Therefore $v_{j}\in\operatorname{span}(v^{(j)})$, and by Dropping a Redundant Vector Does Not Change the Span (i) the $n$-tuple $v^{(j)}$ spans $V$.

The induction hypothesis, applied to $v^{(j)}$, gives $m\leq n$ and a map $k':[m]\to[n]$, strictly increasing in the sense of (i), such that $(v^{(j)}_{k'(1)},\dots,v^{(j)}_{k'(m)})$ is a basis of $V$. Put $k=g_{j}\circ k':[m]\to[n+1]$. It is strictly increasing because $g_{j}$ is, by its definition in Bijections between Intervals: the Gap Map and the Reversal (i), and $v_{k(l)}=v^{(j)}_{k'(l)}$ for every $l\in[m]$, so $(v_{k(1)},\dots,v_{k(m)})$ is that same basis; and $m\leq n+1$. This completes the induction and proves (i).