# Metamath Proof Explorer

## Theorem ismet2

Description: An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion ismet2 ${⊢}{D}\in \mathrm{Met}\left({X}\right)↔\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)$

### Proof

Step Hyp Ref Expression
1 elfvex ${⊢}{D}\in \mathrm{Met}\left({X}\right)\to {X}\in \mathrm{V}$
2 elfvex ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in \mathrm{V}$
3 2 adantr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)\to {X}\in \mathrm{V}$
4 simpllr ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {D}:{X}×{X}⟶ℝ$
5 simpr ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {z}\in {X}$
6 simplrl ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {x}\in {X}$
7 4 5 6 fovrnd ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {z}{D}{x}\in ℝ$
8 simplrr ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {y}\in {X}$
9 4 5 8 fovrnd ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to {z}{D}{y}\in ℝ$
10 7 9 rexaddd ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\to \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)=\left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
11 10 breq2d ${⊢}\left(\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {z}\in {X}\right)\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)$
12 11 ralbidva ${⊢}\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\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)$
13 12 anbi2d ${⊢}\left(\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\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)$
14 13 2ralbidva ${⊢}\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\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)$
15 simpr ${⊢}\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\to {D}:{X}×{X}⟶ℝ$
16 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
17 fss ${⊢}\left({D}:{X}×{X}⟶ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
18 15 16 17 sylancl ${⊢}\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
19 18 biantrurd ${⊢}\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\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)↔\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)$
20 14 19 bitr3d ${⊢}\left({X}\in \mathrm{V}\wedge {D}:{X}×{X}⟶ℝ\right)\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)↔\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)$
21 20 pm5.32da ${⊢}{X}\in \mathrm{V}\to \left(\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)↔\left({D}:{X}×{X}⟶ℝ\wedge \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)\right)$
22 21 biancomd ${⊢}{X}\in \mathrm{V}\to \left(\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)↔\left(\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)\wedge {D}:{X}×{X}⟶ℝ\right)\right)$
23 ismet ${⊢}{X}\in \mathrm{V}\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)$
24 isxmet ${⊢}{X}\in \mathrm{V}\to \left({D}\in \mathrm{\infty 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)$
25 24 anbi1d ${⊢}{X}\in \mathrm{V}\to \left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)↔\left(\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)\wedge {D}:{X}×{X}⟶ℝ\right)\right)$
26 22 23 25 3bitr4d ${⊢}{X}\in \mathrm{V}\to \left({D}\in \mathrm{Met}\left({X}\right)↔\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)\right)$
27 1 3 26 pm5.21nii ${⊢}{D}\in \mathrm{Met}\left({X}\right)↔\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)$