Proof of Basic Properties of the Trace

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 and distributive laws of Commutative Rings §ring are used for real numbers without further mention. 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) 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. 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 (such as $i\mapsto sM_{ii}$ on $[n]$, or $j\mapsto U_{ij}V_{ji}$ on $[q]$ for fixed $i$) and every map on a product of two index sets (such as $(i,j)\mapsto U_{ij}V_{ji}$ on $[p]\times[q]$) 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, 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 a diagonal entry of a product matrix, which is a value of a map.

The trace is the sum of the diagonal entries, by Trace of a Real Square Matrix §trace; entries of $sM$, $tN$ and $sM+tN$ are as in Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations, of products as in Product of Real Matrices §product and of transposes as in Transpose of a Real Matrix §transpose.

Clause linearity. For $i\in[n]$, $(sM+tN)_{ii}=(sM)_{ii}+(tN)_{ii}=sM_{ii}+tN_{ii}$, so by (S1) and (S2)

$$\operatorname{tr}(sM+tN)=\sum_{i=1}^{n}(sM_{ii}+tN_{ii})=s\sum_{i=1}^{n}M_{ii}+t\sum_{i=1}^{n}N_{ii}=s\operatorname{tr}(M)+t\operatorname{tr}(N).$$

Clause transpose. $M^{\top}\in\mathcal{M}_{n}(\mathbb{R})$ and $(M^{\top})_{ii}=M_{ii}$ for $i\in[n]$, so $\operatorname{tr}(M^{\top})=\sum_{i=1}^{n}M_{ii}=\operatorname{tr}(M)$.

Clause cyclic. Here $UV\in\mathcal{M}_{p}(\mathbb{R})$ and $VU\in\mathcal{M}_{q}(\mathbb{R})$. By (S3),

$$\operatorname{tr}(UV)=\sum_{i=1}^{p}\sum_{j=1}^{q}U_{ij}V_{ji}=\sum_{j=1}^{q}\sum_{i=1}^{p}V_{ji}U_{ij}=\sum_{j=1}^{q}(VU)_{jj}=\operatorname{tr}(VU).$$

Clause entrywise. Here $U^{\top},V^{\top}\in\mathcal{M}_{q\times p}(\mathbb{R})$, $U^{\top}V\in\mathcal{M}_{q}(\mathbb{R})$ and $UV^{\top}\in\mathcal{M}_{p}(\mathbb{R})$, with $(U^{\top})_{ji}=U_{ij}$ and $(V^{\top})_{ji}=V_{ij}$ for $i\in[p]$ and $j\in[q]$. By (S3),

$$\operatorname{tr}(U^{\top}V)=\sum_{j=1}^{q}\sum_{i=1}^{p}(U^{\top})_{ji}V_{ij}=\sum_{j=1}^{q}\sum_{i=1}^{p}U_{ij}V_{ij}=\sum_{i=1}^{p}\sum_{j=1}^{q}U_{ij}V_{ij},$$ $$\operatorname{tr}(UV^{\top})=\sum_{i=1}^{p}\sum_{j=1}^{q}U_{ij}(V^{\top})_{ji}=\sum_{i=1}^{p}\sum_{j=1}^{q}U_{ij}V_{ij}.$$