# Metamath Proof Explorer

## Theorem stdbdbl

Description: The standard bounded metric corresponding to C generates the same balls as C for radii less than R . (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 stdbdbl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {P}\mathrm{ball}\left({D}\right){S}={P}\mathrm{ball}\left({C}\right){S}$

### 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 simpll2 ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {R}\in {ℝ}^{*}$
3 simpr1 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {P}\in {X}$
4 3 adantr ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {P}\in {X}$
5 simpr ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {z}\in {X}$
6 1 stdbdmetval ${⊢}\left({R}\in {ℝ}^{*}\wedge {P}\in {X}\wedge {z}\in {X}\right)\to {P}{D}{z}=if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)$
7 2 4 5 6 syl3anc ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {P}{D}{z}=if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)$
8 7 breq1d ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({P}{D}{z}<{S}↔if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)<{S}\right)$
9 simplr3 ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {S}\le {R}$
10 9 biantrud ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({S}\le {P}{C}{z}↔\left({S}\le {P}{C}{z}\wedge {S}\le {R}\right)\right)$
11 simpr2 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {S}\in {ℝ}^{*}$
12 11 adantr ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {S}\in {ℝ}^{*}$
13 simpl1 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {C}\in \mathrm{\infty Met}\left({X}\right)$
14 13 adantr ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {C}\in \mathrm{\infty Met}\left({X}\right)$
15 xmetcl ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {z}\in {X}\right)\to {P}{C}{z}\in {ℝ}^{*}$
16 14 4 5 15 syl3anc ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to {P}{C}{z}\in {ℝ}^{*}$
17 xrlemin ${⊢}\left({S}\in {ℝ}^{*}\wedge {P}{C}{z}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to \left({S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)↔\left({S}\le {P}{C}{z}\wedge {S}\le {R}\right)\right)$
18 12 16 2 17 syl3anc ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)↔\left({S}\le {P}{C}{z}\wedge {S}\le {R}\right)\right)$
19 10 18 bitr4d ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({S}\le {P}{C}{z}↔{S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\right)$
20 19 notbid ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left(¬{S}\le {P}{C}{z}↔¬{S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\right)$
21 xrltnle ${⊢}\left({P}{C}{z}\in {ℝ}^{*}\wedge {S}\in {ℝ}^{*}\right)\to \left({P}{C}{z}<{S}↔¬{S}\le {P}{C}{z}\right)$
22 16 12 21 syl2anc ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({P}{C}{z}<{S}↔¬{S}\le {P}{C}{z}\right)$
23 16 2 ifcld ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\in {ℝ}^{*}$
24 xrltnle ${⊢}\left(if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\in {ℝ}^{*}\wedge {S}\in {ℝ}^{*}\right)\to \left(if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)<{S}↔¬{S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\right)$
25 23 12 24 syl2anc ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left(if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)<{S}↔¬{S}\le if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)\right)$
26 20 22 25 3bitr4d ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({P}{C}{z}<{S}↔if\left({P}{C}{z}\le {R},{P}{C}{z},{R}\right)<{S}\right)$
27 8 26 bitr4d ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\wedge {z}\in {X}\right)\to \left({P}{D}{z}<{S}↔{P}{C}{z}<{S}\right)$
28 27 rabbidva ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to \left\{{z}\in {X}|{P}{D}{z}<{S}\right\}=\left\{{z}\in {X}|{P}{C}{z}<{S}\right\}$
29 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)$
30 29 adantr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
31 blval ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {S}\in {ℝ}^{*}\right)\to {P}\mathrm{ball}\left({D}\right){S}=\left\{{z}\in {X}|{P}{D}{z}<{S}\right\}$
32 30 3 11 31 syl3anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {P}\mathrm{ball}\left({D}\right){S}=\left\{{z}\in {X}|{P}{D}{z}<{S}\right\}$
33 blval ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {S}\in {ℝ}^{*}\right)\to {P}\mathrm{ball}\left({C}\right){S}=\left\{{z}\in {X}|{P}{C}{z}<{S}\right\}$
34 13 3 11 33 syl3anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {P}\mathrm{ball}\left({C}\right){S}=\left\{{z}\in {X}|{P}{C}{z}<{S}\right\}$
35 28 32 34 3eqtr4d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({P}\in {X}\wedge {S}\in {ℝ}^{*}\wedge {S}\le {R}\right)\right)\to {P}\mathrm{ball}\left({D}\right){S}={P}\mathrm{ball}\left({C}\right){S}$