Proof of Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes

Each result cited is universally quantified over the data in its own statement.

Conventions. We work in Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces; $\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 field and a commutative ring by Ordered Fields §ordered-field and Fields §field; the associative, commutative, neutral-element and distributive laws of Commutative Rings §ring are used for real numbers without further mention, and $0\cdot u=u\cdot0=0$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero. Addition on $\mathbb{R}$ is associative and commutative with neutral element $0$, and for $a\in\mathbb{N}$ a sum $\sum_{k=1}^{a}f(k)$ is the sum over the set $[a]=\{1,\dots,a\}$, by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings, Sums and Products over a Finite Set and over an Interval §intervals and Intervals of Natural Numbers §segment; $[a]$ is 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. For $a,b\in\mathbb{N}$, maps $f,g:[a]\to\mathbb{R}$ and $c\in\mathbb{R}$ we use: (S1) $\sum_{k=1}^{a}(f(k)+g(k))=\sum_{k=1}^{a}f(k)+\sum_{k=1}^{a}g(k)$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §termwise; (S2) $c\sum_{k=1}^{a}f(k)=\sum_{k=1}^{a}c\,f(k)$, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §distributive; (S3) if $y\in[a]$ and $f(k)=0$ for every $k\in[a]$ with $k\neq y$, then $\sum_{k=1}^{a}f(k)=f(y)$, by Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §vanishing; (S4) for $h:[a]\times[b]\to\mathbb{R}$, $\sum_{k=1}^{a}\sum_{l=1}^{b}h(k,l)=\sum_{l=1}^{b}\sum_{k=1}^{a}h(k,l)$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §product; (S5) $\sum_{k=1}^{a}c=a\,c$, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant; (S6) if $f(k)\le g(k)$ for every $k\in[a]$, then $\sum_{k=1}^{a}f(k)\le\sum_{k=1}^{a}g(k)$, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison; (S7) $\sum_{k=1}^{a}(f(k)-g(k))=\sum_{k=1}^{a}f(k)-\sum_{k=1}^{a}g(k)$, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §difference. Two sums whose terms agree at every index are equal, the term maps being equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

Maps given by expressions. Every term map summed below (for fixed values of the other indices, such as $j\mapsto A_{ij}B_{jk}C_{kl}$ on $[n]$) and every map on a product of two index sets (such as $(k,j)\mapsto A_{ij}B_{jk}C_{kl}$ on $[p]\times[n]$) takes values in $\mathbb{R}$ and exists by Maps and Relations Given by Formulas §map, respectively Maps and Relations Given by Formulas §binary: its expression is built from entries and components, which are values of maps, and from sums and products in $\mathbb{R}$, which are values of binary operations, and such expressions are predicative by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §value-substitution, Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §operation-substitution and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. Wherever an inner sum occurs as a function of an outer index, the computations below identify it termwise with an entry of a matrix or a component of a point, which is a value of a map.

Entries of sums and scalar multiples of matrices are as in Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations, components of sums and scalar multiples of points as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations; two matrices of the same size are equal when all their entries agree, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality, and two points of the same $\mathbb{R}^{r}$ when all their components agree, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality. Entries of products, of matrix-vector products and of transposes are given by Product of Real Matrices §product, Matrix-Vector Product §product and Transpose of a Real Matrix §transpose; $\delta$ denotes the entries of an identity matrix and $(e_{k})_{i}=\delta_{ik}$, by Identity Matrix and Standard Basis Vectors §identity and Identity Matrix and Standard Basis Vectors §basis.

Clause associative. Both sides lie in $\mathcal{M}_{m\times q}(\mathbb{R})$. For $i\in[m]$ and $l\in[q]$, by (S2) and (S4),

$$((AB)C)_{il}=\sum_{k=1}^{p}\Bigl(\sum_{j=1}^{n}A_{ij}B_{jk}\Bigr)C_{kl}=\sum_{k=1}^{p}\sum_{j=1}^{n}A_{ij}B_{jk}C_{kl}=\sum_{j=1}^{n}\sum_{k=1}^{p}A_{ij}B_{jk}C_{kl}=\sum_{j=1}^{n}A_{ij}\sum_{k=1}^{p}B_{jk}C_{kl}=(A(BC))_{il}.$$

Clause distributive. For $i\in[m]$ and $k\in[p]$, by (S1),

