# Metamath Proof Explorer

## Theorem ismet

Description: Express the predicate " D is a metric." (Contributed by NM, 25-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ismet ${⊢}{X}\in {A}\to \left({D}\in \mathrm{Met}\left({X}\right)↔\left({D}:{X}×{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{X}\in {A}\to {X}\in \mathrm{V}$
2 xpeq12 ${⊢}\left({t}={X}\wedge {t}={X}\right)\to {t}×{t}={X}×{X}$
3 2 anidms ${⊢}{t}={X}\to {t}×{t}={X}×{X}$
4 3 oveq2d ${⊢}{t}={X}\to {ℝ}^{\left({t}×{t}\right)}={ℝ}^{\left({X}×{X}\right)}$
5 raleq ${⊢}{t}={X}\to \left(\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)$
6 5 anbi2d ${⊢}{t}={X}\to \left(\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)↔\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right)$
7 6 raleqbi1dv ${⊢}{t}={X}\to \left(\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right)$
8 7 raleqbi1dv ${⊢}{t}={X}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right)$
9 4 8 rabeqbidv ${⊢}{t}={X}\to \left\{{d}\in \left({ℝ}^{\left({t}×{t}\right)}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}=\left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}$
10 df-met ${⊢}\mathrm{Met}=\left({t}\in \mathrm{V}⟼\left\{{d}\in \left({ℝ}^{\left({t}×{t}\right)}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}\right)$
11 ovex ${⊢}{ℝ}^{\left({X}×{X}\right)}\in \mathrm{V}$
12 11 rabex ${⊢}\left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}\in \mathrm{V}$
13 9 10 12 fvmpt ${⊢}{X}\in \mathrm{V}\to \mathrm{Met}\left({X}\right)=\left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}$
14 1 13 syl ${⊢}{X}\in {A}\to \mathrm{Met}\left({X}\right)=\left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}$
15 14 eleq2d ${⊢}{X}\in {A}\to \left({D}\in \mathrm{Met}\left({X}\right)↔{D}\in \left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}\right)$
16 oveq ${⊢}{d}={D}\to {x}{d}{y}={x}{D}{y}$
17 16 eqeq1d ${⊢}{d}={D}\to \left({x}{d}{y}=0↔{x}{D}{y}=0\right)$
18 17 bibi1d ${⊢}{d}={D}\to \left(\left({x}{d}{y}=0↔{x}={y}\right)↔\left({x}{D}{y}=0↔{x}={y}\right)\right)$
19 oveq ${⊢}{d}={D}\to {z}{d}{x}={z}{D}{x}$
20 oveq ${⊢}{d}={D}\to {z}{d}{y}={z}{D}{y}$
21 19 20 oveq12d ${⊢}{d}={D}\to \left({z}{d}{x}\right)+\left({z}{d}{y}\right)=\left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
22 16 21 breq12d ${⊢}{d}={D}\to \left({x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)↔{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)$
23 22 ralbidv ${⊢}{d}={D}\to \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)$
24 18 23 anbi12d ${⊢}{d}={D}\to \left(\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)↔\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)$
25 24 2ralbidv ${⊢}{d}={D}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)$
26 25 elrab ${⊢}{D}\in \left\{{d}\in \left({ℝ}^{\left({X}×{X}\right)}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{d}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{d}{y}\le \left({z}{d}{x}\right)+\left({z}{d}{y}\right)\right)\right\}↔\left({D}\in \left({ℝ}^{\left({X}×{X}\right)}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)$
27 15 26 syl6bb ${⊢}{X}\in {A}\to \left({D}\in \mathrm{Met}\left({X}\right)↔\left({D}\in \left({ℝ}^{\left({X}×{X}\right)}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)\right)$
28 reex ${⊢}ℝ\in \mathrm{V}$
29 sqxpexg ${⊢}{X}\in {A}\to {X}×{X}\in \mathrm{V}$
30 elmapg ${⊢}\left(ℝ\in \mathrm{V}\wedge {X}×{X}\in \mathrm{V}\right)\to \left({D}\in \left({ℝ}^{\left({X}×{X}\right)}\right)↔{D}:{X}×{X}⟶ℝ\right)$
31 28 29 30 sylancr ${⊢}{X}\in {A}\to \left({D}\in \left({ℝ}^{\left({X}×{X}\right)}\right)↔{D}:{X}×{X}⟶ℝ\right)$
32 31 anbi1d ${⊢}{X}\in {A}\to \left(\left({D}\in \left({ℝ}^{\left({X}×{X}\right)}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)↔\left({D}:{X}×{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)\right)$
33 27 32 bitrd ${⊢}{X}\in {A}\to \left({D}\in \mathrm{Met}\left({X}\right)↔\left({D}:{X}×{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)\right)$