Dropping a Redundant Vector from a Spanning Family

Let $K$ be a \reftext{def:field-c54-2026b}{field}, let $V$ be a \reftext{def:vector-space-2026a}{vector space over $K$}, and let $n$ be a \reftext{def:natural-numbers-2026a}{natural number}. Inequalities between natural numbers use the \reftext{def:order-natural-numbers-2026a}{order relations} on $\mathbb{N}$.

Let $v$ be a \reftext{def:finite-tuple-power-2026a}{tuple} in $V^{n+1}$ that \reftext{def:spanning-finite-family-2026a}{spans} $V$, let $j$ be a natural number with $j\le n+1$, and let $v^{(j)}$ be the tuple in $V^{n}$ obtained from $v$ by extracting the index $j$, as defined in \ref{lem:finite-sum-extraction-2026a}.

If $v_{j}$ lies in the \reftext{def:span-finite-family-2026b}{span} of $v^{(j)}$, then $v^{(j)}$ spans $V$.