Metamath Proof Explorer

Theorem elbl4

Description: Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion elbl4 ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → B ∈ A ball ⁡ D R ↔ B D -1 0 R A

Proof

Step Hyp Ref Expression
1 rpxr ⊢ R ∈ ℝ + → R ∈ ℝ *
2 blcomps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ A ∈ X ∧ B ∈ X → B ∈ A ball ⁡ D R ↔ A ∈ B ball ⁡ D R
3 1 2 sylanl2 ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → B ∈ A ball ⁡ D R ↔ A ∈ B ball ⁡ D R
4 simpll ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → D ∈ PsMet ⁡ X
5 simprr ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → B ∈ X
6 simplr ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → R ∈ ℝ +
7 blval2 ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X ∧ R ∈ ℝ + → B ball ⁡ D R = D -1 0 R B
8 7 eleq2d ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X ∧ R ∈ ℝ + → A ∈ B ball ⁡ D R ↔ A ∈ D -1 0 R B
9 4 5 6 8 syl3anc ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → A ∈ B ball ⁡ D R ↔ A ∈ D -1 0 R B
10 elimasng ⊢ B ∈ X ∧ A ∈ X → A ∈ D -1 0 R B ↔ B A ∈ D -1 0 R
11 df-br ⊢ B D -1 0 R A ↔ B A ∈ D -1 0 R
12 10 11 bitr4di ⊢ B ∈ X ∧ A ∈ X → A ∈ D -1 0 R B ↔ B D -1 0 R A
13 12 ancoms ⊢ A ∈ X ∧ B ∈ X → A ∈ D -1 0 R B ↔ B D -1 0 R A
14 13 adantl ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → A ∈ D -1 0 R B ↔ B D -1 0 R A
15 3 9 14 3bitrd ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ + ∧ A ∈ X ∧ B ∈ X → B ∈ A ball ⁡ D R ↔ B D -1 0 R A