Proof of Powers of a Square Matrix

Computations with real numbers use The Real Numbers as a Type. Matrix products are associative by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (i). An induction on $k\in\mathbb{N}_{0}$ below shows that the class of the $k\in\mathbb{N}_{0}$ with the stated property contains $0$ and contains $k+1$ whenever it contains $k$; it then contains $\mathbb{N}_{0}$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity (iv), the successor of $k$ being $k+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (v).

Step 1: $M^{0}=I_{n}$ and $M^{k+1}=M^{k}M$. By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (iv), with $n$ in place of $m$, $I_{n}X=X=XI_{n}$ for every $X\in\mathcal{M}_{n}(\mathbb{R})$, so $I_{n}$ is a neutral element of the matrix product on $\mathcal{M}_{n}(\mathbb{R})$ (Associative and Commutative Binary Operations, and Neutral Elements (iii)); it is the only one by A Binary Operation Has at Most One Neutral Element (i), so $M^{0}=I_{n}$ by Powers with Exponents in the Natural Numbers with Zero (ii). Let $k\in\mathbb{N}_{0}$. This step is a case split, not an induction: $k=0$ or $k\in\mathbb{N}$, by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii). If $k=0$, then $k+1=1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i), and $M^{1}=\prod_{l=1}^{1}M=M$ by Powers with Exponents in the Natural Numbers with Zero (i) and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), applied to the constant map $[1]\to\mathcal{M}_{n}(\mathbb{R})$ with value $M$; and $M=I_{n}M=M^{0}M$. If $k\in\mathbb{N}$, then $k+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), applied to the constant map $[k+1]\to\mathcal{M}_{n}(\mathbb{R})$ with value $M$, whose restriction to $[k]$ is the constant map $[k]\to\mathcal{M}_{n}(\mathbb{R})$ with value $M$ (Iterated Operations: Finite Sums and Finite Products (ii)), gives

$$M^{k+1}=\prod_{l=1}^{k+1}M=\Bigl(\prod_{l=1}^{k}M\Bigr)M=M^{k}M$$

by Powers with Exponents in the Natural Numbers with Zero (i). So $M^{k+1}=M^{k}M$ for every $k\in\mathbb{N}_{0}$.

Step 2: (iii). Let $BM=MB$. For $k=0$, $BM^{0}=BI_{n}=B=I_{n}B=M^{0}B$ by Step 1 and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (iv). If $BM^{k}=M^{k}B$, then by Step 1 and associativity

$$BM^{k+1}=B(M^{k}M)=(BM^{k})M=(M^{k}B)M=M^{k}(BM)=M^{k}(MB)=(M^{k}M)B=M^{k+1}B .$$

By induction, $BM^{k}=M^{k}B$ for every $k\in\mathbb{N}_{0}$.

Step 3: (i). Step 2 with $M$ in place of $B$ gives $MM^{k}=M^{k}M$; together with Step 1 this is (i).

Step 4: (ii). Fix $j\in\mathbb{N}_{0}$. For $k=0$, $j+0=j$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i), and $M^{j}=M^{j}I_{n}=M^{j}M^{0}$ by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (iv) and (i). If $M^{j+k}=M^{j}M^{k}$, then, as $j+(k+1)=(j+k)+1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iii),

$$M^{j+(k+1)}=M^{(j+k)+1}=M^{j+k}M=(M^{j}M^{k})M=M^{j}(M^{k}M)=M^{j}M^{k+1}$$

by (i) and associativity. By induction on $k$, (ii) holds.

Step 5: (iv). By Powers with Exponents in the Natural Numbers with Zero (ii), $c^{0}=1$, and $c^{k+1}=c^{k}c^{1}=c^{k}c$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i) and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii), $\mathbb{R}$ being a commutative ring. For $k=0$, $(cM)^{0}=I_{n}=1\,I_{n}=c^{0}M^{0}$ by (i), the middle equality entrywise by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv). If $(cM)^{k}=c^{k}M^{k}$, then by (i) and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (iii), used twice,

$$(cM)^{k+1}=(cM)^{k}(cM)=(c^{k}M^{k})(cM)=c^{k}\bigl(M^{k}(cM)\bigr)=c^{k}\bigl(c\,(M^{k}M)\bigr)=(c^{k}c)M^{k+1}=c^{k+1}M^{k+1},$$

where $c^{k}(cX)=(c^{k}c)X$ for $X\in\mathcal{M}_{n}(\mathbb{R})$ holds entrywise by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv). By induction, (iv) holds.

Step 6: (v). For $k=0$, $(M^{\top})^{0}=I_{n}=I_{n}^{\top}=(M^{0})^{\top}$ by (i) and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (vii). If $(M^{\top})^{k}=(M^{k})^{\top}$, then by (i) and the rule $(XY)^{\top}=Y^{\top}X^{\top}$ of Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (vii), with $M$ and $M^{k}$ in place of $X$ and $Y$,

$$(M^{\top})^{k+1}=(M^{\top})^{k}M^{\top}=(M^{k})^{\top}M^{\top}=(MM^{k})^{\top}=(M^{k+1})^{\top}.$$

By induction, (v) holds.

Step 7: (vi). For $k=0$, $\lVert M^{0}\rVert=\lVert I_{n}\rVert=\lVert 1\,I_{n}\rVert=|1|=1=\lVert M\rVert^{0}$ by (i), The Operator Norm of Entries, Transposes, Multiples of the Identity, Orthogonal Factors and Diagonal Matrices (vi) with $t=1$, and Powers with Exponents in the Natural Numbers with Zero (ii). If $\lVert M^{k}\rVert\le\lVert M\rVert^{k}$, then, as $0\le\lVert M\rVert$ by Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (i), (i), Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (vii), and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i) and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii) for the real number $\lVert M\rVert$ (so $\lVert M\rVert^{k+1}=\lVert M\rVert^{k}\lVert M\rVert^{1}=\lVert M\rVert^{k}\lVert M\rVert$) give

$$\lVert M^{k+1}\rVert=\lVert M^{k}M\rVert\le\lVert M^{k}\rVert\,\lVert M\rVert\le\lVert M\rVert^{k}\,\lVert M\rVert=\lVert M\rVert^{k+1}.$$

By induction, (vi) holds.