Proof of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique

Each result cited is universally quantified over the data in its own statement. We work in Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces.

Preliminaries. $\mathbb{R}$ is an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, hence a commutative ring by Ordered Fields §ordered-field and Fields §field; so $+$ and $\cdot$ are binary operations on $\mathbb{R}$ whose values lie in $\mathbb{R}$ by Binary Operations on a Set §notation, and sums are as in Commutative Rings, Fields and Ordered Fields: Standard Notation §rings. For $q\in\{m,n,p\}$, $[q]=\{1,\dots,q\}$ by Intervals of Natural Numbers §segment; it is a set by Tuples in a Set: the Set of n-Tuples and Their Components §tuples, finite by 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 §naturals, and $1\le q$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order. For $q,r\in\{m,n,p\}$, $[q]\times[r]$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, and its elements are exactly the pairs $(i,j)$ with $i\in[q]$ and $j\in[r]$, by The Cartesian Product of Two Classes §product and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. For a set $D$, $\mathbb{R}^{D}$ is a set whose elements are exactly the maps $h:D\to\mathbb{R}$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §set and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members; for such $h$ and $u\in D$ we have $u\in\operatorname{dom}h$ and $h(u)\in\operatorname{ran}h\subseteq\mathbb{R}$, by Functions, Values of a Function, and Functions from One Class to Another §map, Functions, Values of a Function, and Functions from One Class to Another §value and Relations, Domain, Range, Inverse and Composition §range. In particular $\mathcal{M}_{q\times r}(\mathbb{R})=\mathbb{R}^{[q]\times[r]}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, with $A_{ij}=A((i,j))$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries and Sets and Maps: Ordinary Notation §maps; and $\mathbb{R}^{q}=\mathbb{R}^{[q]}$, with $x_{j}=x(j)$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §space and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. For a map $f$ on a product, $f(v,w)$ stands for $f((v,w))$ by Sets and Maps: Ordinary Notation §maps.

(E) Two elements of $\mathbb{R}^{D}$ both have domain $D$ by Functions, Values of a Function, and Functions from One Class to Another §map, so they are equal as soon as their values agree at every element of $D$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality; for $D=[q]\times[r]$ it suffices to compare the values at the pairs $(i,j)$ with $i\in[q]$ and $j\in[r]$.

(S) Let $\Sigma_{[n]}:\mathbb{R}^{[n]}\to\mathbb{R}$ be the map of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §sum-map for the finite set $B=[n]$. Let $a\in\mathbb{R}^{[n]}$, and let $s(j)$ be an expression with $s(j)=a(j)$ for every $j\in[n]$. Then $\sum_{j=1}^{n}s(j)=\Sigma_{[n]}(a)$. Indeed, by Iterated Operations: Finite Sums and Finite Products §iterated, $\sum_{j=1}^{n}s(j)$ is the iterated sum of the map $j\mapsto s(j)$ on $[n]$, which is $a$ by (E); since $1\le n$, Sums and Products over a Finite Set and over an Interval §intervals gives $\sum_{j=1}^{n}a_{j}=\sum_{j\in[n]}a(j)$; and this is $\Sigma_{[n]}(a)$ by The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §sum-map.

Step 1: real-valued maps given by expressions, as defined set symbols. Let $v_{1},\dots,v_{k}$ be set variables, the arguments, and $\gamma(v_{1},\dots,v_{k})$ a predicative formula. Let $D$ be one of the sets $[q]$ or $[q]\times[r]$ above, and let $e$ be an expression, either $e(u)$ for $u\in D$, or $e(u,w)$ for $u\in[q]$ and $w\in[r]$ when $D=[q]\times[r]$, in the arguments and the parameters $[m]$, $[n]$, $[p]$, $\mathbb{R}$, $\cdot$ and $\Sigma_{[n]}$. Assume that $e$ is built from ordered pairs, used as defined set symbols as in The Cartesian Product of Two Classes §product, from values of maps and of binary operations, which are defined set symbols by Functions, Values of a Function, and Functions from One Class to Another §value and Binary Operations on a Set §notation, and from symbols introduced by earlier uses of this step; that no quantifier in it is applied to a class variable; and that whenever $\gamma$ holds, the symbols in $e$ are used properly and the value of $e$ lies in $\mathbb{R}$ at every $u\in D$, respectively at all $u\in[q]$ and $w\in[r]$. Let $\theta_{e}(h,v_{1},\dots,v_{k})$ be

$$\mu(h,D,\mathbb{R})\wedge\forall u\,\bigl(u\in D\Rightarrow h(u)=e(u)\bigr),\quad\text{respectively}\quad\mu(h,D,\mathbb{R})\wedge\forall u\,\forall w\,\bigl((u\in[q]\wedge w\in[r])\Rightarrow h((u,w))=e(u,w)\bigr),$$

