# Metamath Proof Explorer

## Theorem prdsmet

Description: The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsmet.y ${⊢}{Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\right)$
prdsmet.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
prdsmet.v ${⊢}{V}={\mathrm{Base}}_{{R}}$
prdsmet.e ${⊢}{E}={\mathrm{dist}\left({R}\right)↾}_{\left({V}×{V}\right)}$
prdsmet.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
prdsmet.s ${⊢}{\phi }\to {S}\in {W}$
prdsmet.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
prdsmet.r ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {R}\in {Z}$
prdsmet.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
Assertion prdsmet ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 prdsmet.y ${⊢}{Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\right)$
2 prdsmet.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 prdsmet.v ${⊢}{V}={\mathrm{Base}}_{{R}}$
4 prdsmet.e ${⊢}{E}={\mathrm{dist}\left({R}\right)↾}_{\left({V}×{V}\right)}$
5 prdsmet.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
6 prdsmet.s ${⊢}{\phi }\to {S}\in {W}$
7 prdsmet.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
8 prdsmet.r ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {R}\in {Z}$
9 prdsmet.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
10 metxmet ${⊢}{E}\in \mathrm{Met}\left({V}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
11 9 10 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
12 1 2 3 4 5 6 7 8 11 prdsxmet ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({B}\right)$
13 1 2 3 4 5 6 7 8 11 prdsdsf ${⊢}{\phi }\to {D}:{B}×{B}⟶\left[0,\mathrm{+\infty }\right]$
14 13 ffnd ${⊢}{\phi }\to {D}Fn\left({B}×{B}\right)$
15 6 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {S}\in {W}$
16 7 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {I}\in \mathrm{Fin}$
17 8 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\in {Z}$
18 17 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\in {Z}$
19 simprl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}\in {B}$
20 simprr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {g}\in {B}$
21 1 2 15 16 18 19 20 3 4 5 prdsdsval3 ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}{D}{g}=sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$
22 1 2 15 16 18 3 19 prdsbascl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {V}$
23 1 2 15 16 18 3 20 prdsbascl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}$
24 r19.26 ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)↔\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}\right)$
25 metcl ${⊢}\left({E}\in \mathrm{Met}\left({V}\right)\wedge {f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ$
26 25 3expib ${⊢}{E}\in \mathrm{Met}\left({V}\right)\to \left(\left({f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\right)$
27 9 26 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left(\left({f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\right)$
28 27 ralimdva ${⊢}{\phi }\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\right)$
29 28 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\right)$
30 24 29 syl5bir ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left(\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\right)$
31 22 23 30 mp2and ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in ℝ$
32 eqid ${⊢}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)$
33 32 fmpt ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in ℝ↔\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right):{I}⟶ℝ$
34 31 33 sylib ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right):{I}⟶ℝ$
35 34 frnd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\subseteq ℝ$
36 0red ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to 0\in ℝ$
37 36 snssd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left\{0\right\}\subseteq ℝ$
38 35 37 unssd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq ℝ$
39 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
40 39 a1i ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to <\mathrm{Or}{ℝ}^{*}$
41 mptfi ${⊢}{I}\in \mathrm{Fin}\to \left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\in \mathrm{Fin}$
42 rnfi ${⊢}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\in \mathrm{Fin}\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\in \mathrm{Fin}$
43 16 41 42 3syl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\in \mathrm{Fin}$
44 snfi ${⊢}\left\{0\right\}\in \mathrm{Fin}$
45 unfi ${⊢}\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\in \mathrm{Fin}\wedge \left\{0\right\}\in \mathrm{Fin}\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\in \mathrm{Fin}$
46 43 44 45 sylancl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\in \mathrm{Fin}$
47 ssun2 ${⊢}\left\{0\right\}\subseteq \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}$
48 c0ex ${⊢}0\in \mathrm{V}$
49 48 snss ${⊢}0\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)↔\left\{0\right\}\subseteq \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}$
50 47 49 mpbir ${⊢}0\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)$
51 ne0i ${⊢}0\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\ne \varnothing$
52 50 51 mp1i ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\ne \varnothing$
53 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
54 38 53 sstrdi ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq {ℝ}^{*}$
55 fisupcl ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\in \mathrm{Fin}\wedge \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\ne \varnothing \wedge \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq {ℝ}^{*}\right)\right)\to sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)$
56 40 46 52 54 55 syl13anc ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)$
57 38 56 sseldd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\in ℝ$
58 21 57 eqeltrd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}{D}{g}\in ℝ$
59 58 ralrimivva ${⊢}{\phi }\to \forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}{f}{D}{g}\in ℝ$
60 ffnov ${⊢}{D}:{B}×{B}⟶ℝ↔\left({D}Fn\left({B}×{B}\right)\wedge \forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}{f}{D}{g}\in ℝ\right)$
61 14 59 60 sylanbrc ${⊢}{\phi }\to {D}:{B}×{B}⟶ℝ$
62 ismet2 ${⊢}{D}\in \mathrm{Met}\left({B}\right)↔\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {D}:{B}×{B}⟶ℝ\right)$
63 12 61 62 sylanbrc ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({B}\right)$