Proof of Concatenation Identifies a Product of Euclidean Spaces with a Euclidean Space

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

Clause index-split. $m+n\in\mathbb{N}$ and $[m]\subseteq[m+n]$ (Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §sum). For $j\in[n]$, $m+j\in[m+n]$ and $m+j\notin[m]$ (Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §shift). Every $k\in[m+n]$ lies in exactly one of $[m]$ and $\{m+j:j\in[n]\}$, and in the second case $m<k$ and $k=m+j$ for exactly one $j\in[n]$, namely $j=k-m$ (Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §cases).

Points of $\mathbb{R}^{m+n}$ are compared coordinatewise: by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality, two points of $\mathbb{R}^{p}$ are equal exactly when their components agree at every index of $[p]$, and by the clause index-split every $k\in[m+n]$ lies in $[m]$ or equals $m+j$ for exactly one $j\in[n]$, and not both; so for $\mathbb{R}^{m+n}$ it suffices to compare components at the indices $k\in[m]$ and $m+j$ with $j\in[n]$.

Preliminaries. By the clause index-split, $m+n\in\mathbb{N}$, so for each $p\in\{m,n,m+n\}$ the Euclidean space $\mathbb{R}^{p}$ is the set $\mathbb{R}^{[p]}$ of maps $[p]\to\mathbb{R}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §space and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. Let $\sigma:[n]\to[m+n]\setminus[m]$, $j\mapsto m+j$, be the bijection of the segment-split clause shift cited in the clause index-split. Its inverse $\rho=\sigma^{-1}:[m+n]\setminus[m]\to[n]$ is a bijective map with $\rho\circ\sigma=\mathrm{id}_{[n]}$ and $\sigma\circ\rho=\mathrm{id}_{[m+n]\setminus[m]}$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse); evaluating composites and identities by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\rho(m+j)=j$ for $j\in[n]$ and $m+\rho(k)=k$ for $k\in[m+n]\setminus[m]$.

For the clause concatenation, let $X=\mathbb{R}^m\times\mathbb{R}^n$. Both $X$ and $X\times[m+n]$ are sets by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. Let $\pi_{1}:X\to\mathbb{R}^{m}$ and $\pi_{2}:X\to\mathbb{R}^{n}$ be the projections of Projection, Evaluation and Currying Maps §projections, with $\mathbb{R}^{m}$ and $\mathbb{R}^{n}$ for its $X$ and $Y$, so that $\pi_{1}(\xi,\eta)=\xi$ and $\pi_{2}(\xi,\eta)=\eta$ for $\xi\in\mathbb{R}^{m}$ and $\eta\in\mathbb{R}^{n}$; and let $q_{1}:X\times[m+n]\to X$ and $q_{2}:X\times[m+n]\to[m+n]$ be the projections of the same clause, with $X$ and $[m+n]$ for its $X$ and $Y$, so that $q_{1}(u,k)=u$ and $q_{2}(u,k)=k$ for $u\in X$ and $k\in[m+n]$. For $p\in X\times[m+n]$ write $u=q_{1}(p)\in X$ and $k=q_{2}(p)\in[m+n]$; then $\pi_{1}u\in\mathbb{R}^{m}=\mathbb{R}^{[m]}$ and $\pi_{2}u\in\mathbb{R}^{n}=\mathbb{R}^{[n]}$, so $\pi_{1}u$ is a map $[m]\to\mathbb{R}$ and $\pi_{2}u$ a map $[n]\to\mathbb{R}$.

We apply Maps Defined by Cases §cases on $X\times[m+n]$. Its property is $q_{2}(p)\in[m]$, that is $k\in[m]$, which, for $p\in X\times[m+n]$, is expressed by the predicative formula $\exists z\,((p,z)\in q_{2}\wedge z\in[m])$, with $q_{2}$ and $[m]$ as parameters, as $p\in\operatorname{dom}q_{2}$ by Functions, Values of a Function, and Functions from One Class to Another §map. Its expressions are $t_{1}(p)=(\pi_{1}u)(k)$ and $t_{2}(p)=(\pi_{2}u)(\rho(k))$, with $u=q_{1}(p)$ and $k=q_{2}(p)$, built from the values of the maps $q_{1}$, $q_{2}$, $\pi_{1}$, $\pi_{2}$, $\rho$, $\pi_{1}u$ and $\pi_{2}u$; values of functions are defined set symbols by Functions, Values of a Function, and Functions from One Class to Another §value, a value $F(c)$ is used properly when $c\in\operatorname{dom}F$, and values of maps lie in their codomains. If $k\in[m]$, then $k\in[m]=\operatorname{dom}\pi_{1}u$, so $t_{1}(p)$ is used properly and lies in $\mathbb{R}$. If not, then $k\in[m+n]\setminus[m]=\operatorname{dom}\rho$ and $\rho(k)\in[n]=\operatorname{dom}\pi_{2}u$, so $t_{2}(p)$ is used properly and lies in $\mathbb{R}$. This gives a map $g:X\times[m+n]\to\mathbb{R}$ with $g(u,k)=(\pi_1u)(k)$ if $k\in[m]$ and $g(u,k)=(\pi_2u)(\rho(k))$ if $k\notin[m]$, for $u\in X$ and $k\in[m+n]$, and Projection, Evaluation and Currying Maps §currying gives a map $\iota:X\to\mathbb{R}^{[m+n]}=\mathbb{R}^{m+n}$ with $\iota(u)(k)=g(u,k)$ for $u\in X$ and $k\in[m+n]$.

