Proof of Elementary Properties of Linear Independence

Write (V$k$) for claim $k$ of Elementary Identities in a Vector Space, (F$k$) for claim $k$ of Properties of Finite Sums of Vectors, and (O$k$) for claim $k$ of Properties of the Order on the Natural Numbers. Field axioms are numbered as in Field; the conditions $1v=v$ and $\lambda(\mu v)=(\lambda\mu)v$ used below are among those of the definition of a vector space.

Claim 1. Let $j\in[n]$ and let $c\in K^{j}$ satisfy $\sum_{k=1}^{j}c_{k}v_{k}=0_{V}$, the components of $v|_{[j]}$ being $v_{k}$ for $k\in[j]$. Define $\tilde{c}\in K^{n}$ by $\tilde{c}_{k}=c_{k}$ for $k\in[j]$ and $\tilde{c}_{k}=0$ for every other $k\in[n]$, and let $u\in V^{n}$ have components $u_{k}=\tilde{c}_{k}v_{k}$. If $k\in[n]$ satisfies $j<k$, then $k\in[j]$ fails by (O3), so $u_{k}=0v_{k}=0_{V}$ by (V3). Hence A Finite Sum of Vectors with Vanishing Tail applies to $u$, and together with the restriction part of (F1),

Since $v$ is linearly independent, $\tilde{c}_{k}=0$ for every $k\in[n]$, so $c_{k}=0$ for every $k\in[j]$. Thus $v|_{[j]}$ is linearly independent.

Claim 2. Let $v$ be linearly independent.

Suppose $v_{1}=0_{V}$. By claim 1 the tuple $v|_{[1]}$ is linearly independent. Yet the map $c\in K^{1}$ with $c_{1}=1$ satisfies $\sum_{k=1}^{1}c_{k}v_{k}=1v_{1}=v_{1}=0_{V}$ by (F1), while $1\ne 0$ by field axiom 6. This contradicts independence, so $v_{1}\ne 0_{V}$.

Now let $m\in\mathbb{N}$ with $m+1\in[n]$. By (O4), (O6) and (O1) we have $1\le m$ and $m\le m+1\le n$, so $m\in[m+1]$ and $m\in[n]$; in particular both $v|_{[m]}$ and $v|_{[m+1]}$ are defined, the former being also the restriction of the latter to $[m]$, and $v|_{[m+1]}$ is linearly independent by claim 1.

Suppose $v_{m+1}\in\operatorname{span}(v|_{[m]})$, say

Define $c\in K^{m+1}$ by $c_{k}=d_{k}$ for $k\in[m]$ and $c_{m+1}=-1$, the additive inverse of $1$ in $K$. By the recursion and restriction parts of (F1), then (V5), then (V2),

If $-1=0$, then adding $1$ gives $0=1$, contradicting field axiom 6; so $c_{m+1}\ne 0$, contradicting the independence of $v|_{[m+1]}$. Hence $v_{m+1}\notin\operatorname{span}(v|_{[m]})$.

Claim 3. Since $v$ is not linearly independent, there are $c\in K^{n}$ with $\sum_{k=1}^{n}c_{k}v_{k}=0_{V}$ and an index $j\in[n]$ with $c_{j}\ne 0$. Let $b\in V^{n}$ have components $b_{k}=c_{k}v_{k}$, and let $b^{(j)}\in V^{p}$, $c^{(j)}\in K^{p}$ and $v^{(j)}\in V^{p}$ be obtained from $b$, $c$ and $v$ by omitting the $j$-th component as in Extraction of a Summand from a Finite Sum of Vectors. All three omissions use the same index shift, so $b^{(j)}_{k}=c^{(j)}_{k}v^{(j)}_{k}$ for every $k\in[p]$, and that lemma gives

Hence $c_{j}v_{j}=-w$ by (V2), and $-w=(-1)w$ by (V5). By field axiom 7 there is $\lambda=c_{j}^{-1}$ with $\lambda c_{j}=1$; put $\mu=\lambda\cdot(-1)\in K$. Then

the last equality by the homogeneity (F3) followed by the compatibility of scalar multiplication with multiplication in $K$. Therefore $v_{j}\in\operatorname{span}(v^{(j)})$.