The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, with Euclidean space $\mathbb{R}^{n}$, the set $\mathcal{M}_{m\times n}(\mathbb{R})$ of real $m\times n$ matrices and $\mathcal{M}_{n}(\mathbb{R})=\mathcal{M}_{n\times n}(\mathbb{R})$, for $m,n\in\mathbb{N}$, and the segments $[n]$ of Intervals of Natural Numbers (ii).

(i) Dot product. For every $n\in\mathbb{N}$ and all $x,y\in\mathbb{R}^{n}$, the dot product $x\cdot y$ of the earlier version is the dot product $x\cdot y$ of the new version.

(ii) Euclidean norm. For every $n\in\mathbb{N}$ and every $x\in\mathbb{R}^{n}$, the Euclidean norm $\lVert x\rVert$ of the earlier version is the Euclidean norm $\lVert x\rVert$ of the new version.

(iii) Euclidean distance. For every $n\in\mathbb{N}$, the Euclidean distance $d_{E}:\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ of the earlier version is the Euclidean distance $d_{E}$ of the new version.

(iv) Matrix-vector product. For all $m,n\in\mathbb{N}$, every $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ and every $x\in\mathbb{R}^{n}$, the matrix-vector product $Ax$ of the earlier version is the matrix-vector product $Ax$ of the new version.

(v) Identity matrix and standard basis. For every $n\in\mathbb{N}$, the identity matrix $I_{n}$ of the earlier version is the identity matrix $I_{n}$ of the new version, and for every $k\in[n]$ the standard basis vector $e_{k}$ of the earlier version is the standard basis vector $e_{k}$ of the new version.

(vi) Matrix product. For all $m,n,p\in\mathbb{N}$, every $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ and every $B\in\mathcal{M}_{n\times p}(\mathbb{R})$, the product $AB$ of the earlier version is the product $AB$ of the new version.

(vii) Transpose. For all $m,n\in\mathbb{N}$ and every $A\in\mathcal{M}_{m\times n}(\mathbb{R})$, the transpose $A^{\top}$ of the earlier version is the transpose $A^{\top}$ of the new version.

(viii) Trace. For every $n\in\mathbb{N}$ and every $M\in\mathcal{M}_{n}(\mathbb{R})$, the trace $\operatorname{tr}(M)$ of the earlier version is the trace $\operatorname{tr}(M)$ of the new version.

(ix) Determinant. For every $n\in\mathbb{N}$, the determinant $\det:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$ of the earlier version is the determinant $\det$ of the new version.

(x) Minors, cofactors and adjugate. For every $n\in\mathbb{N}$ with $2\le n$, every $A\in\mathcal{M}_{n}(\mathbb{R})$ and all $i,j\in[n]$, the matrix $A^{(i,j)}$, the minor $M_{ij}(A)$, the cofactor $C_{ij}(A)$ and the adjugate $\operatorname{adj}(A)$ of the earlier version (Minor, Cofactor, and Adjugate of a Real Square Matrix (i), Minor, Cofactor, and Adjugate of a Real Square Matrix (ii), Minor, Cofactor, and Adjugate of a Real Square Matrix (iii), Minor, Cofactor, and Adjugate of a Real Square Matrix (iv)) are those of the new version (Minor, Cofactor, and Adjugate of a Real Square Matrix (i), Minor, Cofactor, and Adjugate of a Real Square Matrix (ii), Minor, Cofactor, and Adjugate of a Real Square Matrix (iii), Minor, Cofactor, and Adjugate of a Real Square Matrix (iv)).

(xi) Inverses. For every $n\in\mathbb{N}$ and all $A,B\in\mathcal{M}_{n}(\mathbb{R})$, $B$ is an inverse of $A$ in the earlier version if and only if it is an inverse of $A$ in the new version; and $A$ is invertible in the earlier version if and only if it is invertible in the new version, and then $A^{-1}$ is the same matrix in both.

(xii) Block matrices. For all $m,n\in\mathbb{N}$ and all $A\in\mathcal{M}_{m}(\mathbb{R})$, $B\in\mathcal{M}_{m\times n}(\mathbb{R})$, $C\in\mathcal{M}_{n\times m}(\mathbb{R})$ and $D\in\mathcal{M}_{n}(\mathbb{R})$, the block matrix with blocks $A$, $B$, $C$, $D$ of the earlier version is the block matrix with these blocks of the new version.

(xiii) Diagonal matrices. For every $n\in\mathbb{N}$ and every $\lambda\in\mathbb{R}^{n}$, the diagonal matrix $\operatorname{diag}(\lambda)$ of the earlier version is the diagonal matrix $\operatorname{diag}(\lambda)$ of the new version.

(xiv) Orthogonal matrices. For every $n\in\mathbb{N}$ and every $Q\in\mathcal{M}_{n}(\mathbb{R})$, $Q$ is orthogonal in the earlier version if and only if it is orthogonal in the new version; and the set $\mathrm{O}(n)$ of the earlier version is the set $\mathrm{O}(n)$ of the new version.