Proof of Absolute Value and Squaring as Maps on the Reals, and Entrywise Absolute Values and Squares of a Real Matrix

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

By The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum §ordered-field, $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field, so the results on ordered fields cited below apply to it; and $\mathbb{R}$ is a set by The Real Numbers §reals.

Clause absolute-value. Apply Maps and Relations Given by Formulas §map with $\mathbb{R}$ for its $a$ and $b$ and the expression $|u|$, which lies in $\mathbb{R}$ for $u\in\mathbb{R}$. The symbol $|u|$ is used properly at every $u\in\mathbb{R}$: there $|u|$ is uniquely determined by Absolute Value in an Ordered Field §absolute-value, and the condition $u\in\mathbb{R}\wedge z=|u|$ is equivalent to a predicative formula 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 §absolute-value-formula, with $u$ and $z$ for its $x$ and $z$ and with $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ as the values of its $t_{1},\dots,t_{6}$; so $|u|$ is a defined set symbol with argument $u$, used properly where $u\in\mathbb{R}$. The lemma gives exactly one map $a:\mathbb{R}\to\mathbb{R}$ with $a(u)=|u|$ for every $u\in\mathbb{R}$.

Clause square. The multiplication $\cdot$ is a binary operation on $\mathbb{R}$, so for $u\in\mathbb{R}$ the product $u\cdot u$ is the value of $\cdot$ at $(u,u)$, a defined set symbol, and lies in $\mathbb{R}$, by Binary Operations on a Set §notation; it is the unique set $z$ with $((u,u),z)\in{\cdot}$, a predicative formula by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §operation-membership, and it is used properly where $u\in\mathbb{R}$. Apply Maps and Relations Given by Formulas §map with $\mathbb{R}$ for its $a$ and $b$ and the expression $u\cdot u$: there is exactly one map $q:\mathbb{R}\to\mathbb{R}$ with $q(u)=u\cdot u=u^{2}$ for every $u\in\mathbb{R}$.

Clause entrywise. By Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, $A$ is a map $A:[m]\times[n]\to\mathbb{R}$, and $\mathcal{M}_{m\times n}(\mathbb{R})$ is the set of these maps, so a set lies in $\mathcal{M}_{m\times n}(\mathbb{R})$ if and only if it is a map $[m]\times[n]\to\mathbb{R}$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, applied to $A$ and the map $a$ of the clause absolute-value, the composite $a\circ A$ is a map $[m]\times[n]\to\mathbb{R}$ with $(a\circ A)((i,j))=a(A((i,j)))$ for $(i,j)\in[m]\times[n]$; so $a\circ A\in\mathcal{M}_{m\times n}(\mathbb{R})$, and by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries, for $i\in[m]$ and $j\in[n]$, $(a\circ A)_{ij}=a(A_{ij})=|A_{ij}|$, as $A_{ij}\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph. Likewise $q\circ A\in\mathcal{M}_{m\times n}(\mathbb{R})$ with $(q\circ A)_{ij}=q(A_{ij})=A_{ij}^{2}$. If $N\in\mathcal{M}_{m\times n}(\mathbb{R})$ also has $N_{ij}=|A_{ij}|$ for all $i\in[m]$ and $j\in[n]$, then $N$ and $a\circ A$ have the same entries, so $N=a\circ A$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality; the same argument applies to $q\circ A$. So $a\circ A$ and $q\circ A$ are the only matrices in $\mathcal{M}_{m\times n}(\mathbb{R})$ with the stated entries.