Metamath Proof Explorer

Theorem blcomps

Description: Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blcomps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P ∈ A ball ⁡ D 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 elbl3ps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ A ∈ X ∧ P ∈ X → P ∈ A ball ⁡ D R ↔ P D A < R
3 2 ancom2s ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P ∈ A ball ⁡ D R ↔ P D A < R
4 1 3 bitr4d ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P ∈ A ball ⁡ D R