# Metamath Proof Explorer

## Theorem blval2

Description: The ball around a point P , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blval2 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to {P}\mathrm{ball}\left({D}\right){R}={{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]$

### Proof

Step Hyp Ref Expression
1 rpxr ${⊢}{R}\in {ℝ}^{+}\to {R}\in {ℝ}^{*}$
2 blvalps ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {P}\mathrm{ball}\left({D}\right){R}=\left\{{x}\in {X}|{P}{D}{x}<{R}\right\}$
3 1 2 syl3an3 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to {P}\mathrm{ball}\left({D}\right){R}=\left\{{x}\in {X}|{P}{D}{x}<{R}\right\}$
4 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)$
5 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]$
6 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|{P}{D}{x}<{R}\right\}$
7 psmetf ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
8 ffn ${⊢}{D}:{X}×{X}⟶{ℝ}^{*}\to {D}Fn\left({X}×{X}\right)$
9 elpreima ${⊢}{D}Fn\left({X}×{X}\right)\to \left(⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]↔\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)\right)$
10 7 8 9 3syl ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left(⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]↔\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)\right)$
11 10 3ad2ant1 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]↔\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)\right)$
12 opelxp ${⊢}⟨{P},{x}⟩\in \left({X}×{X}\right)↔\left({P}\in {X}\wedge {x}\in {X}\right)$
13 12 baib ${⊢}{P}\in {X}\to \left(⟨{P},{x}⟩\in \left({X}×{X}\right)↔{x}\in {X}\right)$
14 13 3ad2ant2 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(⟨{P},{x}⟩\in \left({X}×{X}\right)↔{x}\in {X}\right)$
15 14 biimpd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(⟨{P},{x}⟩\in \left({X}×{X}\right)\to {x}\in {X}\right)$
16 15 adantrd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)\to {x}\in {X}\right)$
17 simprl ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)\to {x}\in {X}$
18 17 ex ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\to {x}\in {X}\right)$
19 simpl2 ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {P}\in {X}$
20 19 13 syl ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(⟨{P},{x}⟩\in \left({X}×{X}\right)↔{x}\in {X}\right)$
21 df-ov ${⊢}{P}{D}{x}={D}\left(⟨{P},{x}⟩\right)$
22 21 eleq1i ${⊢}{P}{D}{x}\in \left[0,{R}\right)↔{D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)$
23 0xr ${⊢}0\in {ℝ}^{*}$
24 simpl3 ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {R}\in {ℝ}^{+}$
25 24 rpxrd ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {R}\in {ℝ}^{*}$
26 elico1 ${⊢}\left(0\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to \left({P}{D}{x}\in \left[0,{R}\right)↔\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\wedge {P}{D}{x}<{R}\right)\right)$
27 23 25 26 sylancr ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({P}{D}{x}\in \left[0,{R}\right)↔\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\wedge {P}{D}{x}<{R}\right)\right)$
28 simpl1 ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {D}\in \mathrm{PsMet}\left({X}\right)$
29 simpr ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\in {X}$
30 psmetcl ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {X}\right)\to {P}{D}{x}\in {ℝ}^{*}$
31 28 19 29 30 syl3anc ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {P}{D}{x}\in {ℝ}^{*}$
32 psmetge0 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {X}\right)\to 0\le {P}{D}{x}$
33 28 19 29 32 syl3anc ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to 0\le {P}{D}{x}$
34 31 33 jca ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\right)$
35 34 biantrurd ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({P}{D}{x}<{R}↔\left(\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\right)\wedge {P}{D}{x}<{R}\right)\right)$
36 df-3an ${⊢}\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\wedge {P}{D}{x}<{R}\right)↔\left(\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\right)\wedge {P}{D}{x}<{R}\right)$
37 35 36 syl6rbbr ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(\left({P}{D}{x}\in {ℝ}^{*}\wedge 0\le {P}{D}{x}\wedge {P}{D}{x}<{R}\right)↔{P}{D}{x}<{R}\right)$
38 27 37 bitrd ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({P}{D}{x}\in \left[0,{R}\right)↔{P}{D}{x}<{R}\right)$
39 22 38 syl5bbr ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)↔{P}{D}{x}<{R}\right)$
40 20 39 anbi12d ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
41 40 ex ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left({x}\in {X}\to \left(\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)\right)$
42 16 18 41 pm5.21ndd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(\left(⟨{P},{x}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{P},{x}⟩\right)\in \left[0,{R}\right)\right)↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
43 11 42 bitrd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left(⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
44 elimasng ${⊢}\left({P}\in {X}\wedge {x}\in \mathrm{V}\right)\to \left({x}\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]↔⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\right)$
45 44 elvd ${⊢}{P}\in {X}\to \left({x}\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]↔⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\right)$
46 45 3ad2ant2 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left({x}\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]↔⟨{P},{x}⟩\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\right)$
47 rabid ${⊢}{x}\in \left\{{x}\in {X}|{P}{D}{x}<{R}\right\}↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)$
48 47 a1i ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left({x}\in \left\{{x}\in {X}|{P}{D}{x}<{R}\right\}↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
49 43 46 48 3bitr4d ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to \left({x}\in {{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]↔{x}\in \left\{{x}\in {X}|{P}{D}{x}<{R}\right\}\right)$
50 4 5 6 49 eqrd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to {{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]=\left\{{x}\in {X}|{P}{D}{x}<{R}\right\}$
51 3 50 eqtr4d ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to {P}\mathrm{ball}\left({D}\right){R}={{D}}^{-1}\left[\left[0,{R}\right)\right]\left[\left\{{P}\right\}\right]$