[proofplan]
We start with a spanning list $(v_1, \ldots, v_m)$ and iteratively inspect each vector: if removing $v_j$ still leaves a spanning list, we discard it; otherwise we keep it. The resulting sublist spans $V$ because every removal preserves spanning. It is linearly independent because any dependence relation among the retained vectors would allow one of them to be removed without losing spanning — contradicting the fact that it was kept.
[/proofplan]
[step:Define the reduction algorithm]
Let $(v_1, \ldots, v_m)$ be a list that spans $V$. We construct a decreasing sequence of sublists $S_0 \supset S_1 \supset \cdots \supset S_m$ as follows:
- $S_0 := (v_1, \ldots, v_m)$.
- For $j = 1, \ldots, m$: if $\operatorname{span}(S_{j-1} \setminus \{v_j\}) = V$, set $S_j := S_{j-1} \setminus \{v_j\}$ (discard $v_j$). Otherwise, set $S_j := S_{j-1}$ (keep $v_j$).
- The final sublist is $B := S_m$.
[/step]
[step:Verify that $B$ spans $V$]
We show by induction on $j$ that $\operatorname{span}(S_j) = V$ for every $j = 0, 1, \ldots, m$.
**Base case:** $\operatorname{span}(S_0) = \operatorname{span}(v_1, \ldots, v_m) = V$ by hypothesis.
**Inductive step:** Suppose $\operatorname{span}(S_{j-1}) = V$. If $v_j$ is discarded, then $S_j = S_{j-1} \setminus \{v_j\}$ and the algorithm only performs this removal when $\operatorname{span}(S_{j-1} \setminus \{v_j\}) = V$, so $\operatorname{span}(S_j) = V$. If $v_j$ is kept, then $S_j = S_{j-1}$, and $\operatorname{span}(S_j) = \operatorname{span}(S_{j-1}) = V$.
In particular, $\operatorname{span}(B) = \operatorname{span}(S_m) = V$.
[/step]
[step:Show that $B$ is linearly independent]
Suppose for contradiction that $B$ is linearly dependent. By the [Equivalent Characterization of Dependence](/theorems/3260) (implication $(1) \implies (2)$), there exists some $v_k \in B$ that lies in the span of the remaining vectors in $B$, i.e.,
\begin{align*}
v_k \in \operatorname{span}(B \setminus \{v_k\}).
\end{align*}
This means $\operatorname{span}(B \setminus \{v_k\}) = \operatorname{span}(B) = V$. We trace back to the algorithm's decision at stage $k$. At that stage, the algorithm inspected $v_k$ within the list $S_{k-1}$. Since $B \subset S_{k-1}$ (later stages only remove vectors, never add them), we have
\begin{align*}
V = \operatorname{span}(B \setminus \{v_k\}) \subset \operatorname{span}(S_{k-1} \setminus \{v_k\}) \subset V,
\end{align*}
so $\operatorname{span}(S_{k-1} \setminus \{v_k\}) = V$. But then the algorithm would have discarded $v_k$ at stage $k$, and $v_k$ would not be in $B$. This contradicts $v_k \in B$.
Therefore $B$ is linearly independent.
[guided]
The key question is: why can't the retained vectors have a nontrivial dependence relation among them? The answer lies in the contrapositive of the algorithm's retention criterion.
A vector $v_k$ is kept (retained in $B$) precisely when $\operatorname{span}(S_{k-1} \setminus \{v_k\}) \neq V$, i.e., removing $v_k$ from the list at stage $k$ would cause the list to lose spanning. If the final list $B$ were linearly dependent, the [Equivalent Characterization of Dependence](/theorems/3260) would give us a vector $v_k \in B$ expressible as a linear combination of the other vectors in $B$:
\begin{align*}
v_k = \sum_{\substack{v_i \in B \\ i \neq k}} c_i \, v_i.
\end{align*}
This would mean $\operatorname{span}(B \setminus \{v_k\}) = \operatorname{span}(B) = V$. Now, since $B \subset S_{k-1}$ (the algorithm only removes vectors in later stages, so every vector surviving to $B$ was present at stage $k$), we have $B \setminus \{v_k\} \subset S_{k-1} \setminus \{v_k\}$, and hence
\begin{align*}
V = \operatorname{span}(B \setminus \{v_k\}) \subset \operatorname{span}(S_{k-1} \setminus \{v_k\}) \subset V.
\end{align*}
So $\operatorname{span}(S_{k-1} \setminus \{v_k\}) = V$. But the algorithm checks this exact condition at stage $k$ and discards $v_k$ when it holds. Since $v_k \in B$, the algorithm did not discard it, meaning $\operatorname{span}(S_{k-1} \setminus \{v_k\}) \neq V$ — a contradiction.
The contradiction shows that no such $v_k$ can exist, so $B$ is linearly independent. The essential insight is that the algorithm's greedy retention rule — keep a vector only when it is indispensable for spanning — automatically prevents any dependence among the kept vectors.
[/guided]
[/step]
[step:Conclude that $B$ is a basis obtained by removing elements from the original list]
The sublist $B = S_m$ spans $V$ (by the second step) and is linearly independent (by the third step), so $B$ is a basis of $V$. By construction, $B$ is a subset of the original list $(v_1, \ldots, v_m)$: at each stage we either keep or remove a vector, never introducing new ones. Therefore $B$ is obtained from $(v_1, \ldots, v_m)$ by removing elements.
By the [Independent Lists Cannot Exceed Spanning Lists in Size](/theorems/3262), $|B| = \dim V \le m$, confirming that the reduction always produces a basis of the correct size.
[/step]