where $\mu$ is the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map; it is predicative, and $\mu(h,D,\mathbb{R})$ holds if and only if $h:D\to\mathbb{R}$, by that clause. The second conjunct is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, so $\theta_{e}$ is predicative. Whenever $\gamma$ holds, exactly one set $h$ satisfies $\theta_{e}$: this is Maps and Relations Given by Formulas §map with $a=D$ and $b=\mathbb{R}$, respectively Maps and Relations Given by Formulas §binary with $c=[q]$, $d=[r]$ and $b=\mathbb{R}$. Write $T_{e}(v_{1},\dots,v_{k})$ for this set. It is a defined set symbol in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, used properly whenever $\gamma$ holds, and given by a predicative formula, so expressions containing it fall again under Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure (and under Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination) and may be used in later applications of this step; moreover $T_{e}\in\mathbb{R}^{D}$, with $T_{e}(u)=e(u)$ for $u\in D$, respectively $T_{e}((u,w))=e(u,w)$ for $u\in[q]$ and $w\in[r]$. Below, the conditions $A\in\mathcal{M}_{q\times r}(\mathbb{R})$ and $x\in\mathbb{R}^{q}$ in a formula $\gamma$ stand for $\mu(A,[q]\times[r],\mathbb{R})$ and $\mu(x,[q],\mathbb{R})$, which are equivalent to them by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members; so each $\gamma$ below is a conjunction of predicative formulas, hence predicative.

Uniqueness in the clauses product, matrix-vector, transpose and trace. In each of these clauses, the map is obtained from Maps and Relations Given by Formulas §map or Maps and Relations Given by Formulas §binary, with a value $V$ at each argument; we show that $V$ has the entries, components or value required by the clause and, for the first three clauses, that by (E) it is the only element of the target with them. Then every map with the property of the clause has the value $V$ at every argument, and it coincides with the map obtained, by the uniqueness given by the scheme.

Clause product. Let $\gamma_{1}(A,B)$ be $A\in\mathcal{M}_{m\times n}(\mathbb{R})\wedge B\in\mathcal{M}_{n\times p}(\mathbb{R})$. For $i\in[m]$, $j\in[n]$ and $k\in[p]$ we have $(i,j)\in[m]\times[n]=\operatorname{dom}A$ and $(j,k)\in[n]\times[p]=\operatorname{dom}B$, so $A((i,j))$ and $B((j,k))$ are used properly and lie in $\mathbb{R}$, and so does their product. By Step 1 with the arguments $A,B,i,k$, the formula $\gamma_{1}(A,B)\wedge i\in[m]\wedge k\in[p]$, $D=[n]$ and $e(j)=A((i,j))\cdot B((j,k))$, we obtain $R(A,B,i,k)\in\mathbb{R}^{[n]}$ with $R(A,B,i,k)(j)=A_{ij}B_{jk}$ for $j\in[n]$. Hence $R(A,B,i,k)\in\operatorname{dom}\Sigma_{[n]}$, and $\Sigma_{[n]}(R(A,B,i,k))\in\mathbb{R}$; by (S), $\Sigma_{[n]}(R(A,B,i,k))=\sum_{j=1}^{n}A_{ij}B_{jk}$. By Step 1 with the arguments $A,B$, the formula $\gamma_{1}$, $D=[m]\times[p]$ and $e(i,k)=\Sigma_{[n]}(R(A,B,i,k))$, we obtain $C(A,B)\in\mathcal{M}_{m\times p}(\mathbb{R})$ with $C(A,B)_{ik}=\sum_{j=1}^{n}A_{ij}B_{jk}$ for $i\in[m]$ and $k\in[p]$. Then Maps and Relations Given by Formulas §binary, with $c=\mathcal{M}_{m\times n}(\mathbb{R})$, $d=\mathcal{M}_{n\times p}(\mathbb{R})$ and $b=\mathcal{M}_{m\times p}(\mathbb{R})$, gives exactly one map $\pi$ with $\pi(A,B)=C(A,B)$, which has the required entries; and by (E), $C(A,B)$ is the only element of $\mathcal{M}_{m\times p}(\mathbb{R})$ with these entries.

