Proof of The Operator-Norm Distance between Real Matrices Is a Map

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

Let $I=[m]\times[n]$ and $\mathcal{M}=\mathcal{M}_{m\times n}(\mathbb{R})$, which is the set $\mathbb{R}^{I}$ of maps $I\to\mathbb{R}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices. Let $\oplus$ be the binary operation on $\mathcal{M}$ of Pointwise Operations on Real-Valued Maps Exist and Are Unique §binary for the operation $+$ of $\mathbb{R}$, and $\nu:\mathcal{M}\to\mathcal{M}$ the map of Pointwise Operations on Real-Valued Maps Exist and Are Unique §negative. By Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations and Pointwise Operations on Real-Valued Maps §operations, for $V,W\in\mathcal{M}$, $V+W=\oplus((V,W))$, $-W=\nu(W)$ and $V-W=V+(-W)=\oplus((V,\nu(W)))$. Let $\eta:\mathcal{M}\to\mathbb{R}$ be the operator norm, a map with $\eta(K)=\lVert K\rVert$ for $K\in\mathcal{M}$, by The Operator Norm of a Real Matrix §norm.

Apply Maps and Relations Given by Formulas §binary with $\mathbb{R}$ for its $b$, $\mathcal{M}$ for its $c$ and $d$, and the expression $e(V,W)=\eta(\oplus((V,\nu(W))))$. It is built from the variables $V$ and $W$, the maps $\oplus$, $\nu$ and $\eta$ as parameters, and the defined set symbols value of a function (Functions, Values of a Function, and Functions from One Class to Another §value) and ordered pair. Its symbols are used properly and $e(V,W)\in\mathbb{R}$ for all $V,W\in\mathcal{M}$: $W\in\operatorname{dom}\nu=\mathcal{M}$ and $\nu(W)\in\mathcal{M}$; so $(V,\nu(W))\in\mathcal{M}\times\mathcal{M}=\operatorname{dom}\oplus$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and Binary Operations on a Set §operation, and $V-W=\oplus((V,\nu(W)))\in\mathcal{M}$; so $V-W\in\operatorname{dom}\eta$ and $e(V,W)=\eta(V-W)=\lVert V-W\rVert\in\mathbb{R}$. Here domains are those of Functions, Values of a Function, and Functions from One Class to Another §map, and values lie in the codomains by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph. The lemma gives exactly one map $d:\mathcal{M}\times\mathcal{M}\to\mathbb{R}$ with $d((A,B))=e(A,B)=\lVert A-B\rVert$ for all $A,B\in\mathcal{M}$, that is, with $d(A,B)=\lVert A-B\rVert$, since $d(A,B)$ stands for $d((A,B))$ by Sets and Maps: Ordinary Notation §maps.