Proof of Linear Maps Are Determined by Their Values on a Basis

Routine facts about tuples built termwise or with one distinguished component are used without comment (Toolkit for AL2). By Coordinates with Respect to a Basis (i), every $v\in V$ is $v=\sum_{i=1}^{n}a_{i}v_{i}$ for exactly one $(a_{1},\dots,a_{n})\in K^{n}$; we call these the coordinates of $v$.

Uniqueness comes first. If $T$ and $T'$ are linear maps from $V$ to $W$ with $Tv_{i}=T'v_{i}=w_{i}$ for every $i$, then Kernel and Image of a Linear Map Are Subspaces (i) gives, for every $v\in V$ with coordinates $(a_{1},\dots,a_{n})$,

$$Tv=\sum_{i=1}^{n}a_{i}\,Tv_{i}=\sum_{i=1}^{n}a_{i}w_{i}=\sum_{i=1}^{n}a_{i}\,T'v_{i}=T'v,$$

so $T=T'$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i)).

For existence, define $T:V\to W$ by

$$T\Bigl(\sum_{i=1}^{n}a_{i}v_{i}\Bigr)=\sum_{i=1}^{n}a_{i}w_{i}\qquad\bigl((a_{1},\dots,a_{n})\in K^{n}\bigr).$$

This is a map from $V$ to $W$ (Maps from Functional Predicative Relations, and Families of Sections (ii)): every $v\in V$ has coordinates, and the value is well defined because the coordinates are unique (Coordinates with Respect to a Basis (i)).

The map $T$ is linear. Let $u=\sum_{i}a_{i}v_{i}$ and $u'=\sum_{i}a'_{i}v_{i}$ be in $V$, and let $\lambda\in K$. By The Span of a Finite Family is the Smallest Subspace Containing It (i) in $V$, $u+u'=\sum_{i}(a_{i}+a'_{i})v_{i}$ and $\lambda u=\sum_{i}(\lambda a_{i})v_{i}$; so the definition of $T$ and The Span of a Finite Family is the Smallest Subspace Containing It (i) in $W$, for the family $(w_{1},\dots,w_{n})$, give

$$T(u+u')=\sum_{i}(a_{i}+a'_{i})w_{i}=Tu+Tu',\qquad T(\lambda u)=\sum_{i}(\lambda a_{i})w_{i}=\lambda\,Tu.$$

So $T$ is linear (Linear Maps, Linear Operators and Isomorphisms of Vector Spaces (i)).

Finally, $T$ takes the prescribed values. For $k\in[n]$, the coordinates of $v_{k}$ are $a_{k}=1$ and $a_{i}=0$ for $i\neq k$, since this linear combination equals $v_{k}$ by Iterated Operations over an Interval: Extracting One Term and Reversing the Order (i) (applied with $n-1$ in place of $n$), The Span of a Finite Family is the Smallest Subspace Containing It (i) and Vector Space over a Field (vi). The same computation in $W$ gives $Tv_{k}=\sum_{i}a_{i}w_{i}=w_{k}$. For $n=0$ there is nothing to check, and $T$ is the zero map on $V=\{0\}$ (The Span of a Finite Family is the Smallest Subspace Containing It (iv)). This proves (i).