Metamath Proof Explorer

Theorem blpnfctr

Description: The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion blpnfctr ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → P ball ⁡ D +∞ = A ball ⁡ D +∞

Proof

Step Hyp Ref Expression
1 eqid ⊢ D -1 ℝ = D -1 ℝ
2 1 xmeter ⊢ D ∈ ∞Met ⁡ X → D -1 ℝ Er X
3 2 3ad2ant1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → D -1 ℝ Er X
4 simp3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A ∈ P ball ⁡ D +∞
5 1 xmetec ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P D -1 ℝ = P ball ⁡ D +∞
6 5 3adant3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → P D -1 ℝ = P ball ⁡ D +∞
7 4 6 eleqtrrd ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A ∈ P D -1 ℝ
8 elecg ⊢ A ∈ P ball ⁡ D +∞ ∧ P ∈ X → A ∈ P D -1 ℝ ↔ P D -1 ℝ A
9 8 ancoms ⊢ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A ∈ P D -1 ℝ ↔ P D -1 ℝ A
10 9 3adant1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A ∈ P D -1 ℝ ↔ P D -1 ℝ A
11 7 10 mpbid ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → P D -1 ℝ A
12 3 11 erthi ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → P D -1 ℝ = A D -1 ℝ
13 pnfxr ⊢ +∞ ∈ ℝ *
14 blssm ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ +∞ ∈ ℝ * → P ball ⁡ D +∞ ⊆ X
15 13 14 mp3an3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P ball ⁡ D +∞ ⊆ X
16 15 sselda ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A ∈ X
17 1 xmetec ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X → A D -1 ℝ = A ball ⁡ D +∞
18 17 adantlr ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ X → A D -1 ℝ = A ball ⁡ D +∞
19 16 18 syldan ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A D -1 ℝ = A ball ⁡ D +∞
20 19 3impa ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → A D -1 ℝ = A ball ⁡ D +∞
21 12 6 20 3eqtr3d ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ P ball ⁡ D +∞ → P ball ⁡ D +∞ = A ball ⁡ D +∞