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 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ◡ 𝐷 “ ℝ ) = ( ◡ 𝐷 “ ℝ )
2 1 xmeter ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ◡ 𝐷 “ ℝ ) Er 𝑋 )
3 2 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( ◡ 𝐷 “ ℝ ) Er 𝑋 )
4 simp3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
5 1 xmetec ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
6 5 3adant3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
7 4 6 eleqtrrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → 𝐴 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) )
8 elecg ⊢ ( ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝐴 ) )
9 8 ancoms ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝐴 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝐴 ) )
10 9 3adant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝐴 ∈ [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ◡ 𝐷 “ ℝ ) 𝐴 ) )
11 7 10 mpbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → 𝑃 ( ◡ 𝐷 “ ℝ ) 𝐴 )
12 3 11 erthi ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → [ 𝑃 ] ( ◡ 𝐷 “ ℝ ) = [ 𝐴 ] ( ◡ 𝐷 “ ℝ ) )
13 pnfxr ⊢ +∞ ∈ ℝ*
14 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ +∞ ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ⊆ 𝑋 )
15 13 14 mp3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ⊆ 𝑋 )
16 15 sselda ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → 𝐴 ∈ 𝑋 )
17 1 xmetec ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ( ◡ 𝐷 “ ℝ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
18 17 adantlr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ( ◡ 𝐷 “ ℝ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
19 16 18 syldan ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → [ 𝐴 ] ( ◡ 𝐷 “ ℝ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
20 19 3impa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → [ 𝐴 ] ( ◡ 𝐷 “ ℝ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
21 12 6 20 3eqtr3d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )