# Metamath Proof Explorer

## Theorem xpsmet

Description: The direct product of two metric spaces. Definition 14-1.5 of Gleason p. 225. (Contributed by NM, 20-Jun-2007) (Revised by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xpsds.t ${⊢}{T}={R}{×}_{𝑠}{S}$
xpsds.x ${⊢}{X}={\mathrm{Base}}_{{R}}$
xpsds.y ${⊢}{Y}={\mathrm{Base}}_{{S}}$
xpsds.1 ${⊢}{\phi }\to {R}\in {V}$
xpsds.2 ${⊢}{\phi }\to {S}\in {W}$
xpsds.p ${⊢}{P}=\mathrm{dist}\left({T}\right)$
xpsds.m ${⊢}{M}={\mathrm{dist}\left({R}\right)↾}_{\left({X}×{X}\right)}$
xpsds.n ${⊢}{N}={\mathrm{dist}\left({S}\right)↾}_{\left({Y}×{Y}\right)}$
xpsmet.3 ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
xpsmet.4 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({Y}\right)$
Assertion xpsmet ${⊢}{\phi }\to {P}\in \mathrm{Met}\left({X}×{Y}\right)$

### Proof

Step Hyp Ref Expression
1 xpsds.t ${⊢}{T}={R}{×}_{𝑠}{S}$
2 xpsds.x ${⊢}{X}={\mathrm{Base}}_{{R}}$
3 xpsds.y ${⊢}{Y}={\mathrm{Base}}_{{S}}$
4 xpsds.1 ${⊢}{\phi }\to {R}\in {V}$
5 xpsds.2 ${⊢}{\phi }\to {S}\in {W}$
6 xpsds.p ${⊢}{P}=\mathrm{dist}\left({T}\right)$
7 xpsds.m ${⊢}{M}={\mathrm{dist}\left({R}\right)↾}_{\left({X}×{X}\right)}$
8 xpsds.n ${⊢}{N}={\mathrm{dist}\left({S}\right)↾}_{\left({Y}×{Y}\right)}$
9 xpsmet.3 ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
10 xpsmet.4 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({Y}\right)$
11 eqid ${⊢}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)=\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
12 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
13 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}$
14 1 2 3 4 5 11 12 13 xpsval ${⊢}{\phi }\to {T}={\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
15 1 2 3 4 5 11 12 13 xpsrnbas ${⊢}{\phi }\to \mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}$
16 11 xpsff1o2 ${⊢}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{X}×{Y}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
17 f1ocnv ${⊢}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{X}×{Y}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\to {\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\underset{1-1 onto}{⟶}{X}×{Y}$
18 16 17 mp1i ${⊢}{\phi }\to {\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\underset{1-1 onto}{⟶}{X}×{Y}$
19 ovexd ${⊢}{\phi }\to \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\in \mathrm{V}$
20 eqid ${⊢}{\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)↾}_{\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)×\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)}={\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)↾}_{\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)×\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)}$
21 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)$
22 eqid ${⊢}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}$
23 eqid ${⊢}{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}$
24 eqid ${⊢}{\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}={\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}$
25 eqid ${⊢}\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)$
26 fvexd ${⊢}{\phi }\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
27 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
28 nnfi ${⊢}{2}_{𝑜}\in \mathrm{\omega }\to {2}_{𝑜}\in \mathrm{Fin}$
29 27 28 mp1i ${⊢}{\phi }\to {2}_{𝑜}\in \mathrm{Fin}$
30 fvexd ${⊢}\left({\phi }\wedge {k}\in {2}_{𝑜}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\in \mathrm{V}$
31 elpri ${⊢}{k}\in \left\{\varnothing ,{1}_{𝑜}\right\}\to \left({k}=\varnothing \vee {k}={1}_{𝑜}\right)$
32 df2o3 ${⊢}{2}_{𝑜}=\left\{\varnothing ,{1}_{𝑜}\right\}$
33 31 32 eleq2s ${⊢}{k}\in {2}_{𝑜}\to \left({k}=\varnothing \vee {k}={1}_{𝑜}\right)$
34 9 adantr ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {M}\in \mathrm{Met}\left({X}\right)$
35 fveq2 ${⊢}{k}=\varnothing \to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)=\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)$
36 fvpr0o ${⊢}{R}\in {V}\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)={R}$
37 4 36 syl ${⊢}{\phi }\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)={R}$
38 35 37 sylan9eqr ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)={R}$
39 38 fveq2d ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to \mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)=\mathrm{dist}\left({R}\right)$
40 38 fveq2d ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={\mathrm{Base}}_{{R}}$
41 40 2 syl6eqr ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={X}$
42 41 sqxpeqd ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={X}×{X}$
43 39 42 reseq12d ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}={\mathrm{dist}\left({R}\right)↾}_{\left({X}×{X}\right)}$
44 43 7 syl6eqr ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}={M}$
45 41 fveq2d ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)=\mathrm{Met}\left({X}\right)$
46 34 44 45 3eltr4d ${⊢}\left({\phi }\wedge {k}=\varnothing \right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)$
47 10 adantr ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {N}\in \mathrm{Met}\left({Y}\right)$
48 fveq2 ${⊢}{k}={1}_{𝑜}\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)=\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)$
49 fvpr1o ${⊢}{S}\in {W}\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)={S}$
50 5 49 syl ${⊢}{\phi }\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)={S}$
51 48 50 sylan9eqr ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)={S}$
52 51 fveq2d ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to \mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)=\mathrm{dist}\left({S}\right)$
53 51 fveq2d ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={\mathrm{Base}}_{{S}}$
54 53 3 syl6eqr ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={Y}$
55 54 sqxpeqd ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}={Y}×{Y}$
56 52 55 reseq12d ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}={\mathrm{dist}\left({S}\right)↾}_{\left({Y}×{Y}\right)}$
57 56 8 syl6eqr ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}={N}$
58 54 fveq2d ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)=\mathrm{Met}\left({Y}\right)$
59 47 57 58 3eltr4d ${⊢}\left({\phi }\wedge {k}={1}_{𝑜}\right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)$
60 46 59 jaodan ${⊢}\left({\phi }\wedge \left({k}=\varnothing \vee {k}={1}_{𝑜}\right)\right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)$
61 33 60 sylan2 ${⊢}\left({\phi }\wedge {k}\in {2}_{𝑜}\right)\to {\mathrm{dist}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)↾}_{\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}×{\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)}\in \mathrm{Met}\left({\mathrm{Base}}_{\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)}\right)$
62 21 22 23 24 25 26 29 30 61 prdsmet ${⊢}{\phi }\to \mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)\in \mathrm{Met}\left({\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}\right)$
63 fnpr2o ${⊢}\left({R}\in {V}\wedge {S}\in {W}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}$
64 4 5 63 syl2anc ${⊢}{\phi }\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}$
65 dffn5 ${⊢}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}↔\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)$
66 64 65 sylib ${⊢}{\phi }\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)$
67 66 oveq2d ${⊢}{\phi }\to \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)$
68 67 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)=\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)$
69 67 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}$
70 15 69 eqtrd ${⊢}{\phi }\to \mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}$
71 70 fveq2d ${⊢}{\phi }\to \mathrm{Met}\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({k}\in {2}_{𝑜}⟼\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({k}\right)\right)\right)}\right)$
72 62 68 71 3eltr4d ${⊢}{\phi }\to \mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\in \mathrm{Met}\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)$
73 ssid ${⊢}\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\subseteq \mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
74 metres2 ${⊢}\left(\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\in \mathrm{Met}\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)\wedge \mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\subseteq \mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)\to {\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)↾}_{\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)×\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)}\in \mathrm{Met}\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)$
75 72 73 74 sylancl ${⊢}{\phi }\to {\mathrm{dist}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)↾}_{\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)×\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)}\in \mathrm{Met}\left(\mathrm{ran}\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)\right)$
76 14 15 18 19 20 6 75 imasf1omet ${⊢}{\phi }\to {P}\in \mathrm{Met}\left({X}×{Y}\right)$