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

Routine facts about maps are used without comment, in particular that two maps on the same domain with the same values are equal (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)).

The two versions. Each new version treated here has the text of its earlier version, with the same formulas and the same cited lemmas, except for its references: it adopts Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity in place of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces, Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices or Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; it cites Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) in place of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i); it cites the new versions of the other definitions treated here in place of their earlier versions; Block Matrix with Two Row Blocks and Two Column Blocks takes $[p]$ directly from Intervals of Natural Numbers (ii) in place of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (v), whose segments are those of Intervals of Natural Numbers (ii) as well; and Minor, Cofactor, and Adjugate of a Real Square Matrix refers to its own clauses by reference instead of by name. The earlier settings extend Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces, and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity extends Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, which extends Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces; these settings define nothing, and the notation the definitions treated here take from them, $\mathbb{N}$, $\mathbb{R}$ with its operations and order, and maps, is the same in both, as for Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) in The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i) and The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (ii).

By The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i), the set $\mathbb{R}^{n}$ of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i) is that of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i), with the same operations; its points are maps $[n]\to\mathbb{R}$ in both versions, with components their values (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii), Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii)). By The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (ii), the set $\mathcal{M}_{m\times n}(\mathbb{R})$ is the same in both versions, with the same entries and operations. So in every clause below the arguments range over the same sets in both versions, and their components and entries are the same elements of $\mathbb{R}$. The proof goes through the clauses in order, each using the earlier ones.

Dot product, norm and distance. For (i), both versions define

$$x\cdot y=\sum_{k=1}^{n}x_{k}y_{k}$$

(The Dot Product on $\mathbb{R}^n$ (i), The Dot Product on $\mathbb{R}^n$ (i)), a sum of the same elements of $\mathbb{R}$, so the two dot products are equal. For (ii), both versions define $\lVert x\rVert=\sqrt{x\cdot x}$ with the same square root (The Euclidean Norm on $\mathbb{R}^n$ (i), The Euclidean Norm on $\mathbb{R}^n$ (i)), and $x\cdot x$ is the same number by (i). For (iii), both versions define a map $\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ with value $\lVert x-y\rVert$ at $(x,y)$ (The Euclidean Distance on $\mathbb{R}^n$ (i), The Euclidean Distance on $\mathbb{R}^n$ (i)); the difference $x-y$ is the same point by The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i) and its norm the same number by (ii), so the two maps have the same domain and the same values and are equal.

Operations given by the existence lemma. Both versions of the matrix-vector product, the identity matrix and standard basis vectors, the product, the transpose and the trace name the value of the same map, or the same object, of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique, at the same arguments: $Ax$ is the value at $(A,x)$ of the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (ii) (Matrix-Vector Product (i), Matrix-Vector Product (i)); $I_{n}$ is the matrix of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (v) and $e_{k}$ the point of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (vi) (Identity Matrix and Standard Basis Vectors (i), Identity Matrix and Standard Basis Vectors (ii), Identity Matrix and Standard Basis Vectors (i), Identity Matrix and Standard Basis Vectors (ii)); $AB$ is the value at $(A,B)$ of the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (i) (Product of Real Matrices (i), Product of Real Matrices (i)); $A^{\top}$ is the value at $A$ of the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (iii) (Transpose of a Real Matrix (i), Transpose of a Real Matrix (i)); and $\operatorname{tr}(M)$ is the value at $M$ of the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique (iv) (Trace of a Real Square Matrix (i), Trace of a Real Square Matrix (i)). This gives (iv), (v), (vi), (vii) and (viii); in particular the entries $\delta_{ij}$ of $I_{n}$ are the same in both versions.

Determinant and its companions. For (ix), both versions define $\det$ on $\mathcal{M}_{n}(\mathbb{R})$ as the map $D_{n}$ of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique (ii) (Determinant of a Real Square Matrix (i), Determinant of a Real Square Matrix (i)). For (x), let $2\le n$, $A\in\mathcal{M}_{n}(\mathbb{R})$ and $i,j\in[n]$. In both versions $A^{(i,j)}$ is the matrix of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique (v) with entries $A_{s_{i}(k)s_{j}(l)}$, built from the same deletion index maps, so it is the same matrix. The minor $M_{ij}(A)=\det A^{(i,j)}$ is then the same number by (ix) applied on $\mathcal{M}_{n-1}(\mathbb{R})$, and so is the cofactor $C_{ij}(A)=(-1)^{i+j}M_{ij}(A)$. The adjugate is in both versions the matrix of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique (vi), with entries $(-1)^{l+k}\det A^{(l,k)}$, which are the same numbers by what was just shown; so the two adjugates are equal.

Inverses. For (xi), let $A,B\in\mathcal{M}_{n}(\mathbb{R})$. In both versions $B$ is an inverse of $A$ when $AB=I_{n}$ and $BA=I_{n}$ (Inverse Matrix and Invertible Real Square Matrix (i), Inverse Matrix and Invertible Real Square Matrix (i)); the products are the same matrices by (vi) and $I_{n}$ is the same matrix by (v), so the two conditions coincide. Invertibility is in both versions the existence of an inverse (Inverse Matrix and Invertible Real Square Matrix (ii), Inverse Matrix and Invertible Real Square Matrix (ii)), so it agrees, and $A^{-1}$ is in both the unique inverse of $A$, which is the same matrix since the inverses are the same.

Block and diagonal matrices. For (xii), both versions define the block matrix as the unique matrix $M\in\mathcal{M}_{m+n}(\mathbb{R})$ of Existence and Uniqueness of the Block Matrix with Two Row Blocks and Two Column Blocks (i) for the same $A$, $B$, $C$ and $D$ (Block Matrix with Two Row Blocks and Two Column Blocks (i), Block Matrix with Two Row Blocks and Two Column Blocks (i)), so it is the same matrix. For (xiii), both versions define $\operatorname{diag}(\lambda)$ as the map $[n]\times[n]\to\mathbb{R}$, $(i,j)\mapsto\lambda_{i}\delta_{ij}$ (Diagonal Matrix with Prescribed Diagonal (i), Diagonal Matrix with Prescribed Diagonal (i)); the components $\lambda_{i}$ are the same, and so are the entries $\delta_{ij}$ of $I_{n}$ by (v), so the two maps have the same values and are equal.

Orthogonal matrices. For (xiv), let $Q\in\mathcal{M}_{n}(\mathbb{R})$. In both versions $Q$ is orthogonal when $Q^{\top}Q=I_{n}$ (Orthogonal Real Matrices (i), Orthogonal Real Matrices (i)); $Q^{\top}$ is the same matrix by (vii), the product $Q^{\top}Q$ the same by (vi), and $I_{n}$ the same by (v), so the two conditions coincide. The set $\mathrm{O}(n)$ is in both versions the set of $Q\in\mathcal{M}_{n}(\mathbb{R})$ with $Q^{\top}Q=I_{n}$ (Orthogonal Real Matrices (ii), Orthogonal Real Matrices (ii)), a subset of the same set cut out by the same condition, so the two sets have the same elements and are equal.