Proof of The Steinitz Exchange Lemma

Routine facts about nonempty segments and equality of tuples are used without comment (Toolkit for AL2). The argument follows Axler (2.22): the vectors $u_{1},\dots,u_{m}$ are brought into the spanning family one at a time, each time pushing out one of the $w$'s.

For $k\in\{0,\dots,m\}$ let $P(k)$ be the statement: $k\leq n$, and there is a strictly increasing map $\sigma:[n-k]\to[n]$ (that is, $\sigma(l)<\sigma(l')$ whenever $l<l'$) such that the $n$-tuple

$$B_{k}=(u_{1},\dots,u_{k},w_{\sigma(1)},\dots,w_{\sigma(n-k)}),$$

whose $i$-th component is $u_{i}$ for $i\leq k$ and $w_{\sigma(i-k)}$ for $k<i\leq n$, spans $V$ (Span of a Finite Family; Spanning Families (iii)). We prove, by induction on $k\in\mathbb{N}_{0}$ (Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula (ii)), that $k\leq m$ implies $P(k)$. Since $P(m)$ includes $m\leq n$, this proves (i).

For $k=0$ we have $0\leq n$, and we take $\sigma=\mathrm{id}_{[n]}$, so that $B_{0}=(w_{1},\dots,w_{n})$, which spans $V$ by hypothesis.

For the induction step, let $k\in[m]$ and assume $P(k-1)$, with $\sigma:[n-k+1]\to[n]$. Adjoining $u_{k}$ gives the $(n+1)$-tuple

$$C=(u_{1},\dots,u_{k},w_{\sigma(1)},\dots,w_{\sigma(n-k+1)})\in V^{n+1}.$$

Removing its $k$-th component gives $C^{(k)}=B_{k-1}$, in the notation of Dropping a Redundant Vector Does Not Change the Span. Every component of $B_{k-1}$ is a component of $C$ and so lies in $\operatorname{span}(C)$; hence 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) give $V=\operatorname{span}(B_{k-1})\subseteq\operatorname{span}(C)$, and $C$ spans $V$.

The family $C$ is linearly dependent: its component $C_{k}=u_{k}$ lies in $V=\operatorname{span}(B_{k-1})=\operatorname{span}(C^{(k)})$, so Elementary Properties of Linear Independence (v) applies.

We next show that the vector to be removed is one of the $w$'s. By Elementary Properties of Linear Independence (iv) there is $j\in[n+1]$ with $C_{j}\in\operatorname{span}(C_{1},\dots,C_{j-1})$. Suppose that $j\leq k$. Then $u_{j}\in\operatorname{span}(u_{1},\dots,u_{j-1})$, and $(u_{1},\dots,u_{j-1})$ is the family of the other vectors of $(u_{1},\dots,u_{j})$, so $(u_{1},\dots,u_{j})$ is linearly dependent by Elementary Properties of Linear Independence (v); but it is linearly independent by Elementary Properties of Linear Independence (i), applied to the inclusion $[j]\to[m]$. Hence $k<j\leq n+1$; in particular $k\leq n$, and $C_{j}=w_{\sigma(j-k)}$.

We remove this vector. Since $C_{i}=C^{(j)}_{i}$ for $i<j$, 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) give

$$C_{j}\in\operatorname{span}(C_{1},\dots,C_{j-1})\subseteq\operatorname{span}(C^{(j)}),$$

so by Dropping a Redundant Vector Does Not Change the Span (i) and the fact that $C$ spans $V$, $\operatorname{span}(C^{(j)})=\operatorname{span}(C)=V$.

Finally, $C^{(j)}=(u_{1},\dots,u_{k},w_{\sigma'(1)},\dots,w_{\sigma'(n-k)})$ with $\sigma'=\sigma\circ g_{j-k}:[n-k]\to[n]$, where $g_{j-k}:[n-k]\to[n-k+1]$ is the gap map of Bijections between Intervals: the Gap Map and the Reversal (i); and $\sigma'$ is strictly increasing as a composite of strictly increasing maps. Taking $B_{k}=C^{(j)}$, together with $k\leq n$ shown above, this is $P(k)$, which completes the induction.