Metamath Proof Explorer

Theorem elbl3ps

Description: Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007)

Ref Expression
Assertion elbl3ps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A D P < R

Proof

Step Hyp Ref Expression
1 elbl2ps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R
2 psmetsym ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A = A D P
3 2 3expb ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A = A D P
4 3 adantlr ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P D A = A D P
5 4 breq1d ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P D A < R ↔ A D P < R
6 1 5 bitrd ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A D P < R