Let $\xi\in\mathbb{R}^m$, $\eta\in\mathbb{R}^n$ and $w=\iota(\xi,\eta)$. As $\pi_1(\xi,\eta)=\xi$ and $\pi_2(\xi,\eta)=\eta$, $w_k=\xi_k$ for $k\in[m]$; and for $j\in[n]$, $m+j=\sigma(j)\in[m+n]\setminus[m]$, so $w_{m+j}=\eta_{\rho(m+j)}=\eta_j$. If $w'\in\mathbb{R}^{m+n}$ also has $w'_k=\xi_k$ for $k\in[m]$ and $w'_{m+j}=\eta_j$ for $j\in[n]$, then $w'_k=w_k$ for $k\in[m]$, and each $k\in[m+n]\setminus[m]$ equals $m+\rho(k)$ with $\rho(k)\in[n]$, so $w'_k=\eta_{\rho(k)}=w_k$; hence $w'=w$. So exactly one $w\in\mathbb{R}^{m+n}$ satisfies the conditions of the clause concatenation, $\iota$ sends $(\xi,\eta)$ to it, and every map $X\to\mathbb{R}^{m+n}$ doing the same has the values of $\iota$ and so equals $\iota$.

Claim 1. Injectivity. Let $(\xi,\eta),(\xi',\eta')\in\mathbb{R}^m\times\mathbb{R}^n$ with $\iota(\xi,\eta)=\iota(\xi',\eta')$. Comparing coordinates, $\xi_k=\iota(\xi,\eta)_k=\iota(\xi',\eta')_k=\xi'_k$ for $k\in[m]$ and $\eta_j=\iota(\xi,\eta)_{m+j}=\iota(\xi',\eta')_{m+j}=\eta'_j$ for $j\in[n]$, so $\xi=\xi'$ and $\eta=\eta'$, and $(\xi,\eta)=(\xi',\eta')$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic. So $\iota$ is injective.

Surjectivity. Let $w\in\mathbb{R}^{m+n}$, and let $\sigma:[n]\to[m+n]\setminus[m]$, $j\mapsto m+j$, be as in the preliminaries; as $[m+n]\setminus[m]\subseteq[m+n]$, $\sigma$ is also a map $[n]\to[m+n]$. Let $\xi=w|_{[m]}$ and $\eta=w\circ\sigma$. Since $[m]\subseteq[m+n]$ by the clause index-split, $\xi$ is a function with domain $[m]$ and $\xi_k=w_k\in\mathbb{R}$ for $k\in[m]$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction), and $\eta$ is a map $[n]\to\mathbb{R}$ with $\eta_j=w(\sigma(j))=w_{m+j}$ for $j\in[n]$; so $\xi\in\mathbb{R}^{[m]}=\mathbb{R}^m$ and $\eta\in\mathbb{R}^{[n]}=\mathbb{R}^n$. As $w_k=\xi_k$ for $k\in[m]$ and $w_{m+j}=\eta_j$ for $j\in[n]$, the uniqueness in the clause concatenation gives $\iota(\xi,\eta)=w$. So $\iota$ is surjective, hence bijective.

Inverse. As in the preliminaries, $\iota^{-1}:\mathbb{R}^{m+n}\to\mathbb{R}^m\times\mathbb{R}^n$ is a bijective map with $\iota^{-1}\circ\iota=\mathrm{id}_{\mathbb{R}^m\times\mathbb{R}^n}$. For $w\in\mathbb{R}^{m+n}$ and $(\xi,\eta)$ as in the surjectivity step, $\iota(\xi,\eta)=w$, so $\iota^{-1}(w)=\iota^{-1}(\iota(\xi,\eta))=(\xi,\eta)$, evaluating the composite and the identity. Thus $\iota^{-1}$ sends $w$ to the pair whose first entry has $k$th coordinate $w_k$ for $k\in[m]$ and whose second entry has $j$th coordinate $w_{m+j}$ for $j\in[n]$, which is the map described in claim 1.

