Proof of Real Matrices and Linear Maps between Euclidean Spaces

Routine facts about $\mathbb{R}^{n}$ as a real vector space and about subspaces with the restricted operations are used without comment (Toolkit for AL3). The clauses are proved in order, each using the earlier ones.

Let $A\in\mathcal{M}_{m\times n}(\mathbb{R})$. For $x,y\in\mathbb{R}^{n}$ and $s\in\mathbb{R}$, Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (v) gives

$$A(x+y)=Ax+Ay,\qquad A(sx)=s(Ax),$$

and these are the two conditions of Linear Maps, Linear Operators and Isomorphisms of Vector Spaces (i) for $L_{A}$. This proves (i).

Since $L_{A}$ is linear, Kernel and Image of a Linear Map Are Subspaces (ii) shows that $\ker L_{A}$ is a linear subspace of $\mathbb{R}^{n}$ and $\operatorname{im}L_{A}$ one of $\mathbb{R}^{m}$. The space $\mathbb{R}^{m}$ is finite-dimensional by Properties of Dimension (vi), and therefore so is its subspace $\operatorname{im}L_{A}$, which is a vector space with the restricted operations (Linear Subspaces Are Vector Spaces; Intersections (i)), by Properties of Dimension (v). This proves (ii).

For the existence in (iii), let $T$ be a linear map from $\mathbb{R}^{n}$ to $\mathbb{R}^{m}$, and let $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ be the matrix with entries $A_{ij}=(Te_{j})_{i}$ (the map $(i,j)\mapsto(Te_{j})_{i}$ on $[m]\times[n]$ exists by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v) and is a matrix by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i)). By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (vi),

$$(Ae_{j})_{i}=A_{ij}=(Te_{j})_{i}\qquad(i\in[m],\ j\in[n]),$$

so $L_{A}e_{j}=Te_{j}$ for every $j\in[n]$. Now $T$ is linear by assumption and $L_{A}$ is linear by (i), and $(e_{1},\dots,e_{n})$ is a basis of $\mathbb{R}^{n}$ by Properties of Dimension (vi). By the uniqueness part of Linear Maps Are Determined by Their Values on a Basis (i), applied with the values $w_{j}=Te_{j}$, only one linear map from $\mathbb{R}^{n}$ to $\mathbb{R}^{m}$ takes each $e_{j}$ to $Te_{j}$; hence $T=L_{A}$.

For the uniqueness, suppose that also $T=L_{B}$ with $B\in\mathcal{M}_{m\times n}(\mathbb{R})$. Then $Be_{j}=Te_{j}$ for every $j\in[n]$, so Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (vi) gives $B_{ij}=(Be_{j})_{i}=(Te_{j})_{i}=A_{ij}$ for all $i$ and $j$, and $B=A$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii). In particular every matrix representing $T$ has the displayed entries, which completes the proof of (iii).

For (iv), let $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ and $B\in\mathcal{M}_{n\times p}(\mathbb{R})$. For every $z\in\mathbb{R}^{p}$, Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (v) gives $(AB)z=A(Bz)$, that is,

$$L_{AB}z=L_{A}(L_{B}z),$$

and the right-hand side is the value at $z$ of the composite $L_{A}L_{B}$ (both maps linear by (i)) of Operations on Linear Maps (iv). So $L_{AB}=L_{A}L_{B}$.

For (v), let $A\in\mathcal{M}_{n}(\mathbb{R})$. By Kernel and Image of a Linear Map (i), $\ker L_{A}=\{x\in\mathbb{R}^{n}:Ax=0\}$, which contains $0$ since $A0=0$ (Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (v)), so the condition $\ker L_{A}=\{0\}$ is Criteria for Invertibility of a Square Real Matrix (i). The map $L_{A}$ is bijective exactly when it is injective and surjective (Injective, Surjective and Bijective Functions between Classes (iii)), and these two properties are Criteria for Invertibility of a Square Real Matrix (ii) and Criteria for Invertibility of a Square Real Matrix (iii). By Criteria for Invertibility of a Square Real Matrix, all of these conditions are equivalent to Criteria for Invertibility of a Square Real Matrix (vi), the invertibility of $A$.