Proof of Elementary Properties of Linear Independence

Routine facts about nonempty segments are used without comment (Toolkit for AL2). We begin with the empty family. For $n=0$ the condition of Linearly Independent and Linearly Dependent Finite Families (i) asks that $\lambda_{i}=0$ for every $i\in[0]=\emptyset$, which holds for every $\lambda\in K^{0}$. So $v$ is linearly independent, which is (vi).

Next, let $v$ be linearly independent and $k:[m]\to[n]$ injective, and let $(\mu_{1},\dots,\mu_{m})\in K^{m}$ with $\sum_{l=1}^{m}\mu_{l}v_{k(l)}=0_{V}$. Define $\lambda\in K^{n}$ by $\lambda_{k(l)}=\mu_{l}$ for $l\in[m]$ and $\lambda_{i}=0$ for $i\notin k([m])$; this is well defined because $k$ is injective. Split $[n]$ into $k([m])$ and its complement $B$, a finite set (Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv)), by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (ii), and reindex the sum over the first part by the bijection $k:[m]\to k([m])$ (Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (iii)). On $B$ the coefficients $\lambda_{i}$ are $0$. The zero combinations $\sum_{i=1}^{n}0\,v_{i}$ and $\sum_{l=1}^{m}0\,v_{k(l)}$ are both $0_{V}$ (The Span of a Finite Family is the Smallest Subspace Containing It (i)); splitting the first in the same way shows that the part of the sum over $B$ is $0_{V}$. Hence

$$\sum_{i=1}^{n}\lambda_{i}v_{i}=\sum_{l=1}^{m}\mu_{l}v_{k(l)}=0_{V},$$

so every $\lambda_{i}=0$ by Linearly Independent and Linearly Dependent Finite Families (i), and in particular every $\mu_{l}=\lambda_{k(l)}=0$. This proves (i).

For (ii), let $v$ be linearly independent and $j\in[n]$. The one-term family $(v_{j})$, given by $k:[1]\to[n]$, $1\mapsto j$, is linearly independent by (i). Its linear combination with coefficient $1$ is $1v_{j}=v_{j}$ (a one-term sum is its term, by Iterated Operations over an Interval: Extracting One Term and Reversing the Order (i) with $n=0$ and Span of a Finite Family; Spanning Families (i); and Vector Space over a Field (vi)). If $v_{j}$ were $0_{V}$, independence would force $1=0$, contradicting Fields (i). So $v_{j}\neq0_{V}$.

For (iii), let $v$ be linearly independent and $w\notin\operatorname{span}(v_{1},\dots,v_{n})$. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii), a vanishing linear combination of $(v_{1},\dots,v_{n},w)$ reads

$$\sum_{i=1}^{n}\lambda_{i}v_{i}+\lambda_{n+1}w=0_{V}.$$

Suppose that $\lambda_{n+1}\neq0$, choose $\mu\in K$ with $\lambda_{n+1}\mu=1$ (Fields (i)), so that $\mu\lambda_{n+1}=1$ by commutativity, and put $c=-\mu$. Then $\lambda_{n+1}w=-\sum_{i=1}^{n}\lambda_{i}v_{i}$ by The Zero Vector, Negatives and Differences in a Vector Space (ii), so, by Vector Space over a Field (vi), Vector Space over a Field (v), Elementary Identities in a Vector Space (iv) and The Span of a Finite Family is the Smallest Subspace Containing It (i),

$$w=\mu(\lambda_{n+1}w)=c\sum_{i=1}^{n}\lambda_{i}v_{i}=\sum_{i=1}^{n}(c\lambda_{i})v_{i}\in\operatorname{span}(v_{1},\dots,v_{n}),$$

contrary to the choice of $w$. Hence $\lambda_{n+1}=0$, so $\lambda_{n+1}w=0w=0_{V}$ (Elementary Identities in a Vector Space (ii)) and $\sum_{i=1}^{n}\lambda_{i}v_{i}=0_{V}$, and every $\lambda_{i}=0$ by the independence of $v$. So the extended family is linearly independent.

For (iv), let $v$ be linearly dependent. The empty family is linearly independent by (vi), so $n\geq1$. For $j\in\{0,\dots,n\}$ let $(v_{1},\dots,v_{j})$ be the subfamily of $v$ given by the inclusion $[j]\to[n]$, as in (i). Let $j\in[n]$ be least such that $(v_{1},\dots,v_{j})$ is linearly dependent; it exists because $(v_{1},\dots,v_{n})=v$ is dependent. Then $(v_{1},\dots,v_{j-1})$ is linearly independent, by the minimality of $j$ if $j\geq2$ and by (vi) if $j=1$. The family $(v_{1},\dots,v_{j})$ is the extension of $(v_{1},\dots,v_{j-1})$ by $v_{j}$ (unique by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples (vi)); if $v_{j}$ lay outside $\operatorname{span}(v_{1},\dots,v_{j-1})$, (iii) would make it linearly independent, contrary to the choice of $j$. Hence $v_{j}\in\operatorname{span}(v_{1},\dots,v_{j-1})$, which proves (iv).

Finally, for (v), let $j\in[n]$ with $v_{j}\in\operatorname{span}(v^{(j)})$, and write (Span of a Finite Family; Spanning Families (ii))

$$v_{j}=\sum_{i=1}^{n-1}\mu_{i}v^{(j)}_{i}=\sum_{i=1}^{n-1}\mu_{i}v_{g_{j}(i)},$$

with $g_{j}$ the gap map of Bijections between Intervals: the Gap Map and the Reversal (i). The coefficients $\lambda_{j}=-1$ and $\lambda_{g_{j}(i)}=\mu_{i}$ for $i\in[n-1]$ give $\sum_{i=1}^{n}\lambda_{i}v_{i}=v_{j}+(-1)v_{j}=0_{V}$, by Iterated Operations over an Interval: Extracting One Term and Reversing the Order (i) (applied with $n-1$ in place of $n$) and Elementary Identities in a Vector Space (iv); and $\lambda_{j}\neq0$, as $0\neq1$ in $K$ (Fields (i)). So $v$ is linearly dependent (Linearly Independent and Linearly Dependent Finite Families (ii)), which is (v).