Metamath Proof Explorer


Theorem sblpnf

Description: The infinity ball in the absolute value metric is just the whole space. S analogue of blpnf . (Contributed by Steve Rodriguez, 8-Nov-2015)

Ref Expression
Hypotheses sblpnf.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
sblpnf.d 𝐷 = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
Assertion sblpnf ( ( 𝜑𝑃𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 sblpnf.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 sblpnf.d 𝐷 = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
3 elpri ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
4 eqid ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
5 4 remet ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ )
6 xpeq12 ( ( 𝑆 = ℝ ∧ 𝑆 = ℝ ) → ( 𝑆 × 𝑆 ) = ( ℝ × ℝ ) )
7 6 anidms ( 𝑆 = ℝ → ( 𝑆 × 𝑆 ) = ( ℝ × ℝ ) )
8 7 reseq2d ( 𝑆 = ℝ → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
9 fveq2 ( 𝑆 = ℝ → ( Met ‘ 𝑆 ) = ( Met ‘ ℝ ) )
10 8 9 eleq12d ( 𝑆 = ℝ → ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) ↔ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) ) )
11 5 10 mpbiri ( 𝑆 = ℝ → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) )
12 2 11 eqeltrid ( 𝑆 = ℝ → 𝐷 ∈ ( Met ‘ 𝑆 ) )
13 relco Rel ( abs ∘ − )
14 resdm ( Rel ( abs ∘ − ) → ( ( abs ∘ − ) ↾ dom ( abs ∘ − ) ) = ( abs ∘ − ) )
15 13 14 ax-mp ( ( abs ∘ − ) ↾ dom ( abs ∘ − ) ) = ( abs ∘ − )
16 absf abs : ℂ ⟶ ℝ
17 ax-resscn ℝ ⊆ ℂ
18 fss ( ( abs : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → abs : ℂ ⟶ ℂ )
19 16 17 18 mp2an abs : ℂ ⟶ ℂ
20 subf − : ( ℂ × ℂ ) ⟶ ℂ
21 fco ( ( abs : ℂ ⟶ ℂ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℂ )
22 19 20 21 mp2an ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℂ
23 22 fdmi dom ( abs ∘ − ) = ( ℂ × ℂ )
24 23 reseq2i ( ( abs ∘ − ) ↾ dom ( abs ∘ − ) ) = ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) )
25 15 24 eqtr3i ( abs ∘ − ) = ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) )
26 cnmet ( abs ∘ − ) ∈ ( Met ‘ ℂ )
27 25 26 eqeltrri ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) ∈ ( Met ‘ ℂ )
28 xpeq12 ( ( 𝑆 = ℂ ∧ 𝑆 = ℂ ) → ( 𝑆 × 𝑆 ) = ( ℂ × ℂ ) )
29 28 anidms ( 𝑆 = ℂ → ( 𝑆 × 𝑆 ) = ( ℂ × ℂ ) )
30 29 reseq2d ( 𝑆 = ℂ → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) )
31 fveq2 ( 𝑆 = ℂ → ( Met ‘ 𝑆 ) = ( Met ‘ ℂ ) )
32 30 31 eleq12d ( 𝑆 = ℂ → ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) ↔ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) ∈ ( Met ‘ ℂ ) ) )
33 27 32 mpbiri ( 𝑆 = ℂ → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) )
34 2 33 eqeltrid ( 𝑆 = ℂ → 𝐷 ∈ ( Met ‘ 𝑆 ) )
35 12 34 jaoi ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝐷 ∈ ( Met ‘ 𝑆 ) )
36 1 3 35 3syl ( 𝜑𝐷 ∈ ( Met ‘ 𝑆 ) )
37 blpnf ( ( 𝐷 ∈ ( Met ‘ 𝑆 ) ∧ 𝑃𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = 𝑆 )
38 36 37 sylan ( ( 𝜑𝑃𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = 𝑆 )