Claim 2. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations, the $k$th component of $\iota(\xi,\eta)+\iota(\xi',\eta')$ is $\iota(\xi,\eta)_k+\iota(\xi',\eta')_k$. For $k\in[m]$ this is $\xi_k+\xi'_k=(\xi+\xi')_k$, which is the $k$th component of $\iota(\xi+\xi',\eta+\eta')$; at the index $m+j$ with $j\in[n]$ it is $\eta_j+\eta'_j=(\eta+\eta')_j$, which is the $(m+j)$th component of $\iota(\xi+\xi',\eta+\eta')$. This proves the first identity. The second and third are proved in the same way, using $(\lambda z)_k=\lambda z_k$ and $(z-z')_k=z_k-z'_k$ from the same clause.

Claim 3. Let $c:[m+n]\to\mathbb{R}$ be the pointwise product $k\mapsto\iota(\xi,\eta)_k\,\iota(\xi',\eta')_k$. By The Dot Product on $\mathbb{R}^n$ §dot-product,

$$\iota(\xi,\eta)\cdot\iota(\xi',\eta')=\sum_{k=1}^{m+n}c_k ,$$

a sum from $1$ to $m+n$. Addition on $\mathbb{R}$ is associative and commutative, so Splitting an Operation over the Segment [m+n] into [m] and a Shifted Copy of [n] §interval-split, applied to $+$ on $\mathbb{R}$ and $a=c$, gives

$$\sum_{k=1}^{m+n}c_k=\sum_{k=1}^{m}c_k+\sum_{j=1}^{n}c_{m+j},$$

in whichever reading the three sums from $1$ are taken, the first sum on the right being that of $c|_{[m]}$. For $k\in[m]$ we have $c_k=\xi_k\xi'_k$, so $c|_{[m]}$ is the pointwise product of $\xi$ and $\xi'$ and the first sum is $\xi\cdot\xi'$ by the same definition; for $j\in[n]$ we have $c_{m+j}=\eta_j\eta'_j$, so the second sum is $\eta\cdot\eta'$. This proves the first identity of claim 3.

By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, $\lVert z\rVert^{2}=z\cdot z$ in each Euclidean space. Taking $\xi'=\xi$ and $\eta'=\eta$ in the first identity therefore gives $\lVert\iota(\xi,\eta)\rVert^{2}=\lVert\xi\rVert^{2}+\lVert\eta\rVert^{2}$.

Claim 4. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance, $d_E(u,u')=\lVert u-u'\rVert$ in each Euclidean space. By claim 2, $\iota(z)-\iota(z')=\iota(\xi-\xi',\eta-\eta')$, so by claim 3

$$d_E\bigl(\iota(z),\iota(z')\bigr)^{2}=\lVert\iota(\xi-\xi',\eta-\eta')\rVert^{2}=\lVert\xi-\xi'\rVert^{2}+\lVert\eta-\eta'\rVert^{2}=d_E(\xi,\xi')^{2}+d_E(\eta,\eta')^{2},$$

which is the first assertion.

Write $\alpha=d_E(\xi,\xi')$, $\beta=d_E(\eta,\eta')$, $\gamma=d_E(\iota(z),\iota(z'))$ and $\mu=d_{\times}(z,z')$. These are nonnegative by Metric Space §nonnegative, since $d_E$ is a metric by $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence §metric and $d_{\times}$ is a metric by The Product Metric is a Metric §metric. By Product Metric on the Cartesian Product of Two Metric Spaces §value, $\mu=\max\{\alpha,\beta\}$; by The Product Metric is a Metric §domination, $\alpha\le\mu$ and $\beta\le\mu$; and since $\alpha\le\beta$ or $\beta\le\alpha$, The Maximum and Minimum of Two Elements of a Total Order §values gives $\mu=\beta$ or $\mu=\alpha$. The first assertion says $\gamma^{2}=\alpha^{2}+\beta^{2}$.

For the first inequality of the second assertion: $\mu$ is one of $\alpha,\beta$, and the square of the other is nonnegative by Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares §squares, so $\mu^{2}\le\alpha^{2}+\beta^{2}=\gamma^{2}$ by Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares §sum. As $\mu$ and $\gamma$ are nonnegative, $\mu\le\gamma$ (Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff, with exponent $2$ in the ordered field $\mathbb{R}$).

For the second inequality: $0\le\alpha\le\mu$ and $0\le\beta\le\mu$ give $\alpha^{2}\le\mu^{2}$ and $\beta^{2}\le\mu^{2}$ by Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares §product, so $\gamma^{2}=\alpha^{2}+\beta^{2}\le\mu^{2}+\mu^{2}$ by the rule for sums used above. Moreover $(\mu+\mu)^{2}=(\mu^{2}+\mu^{2})+(\mu\,\mu+\mu\,\mu)$ by field arithmetic, and $0\le\mu\,\mu+\mu\,\mu$ by the rules for squares and sums, so $\mu^{2}+\mu^{2}\le(\mu+\mu)^{2}$. Hence $\gamma^{2}\le(\mu+\mu)^{2}$. Since $\gamma$ and $\mu+\mu$ are nonnegative, the latter as a sum of nonnegative reals, $\gamma\le\mu+\mu$, by the monotonicity of squaring used above.