$$(A(B+B'))_{ik}=\sum_{j=1}^{n}A_{ij}(B_{jk}+B'_{jk})=\sum_{j=1}^{n}A_{ij}B_{jk}+\sum_{j=1}^{n}A_{ij}B'_{jk}=(AB)_{ik}+(AB')_{ik}=(AB+AB')_{ik},$$

and in the same way $((A+A')B)_{ik}=\sum_{j=1}^{n}(A_{ij}+A'_{ij})B_{jk}=(AB)_{ik}+(A'B)_{ik}=(AB+A'B)_{ik}$.

Clause scalar. For $i\in[m]$ and $k\in[p]$, by (S2),

$$((sA)B)_{ik}=\sum_{j=1}^{n}(sA_{ij})B_{jk}=s\sum_{j=1}^{n}A_{ij}B_{jk}=(s(AB))_{ik},\qquad (A(sB))_{ik}=\sum_{j=1}^{n}A_{ij}(sB_{jk})=s\sum_{j=1}^{n}A_{ij}B_{jk}=(s(AB))_{ik}.$$

Clause identity. Let $i\in[m]$ and $j\in[n]$. The term $\delta_{ik}A_{kj}$ of $(I_{m}A)_{ij}=\sum_{k=1}^{m}\delta_{ik}A_{kj}$ is $0\cdot A_{kj}=0$ for $k\neq i$, so by (S3) $(I_{m}A)_{ij}=\delta_{ii}A_{ij}=A_{ij}$. Likewise the term $A_{ik}\delta_{kj}$ of $(AI_{n})_{ij}=\sum_{k=1}^{n}A_{ik}\delta_{kj}$ vanishes for $k\neq j$, so $(AI_{n})_{ij}=A_{ij}\delta_{jj}=A_{ij}$.

Clause matrix-vector. Let $i\in[m]$. By (S1) and (S2),

$$(A(x+y))_{i}=\sum_{j=1}^{n}A_{ij}(x_{j}+y_{j})=(Ax)_{i}+(Ay)_{i},\qquad (A(sx))_{i}=\sum_{j=1}^{n}A_{ij}(sx_{j})=s\,(Ax)_{i},$$ $$((A+A')x)_{i}=\sum_{j=1}^{n}(A_{ij}+A'_{ij})x_{j}=(Ax)_{i}+(A'x)_{i},\qquad ((sA)x)_{i}=\sum_{j=1}^{n}(sA_{ij})x_{j}=s\,(Ax)_{i},$$

which are the $i$-th components of $Ax+Ay$, $s(Ax)$, $Ax+A'x$ and $s(Ax)$. Likewise, since $(x-y)_{j}=x_{j}-y_{j}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations and $A_{ij}(x_{j}-y_{j})=A_{ij}x_{j}-A_{ij}y_{j}$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, (S7) gives

$$(A(x-y))_{i}=\sum_{j=1}^{n}A_{ij}(x_{j}-y_{j})=\sum_{j=1}^{n}A_{ij}x_{j}-\sum_{j=1}^{n}A_{ij}y_{j}=(Ax)_{i}-(Ay)_{i},$$

the $i$-th component of $Ax-Ay$. Here $Bz\in\mathbb{R}^{n}$ and $(AB)z,A(Bz)\in\mathbb{R}^{m}$, and by (S2) and (S4)

$$((AB)z)_{i}=\sum_{k=1}^{p}\Bigl(\sum_{j=1}^{n}A_{ij}B_{jk}\Bigr)z_{k}=\sum_{k=1}^{p}\sum_{j=1}^{n}A_{ij}B_{jk}z_{k}=\sum_{j=1}^{n}\sum_{k=1}^{p}A_{ij}B_{jk}z_{k}=\sum_{j=1}^{n}A_{ij}(Bz)_{j}=(A(Bz))_{i}.$$

For $i\in[n]$, the term $\delta_{ik}x_{k}$ of $(I_{n}x)_{i}=\sum_{k=1}^{n}\delta_{ik}x_{k}$ vanishes for $k\neq i$, so $(I_{n}x)_{i}=x_{i}$ by (S3). The origin is the constant map with value $0$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin, so for $i\in[m]$, by (S5), $(A0)_{i}=\sum_{j=1}^{n}A_{ij}\cdot0=\sum_{j=1}^{n}0=n\cdot0=0$, the $i$-th component of the origin of $\mathbb{R}^{m}$.

Clause column. For $k\in[n]$ and $i\in[m]$, the term $A_{ij}\delta_{jk}$ of $(Ae_{k})_{i}=\sum_{j=1}^{n}A_{ij}(e_{k})_{j}=\sum_{j=1}^{n}A_{ij}\delta_{jk}$ vanishes for $j\neq k$, so $(Ae_{k})_{i}=A_{ik}\delta_{kk}=A_{ik}$ by (S3).

Clause transpose. Let $i\in[m]$, $j\in[n]$ and $k\in[p]$; every index pair of $\mathcal{M}_{n\times m}(\mathbb{R})$ is of the form $(j,i)$ and every index pair of $\mathcal{M}_{p\times m}(\mathbb{R})$ of the form $(k,i)$. Applying Transpose of a Real Matrix §transpose twice, $((A^{\top})^{\top})_{ij}=(A^{\top})_{ji}=A_{ij}$. Next

$$((A+A')^{\top})_{ji}=A_{ij}+A'_{ij}=(A^{\top})_{ji}+(A'^{\top})_{ji},\qquad ((sA)^{\top})_{ji}=sA_{ij}=s\,(A^{\top})_{ji};$$

these are the $(j,i)$ entries of $A^{\top}+A'^{\top}$ and $sA^{\top}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations, so the matrices are equal by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality. With $B^{\top}\in\mathcal{M}_{p\times n}(\mathbb{R})$ and $A^{\top}\in\mathcal{M}_{n\times m}(\mathbb{R})$,

$$((AB)^{\top})_{ki}=(AB)_{ik}=\sum_{j=1}^{n}A_{ij}B_{jk}=\sum_{j=1}^{n}(B^{\top})_{kj}(A^{\top})_{ji}=(B^{\top}A^{\top})_{ki}.$$

For $i,j\in[n]$, $(I_{n}^{\top})_{ji}=\delta_{ij}=\delta_{ji}$, both being $1$ if $i=j$ and $0$ otherwise.

Clause adjoint. Here $Ax\in\mathbb{R}^{m}$ and $A^{\top}w\in\mathbb{R}^{n}$ with $(A^{\top}w)_{j}=\sum_{i=1}^{m}(A^{\top})_{ji}w_{i}=\sum_{i=1}^{m}A_{ij}w_{i}$. By The Dot Product on $\mathbb{R}^n$ §dot-product, (S2) and (S4),

$$(Ax)\cdot w=\sum_{i=1}^{m}\Bigl(\sum_{j=1}^{n}A_{ij}x_{j}\Bigr)w_{i}=\sum_{i=1}^{m}\sum_{j=1}^{n}x_{j}A_{ij}w_{i}=\sum_{j=1}^{n}\sum_{i=1}^{m}x_{j}A_{ij}w_{i}=\sum_{j=1}^{n}x_{j}\sum_{i=1}^{m}A_{ij}w_{i}=x\cdot(A^{\top}w).$$

Clause bound. For $i\in[m]$ let $r_{i}$ be the unique set $\rho$ such that $\rho$ is a map $[n]\to\mathbb{R}$ and $\rho(j)=A((i,j))$ for all $j\in[n]$. This formula is predicative 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 Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, and exactly one such $\rho$ exists by Maps and Relations Given by Formulas §map, as for $j\in[n]$ we have $(i,j)\in[m]\times[n]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, hence $A((i,j))\in\mathbb{R}$, $A$ being a map $[m]\times[n]\to\mathbb{R}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, and $A((i,j))=A_{ij}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries. So $r_{i}$ is a defined set symbol, used properly for $i\in[m]$, and expressions containing it fall again under Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. It lies in $\mathbb{R}^{n}$ with components $(r_{i})_{j}=A_{ij}$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. By The Dot Product on $\mathbb{R}^n$ §dot-product, $u_{i}:=(Ax)_{i}=\sum_{j=1}^{n}(r_{i})_{j}x_{j}=r_{i}\cdot x$, so with the Euclidean norms $a_{i}=\lVert r_{i}\rVert$ and $b=\lVert x\rVert$, The Cauchy-Schwarz Inequality on $\mathbb{R}^n$ §cauchy-schwarz gives $|u_{i}|\le a_{i}b$. Here $|u_{i}|\ge0$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value, hence also $a_{i}b\ge|u_{i}|\ge0$. Hence, using $v\le|v|$ for $v=u_{i}^{2}$ from Rules of Arithmetic and Order in an Ordered Field §absolute-value, $|u_{i}^{2}|=|u_{i}|^{2}$ from Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §sign, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff with exponent $2$, and $(a_{i}b)^{2}=a_{i}^{2}b^{2}$ from Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product,

$$u_{i}^{2}\le|u_{i}^{2}|=|u_{i}|^{2}\le(a_{i}b)^{2}=a_{i}^{2}b^{2}.$$

By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, $a_{i}^{2}=\sum_{j=1}^{n}(r_{i})_{j}^{2}=\sum_{j=1}^{n}A_{ij}^{2}$ and $\lVert Ax\rVert^{2}=\sum_{i=1}^{m}u_{i}^{2}$. The map $i\mapsto a_{i}^{2}b^{2}$ exists by Maps and Relations Given by Formulas §map, $a_{i}$ being the value at $r_{i}$ of the norm map of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §norm. By (S6), the termwise equality $a_{i}^{2}=\sum_{j=1}^{n}A_{ij}^{2}$ and (S2),

$$\lVert Ax\rVert^{2}=\sum_{i=1}^{m}u_{i}^{2}\le\sum_{i=1}^{m}a_{i}^{2}\,b^{2}=\Bigl(\sum_{i=1}^{m}\sum_{j=1}^{n}A_{ij}^{2}\Bigr)\lVert x\rVert^{2}.$$