Metamath Proof Explorer

Theorem stdbdmet

Description: The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis stdbdmet.1 ${⊢}{D}=\left({x}\in {X},{y}\in {X}⟼if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
Assertion stdbdmet ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\to {D}\in \mathrm{Met}\left({X}\right)$

Proof

Step Hyp Ref Expression
1 stdbdmet.1 ${⊢}{D}=\left({x}\in {X},{y}\in {X}⟼if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
2 rpxr ${⊢}{R}\in {ℝ}^{+}\to {R}\in {ℝ}^{*}$
3 rpgt0 ${⊢}{R}\in {ℝ}^{+}\to 0<{R}$
4 2 3 jca ${⊢}{R}\in {ℝ}^{+}\to \left({R}\in {ℝ}^{*}\wedge 0<{R}\right)$
5 1 stdbdxmet ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
6 5 3expb ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({R}\in {ℝ}^{*}\wedge 0<{R}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
7 4 6 sylan2 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
8 xmetcl ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{C}{y}\in {ℝ}^{*}$
9 8 3expb ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{C}{y}\in {ℝ}^{*}$
10 9 adantlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{C}{y}\in {ℝ}^{*}$
11 2 ad2antlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}\in {ℝ}^{*}$
12 10 11 ifcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in {ℝ}^{*}$
13 rpre ${⊢}{R}\in {ℝ}^{+}\to {R}\in ℝ$
14 13 ad2antlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {R}\in ℝ$
15 xmetge0 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to 0\le {x}{C}{y}$
16 15 3expb ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to 0\le {x}{C}{y}$
17 16 adantlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to 0\le {x}{C}{y}$
18 rpge0 ${⊢}{R}\in {ℝ}^{+}\to 0\le {R}$
19 18 ad2antlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to 0\le {R}$
20 breq2 ${⊢}{x}{C}{y}=if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\to \left(0\le {x}{C}{y}↔0\le if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
21 breq2 ${⊢}{R}=if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\to \left(0\le {R}↔0\le if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
22 20 21 ifboth ${⊢}\left(0\le {x}{C}{y}\wedge 0\le {R}\right)\to 0\le if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)$
23 17 19 22 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to 0\le if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)$
24 xrmin2 ${⊢}\left({x}{C}{y}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\le {R}$
25 10 11 24 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\le {R}$
26 xrrege0 ${⊢}\left(\left(if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in {ℝ}^{*}\wedge {R}\in ℝ\right)\wedge \left(0\le if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\wedge if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\le {R}\right)\right)\to if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in ℝ$
27 12 14 23 25 26 syl22anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in ℝ$
28 27 ralrimivva ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in ℝ$
29 1 fmpo ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\in ℝ↔{D}:{X}×{X}⟶ℝ$
30 28 29 sylib ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\to {D}:{X}×{X}⟶ℝ$
31 ismet2 ${⊢}{D}\in \mathrm{Met}\left({X}\right)↔\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {D}:{X}×{X}⟶ℝ\right)$
32 7 30 31 sylanbrc ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{+}\right)\to {D}\in \mathrm{Met}\left({X}\right)$