Proof of Coordinates with Respect to a Basis

Routine facts about tuples built termwise and constant tuples are used without comment (Toolkit for AL2). Suppose first that $v$ is a basis (Finite Basis of a Vector Space (i)). Since $v$ spans $V$, every $u\in V$ is $\sum_{i=1}^{n}\lambda_{i}v_{i}$ for some $(\lambda_{1},\dots,\lambda_{n})\in K^{n}$ (Span of a Finite Family; Spanning Families (ii), Span of a Finite Family; Spanning Families (iii)). If also $u=\sum_{i=1}^{n}\mu_{i}v_{i}$, then by The Span of a Finite Family is the Smallest Subspace Containing It (i) and Elementary Identities in a Vector Space (vii)

$$\sum_{i=1}^{n}(\lambda_{i}-\mu_{i})v_{i}=\sum_{i=1}^{n}\lambda_{i}v_{i}-\sum_{i=1}^{n}\mu_{i}v_{i}=u-u=0_{V},$$

so the linear independence of $v$ gives $\lambda_{i}-\mu_{i}=0$, that is $\lambda_{i}=\mu_{i}$, for every $i$ (Linearly Independent and Linearly Dependent Finite Families (i)). So the coefficients exist and are unique.

Conversely, suppose that every $u\in V$ has exactly one such $n$-tuple of coefficients. Their existence for every $u$ says that $v$ spans $V$. If $\sum_{i=1}^{n}\lambda_{i}v_{i}=0_{V}$, then, since also $\sum_{i=1}^{n}0\,v_{i}=0_{V}$ by The Span of a Finite Family is the Smallest Subspace Containing It (i), uniqueness for $u=0_{V}$ gives $\lambda_{i}=0$ for every $i$; so $v$ is linearly independent. Hence $v$ is a basis, and this completes the proof of (i).