Proof of The Product Metric is a Metric

The order $\le$ of $\mathbb{R}$ is a total order, $\mathbb{R}$ being an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals and Ordered Fields §ordered-field; so The Maximum and Minimum of Two Elements of a Total Order applies to it, it is reflexive, antisymmetric and transitive by Partial and Total Orders on a Set and the Associated Strict Relation §partial, and Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders applies to its strict relation $<$. By Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, $x_{1},x_{2}\in X$ and $y_{1},y_{2}\in Y$. Write $s=d_{X}(x_{1},x_{2})$ and $t=d_{Y}(y_{1},y_{2})$; by Product Metric on the Cartesian Product of Two Metric Spaces §value, $d_{X\times Y}(p,q)=\max\{s,t\}$.

Clause domination. By The Maximum and Minimum of Two Elements of a Total Order §bounds, $s\le\max\{s,t\}$ and $t\le\max\{s,t\}$.

Clause strict-bounds. If $\max\{s,t\}<r$, then $s<r$ and $t<r$ by the clause domination and Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §mixed. Conversely, let $s<r$ and $t<r$. By totality $s\le t$ or $t\le s$, and then The Maximum and Minimum of Two Elements of a Total Order §values gives $\max\{s,t\}=t$, respectively $\max\{s,t\}=s$; in either case $\max\{s,t\}<r$.

Clause metric. The map $d_{X\times Y}:(X\times Y)\times(X\times Y)\to\mathbb{R}$ is given by Product Metric on the Cartesian Product of Two Metric Spaces §product-metric. Every point of $X\times Y$ is an ordered pair $(u,v)$ with $u\in X$ and $v\in Y$, by The Cartesian Product of Two Classes §product, and $p$ and $q$ are arbitrary such points; so it suffices to verify the conditions of Metric Space §metric for $p$, $q$ and a further point $w=(x_{3},y_{3})$ with $x_{3}\in X$ and $y_{3}\in Y$. The clauses domination and strict-bounds, proved above for arbitrary points, apply to every pair of points.

Nonnegative. By Metric Space §nonnegative for $d_{X}$, $0\le s$, and $s\le d_{X\times Y}(p,q)$ by the clause domination; by transitivity, $0\le d_{X\times Y}(p,q)$.

Zero. Suppose $d_{X\times Y}(p,q)=0$. The clause domination gives $s\le0$ and $t\le0$, and Metric Space §nonnegative gives $0\le s$ and $0\le t$, so $s=0$ and $t=0$ by antisymmetry. Then Metric Space §zero for $d_{X}$ and $d_{Y}$ gives $x_{1}=x_{2}$ and $y_{1}=y_{2}$, that is $p=q$. Conversely, suppose $p=q$. Then $x_{1}=x_{2}$ and $y_{1}=y_{2}$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, so $s=0$ and $t=0$ by Metric Space §zero; as $0\le0$ by reflexivity, The Maximum and Minimum of Two Elements of a Total Order §values gives $d_{X\times Y}(p,q)=\max\{0,0\}=0$.

Symmetric. By Product Metric on the Cartesian Product of Two Metric Spaces §value and Metric Space §symmetric for $d_{X}$ and $d_{Y}$,

$$d_{X\times Y}(q,p)=\max\{d_{X}(x_{2},x_{1}),d_{Y}(y_{2},y_{1})\}=\max\{s,t\}=d_{X\times Y}(p,q).$$

Triangle. Put $a=d_{X\times Y}(p,q)+d_{X\times Y}(q,w)$. By Metric Space §triangle for $d_{X}$,

$$d_{X}(x_{1},x_{3})\le d_{X}(x_{1},x_{2})+d_{X}(x_{2},x_{3}),$$

and the clause domination for the pairs $p,q$ and $q,w$ gives $d_{X}(x_{1},x_{2})\le d_{X\times Y}(p,q)$ and $d_{X}(x_{2},x_{3})\le d_{X\times Y}(q,w)$; so Rules of Arithmetic and Order in an Ordered Field §order-sum gives $d_{X}(x_{1},x_{2})+d_{X}(x_{2},x_{3})\le a$, and then transitivity gives $d_{X}(x_{1},x_{3})\le a$. In the same way, with Metric Space §triangle for $d_{Y}$, $d_{Y}(y_{1},y_{3})\le a$. By Product Metric on the Cartesian Product of Two Metric Spaces §value and The Maximum and Minimum of Two Elements of a Total Order §least-upper,

$$d_{X\times Y}(p,w)=\max\{d_{X}(x_{1},x_{3}),d_{Y}(y_{1},y_{3})\}\le a .$$

Hence $d_{X\times Y}$ is a metric on $X\times Y$ by Metric Space §metric; as $X\times Y$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, $(X\times Y,d_{X\times Y})$ is a metric space by Metric Space §metric-space.