Proof of The Span of a Finite Family is the Smallest Subspace Containing It

Routine facts about tuples built termwise or with one distinguished component, and about nonempty segments, are used without comment (Toolkit for AL2). We first establish the four identities of (i). The first follows from Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (v), which combines the two sums term by term, together with $\lambda_{i}v_{i}+\mu_{i}v_{i}=(\lambda_{i}+\mu_{i})v_{i}$ (Vector Space over a Field (viii)). For the second, the map $x\mapsto cx$ on $V$ is additive by Vector Space over a Field (vii) and fixes $0_{V}$ by Elementary Identities in a Vector Space (iii), so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi) moves it inside the sum, and $c(\lambda_{i}v_{i})=(c\lambda_{i})v_{i}$ by Vector Space over a Field (v). For the third, $u-w=u+(-1)w$ by The Zero Vector, Negatives and Differences in a Vector Space (iii) and Elementary Identities in a Vector Space (iv), so the first two identities give

$$\sum_{i=1}^{n}\lambda_{i}v_{i}-\sum_{i=1}^{n}\mu_{i}v_{i}=\sum_{i=1}^{n}\lambda_{i}v_{i}+\sum_{i=1}^{n}(-\mu_{i})v_{i}=\sum_{i=1}^{n}(\lambda_{i}-\mu_{i})v_{i}.$$

For the fourth, each term is $0\,v_{i}=0_{V}$ by Elementary Identities in a Vector Space (ii), and a sum of zero vectors is $0_{V}$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi) for the constant map on $V$ with value $0_{V}$ (for $n=0$ this is Span of a Finite Family; Spanning Families (i)). This proves (i).

By the fourth identity, $0_{V}$ is a linear combination of $v$ and so lies in $\operatorname{span}(v_{1},\dots,v_{n})$; by the first two, sums and scalar multiples of linear combinations of $v$ are again linear combinations of $v$. So the span is a linear subspace of $V$ by Linear Subspaces (i).

Now let $j\in[n]$, so that $n\geq1$, and take the coefficients $\lambda_{j}=1$ and $\lambda_{i}=0$ for $i\neq j$. By Iterated Operations over an Interval: Extracting One Term and Reversing the Order (i), applied with $n-1$ in place of $n$ and with the gap map $g_{j}:[n-1]\to[n]$ of Bijections between Intervals: the Gap Map and the Reversal (i),

$$\sum_{i=1}^{n}\lambda_{i}v_{i}=\sum_{k=1}^{n-1}0\,v_{g_{j}(k)}+1v_{j}=0_{V}+v_{j}=v_{j},$$

where the second equality uses the fourth identity of (i) for the $(n-1)$-tuple $(v_{g_{j}(1)},\dots,v_{g_{j}(n-1)})$ and Vector Space over a Field (vi), and the third uses The Zero Vector, Negatives and Differences in a Vector Space (i). So $v_{j}\in\operatorname{span}(v_{1},\dots,v_{n})$, and with the previous paragraph this proves (ii).

For (iii), let $W$ be a linear subspace of $V$ containing every $v_{j}$, and let $(\lambda_{1},\dots,\lambda_{n})\in K^{n}$. Since $W$ contains $0_{V}$ and is closed under addition and scalar multiplication (Linear Subspaces (i)), each $\lambda_{i}v_{i}$ lies in $W$. We show by induction on $k\in\mathbb{N}_{0}$ (Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula (ii)) that, if $k\leq n$, the partial sum $\sum_{i=1}^{k}\lambda_{i}v_{i}$ lies in $W$. For $k=0$ it is $0_{V}$ by Span of a Finite Family; Spanning Families (i). If the claim holds for $k$ and $k+1\leq n$, then by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii)

$$\sum_{i=1}^{k+1}\lambda_{i}v_{i}=\sum_{i=1}^{k}\lambda_{i}v_{i}+\lambda_{k+1}v_{k+1},$$

a sum of two vectors of $W$, which lies in $W$. Taking $k=n$, every linear combination of $v$ lies in $W$, so $\operatorname{span}(v_{1},\dots,v_{n})\subseteq W$. This proves (iii).

Finally, if $n=0$, the set $K^{0}$ consists of the empty map alone (Tuples in a Set: the Set of n-Tuples and Their Components (ii)), and the corresponding sum is $0_{V}$ (Span of a Finite Family; Spanning Families (i)). So $\operatorname{span}(v_{1},\dots,v_{n})=\{0_{V}\}$, which is (iv).