Clause matrix-vector. Let $\gamma_{2}(A,x)$ be $A\in\mathcal{M}_{m\times n}(\mathbb{R})\wedge x\in\mathbb{R}^{n}$. As in the clause product, Step 1 with the arguments $A,x,i$, the formula $\gamma_{2}(A,x)\wedge i\in[m]$, $D=[n]$ and $e(j)=A((i,j))\cdot x(j)$ gives $R'(A,x,i)\in\mathbb{R}^{[n]}$ with $R'(A,x,i)(j)=A_{ij}x_{j}$, so $\Sigma_{[n]}(R'(A,x,i))\in\mathbb{R}$ equals $\sum_{j=1}^{n}A_{ij}x_{j}$ by (S). Step 1 with the arguments $A,x$, the formula $\gamma_{2}$, $D=[m]$ and $e(i)=\Sigma_{[n]}(R'(A,x,i))$ gives $W(A,x)\in\mathbb{R}^{[m]}=\mathbb{R}^{m}$ with $W(A,x)_{i}=\sum_{j=1}^{n}A_{ij}x_{j}$ for $i\in[m]$. Then Maps and Relations Given by Formulas §binary, with $c=\mathcal{M}_{m\times n}(\mathbb{R})$, $d=\mathbb{R}^{n}$ and $b=\mathbb{R}^{m}$, gives exactly one map $\phi$ with $\phi(A,x)=W(A,x)$; by (E), $W(A,x)$ is the only element of $\mathbb{R}^{m}$ with these components.

Clause transpose. Let $\gamma_{3}(A)$ be $A\in\mathcal{M}_{m\times n}(\mathbb{R})$. For $j\in[n]$ and $i\in[m]$, $A((i,j))$ is used properly and lies in $\mathbb{R}$. Step 1 with the argument $A$, the formula $\gamma_{3}$, $D=[n]\times[m]$ and $e(j,i)=A((i,j))$ gives $U(A)\in\mathcal{M}_{n\times m}(\mathbb{R})$ with $U(A)_{ji}=A_{ij}$. Then Maps and Relations Given by Formulas §map, with $a=\mathcal{M}_{m\times n}(\mathbb{R})$ and $b=\mathcal{M}_{n\times m}(\mathbb{R})$, gives exactly one map $\tau$ with $\tau(A)=U(A)$; by (E), $U(A)$ is the only element of $\mathcal{M}_{n\times m}(\mathbb{R})$ with these entries.

Clause trace. Here $\mathcal{M}_{n}(\mathbb{R})=\mathcal{M}_{n\times n}(\mathbb{R})$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices. Let $\gamma_{4}(A)$ be $A\in\mathcal{M}_{n\times n}(\mathbb{R})$. Step 1 with the argument $A$, the formula $\gamma_{4}$, $D=[n]$ and $e(i)=A((i,i))$ gives $\Delta(A)\in\mathbb{R}^{[n]}$ with $\Delta(A)(i)=A_{ii}$, so $\Sigma_{[n]}(\Delta(A))\in\mathbb{R}$ equals $\sum_{i=1}^{n}A_{ii}$ by (S). Then Maps and Relations Given by Formulas §map, with $a=\mathcal{M}_{n}(\mathbb{R})$ and $b=\mathbb{R}$, gives exactly one map $t$ with $t(A)=\Sigma_{[n]}(\Delta(A))=\sum_{i=1}^{n}A_{ii}$, which is the condition of the clause.

Clause identity. In this clause and the next, $1$ and $0$ are the unit and the zero of $\mathbb{R}$, by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals and Commutative Rings, Fields and Ordered Fields: Standard Notation §rings, and they lie in $\mathbb{R}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals. Let $P(z)$ be the formula $\exists u\,(u\in[n]\wedge z=(u,u))$, with the parameter $[n]$; it is predicative, as $z=(u,u)$ is by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-equality. By Maps Defined by Cases §cases, with the sets $[n]\times[n]$ and $\mathbb{R}$, the property $P$ and the expressions $1$ and $0$, there is a map $E:[n]\times[n]\to\mathbb{R}$, so $E\in\mathcal{M}_{n}(\mathbb{R})$, with $E(z)=1$ if $P(z)$ and $E(z)=0$ otherwise. Let $i,j\in[n]$. If $i=j$, then $P((i,j))$ holds with $u=i$, so $E_{ij}=1$. If $i\neq j$, then $P((i,j))$ fails: $(i,j)=(u,u)$ would give $i=u=j$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; so $E_{ij}=0$. If $E'\in\mathcal{M}_{n}(\mathbb{R})$ also has these entries, then $E'_{ij}=E_{ij}$ for all $i,j\in[n]$, and $E'=E$ by (E).

Clause basis. Let $k\in[n]$, and let $P(i)$ be the atomic formula $i=k$, with the parameter $k$. By Maps Defined by Cases §cases, with the sets $[n]$ and $\mathbb{R}$, the property $P$ and the expressions $1$ and $0$, there is a map $e:[n]\to\mathbb{R}$, so $e\in\mathbb{R}^{n}$, with $e_{i}=e(i)=1$ if $i=k$ and $e_{i}=0$ if $i\neq k$, for $i\in[n]$. If $e'\in\mathbb{R}^{n}$ also has these components, then $e'=e$ by (E).