This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blvalps

Description: The ball around a point P is the set of all points whose distance from P is less than the ball's radius R . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blvalps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → P ball ⁡ D R = x ∈ X | P D x < R

Proof

Step Hyp Ref Expression
1 blfvalps ⊢ D ∈ PsMet ⁡ X → ball ⁡ D = y ∈ X , r ∈ ℝ * ⟼ x ∈ X | y D x < r
2 1 3ad2ant1 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → ball ⁡ D = y ∈ X , r ∈ ℝ * ⟼ x ∈ X | y D x < r
3 simprl ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ y = P ∧ r = R → y = P
4 3 oveq1d ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ y = P ∧ r = R → y D x = P D x
5 simprr ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ y = P ∧ r = R → r = R
6 4 5 breq12d ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ y = P ∧ r = R → y D x < r ↔ P D x < R
7 6 rabbidv ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ y = P ∧ r = R → x ∈ X | y D x < r = x ∈ X | P D x < R
8 simp2 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → P ∈ X
9 simp3 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → R ∈ ℝ *
10 elfvdm ⊢ D ∈ PsMet ⁡ X → X ∈ dom ⁡ PsMet
11 10 3ad2ant1 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → X ∈ dom ⁡ PsMet
12 rabexg ⊢ X ∈ dom ⁡ PsMet → x ∈ X | P D x < R ∈ V
13 11 12 syl ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → x ∈ X | P D x < R ∈ V
14 2 7 8 9 13 ovmpod ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → P ball ⁡ D R = x ∈ X | P D x < R