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 ⊢ φ → S ∈ ℝ ℂ
sblpnf.d ⊢ D = abs ∘ − ↾ S × S
Assertion sblpnf ⊢ φ ∧ P ∈ S → P ball ⁡ D +∞ = S

Proof

Step Hyp Ref Expression
1 sblpnf.s ⊢ φ → S ∈ ℝ ℂ
2 sblpnf.d ⊢ D = abs ∘ − ↾ S × S
3 elpri ⊢ S ∈ ℝ ℂ → S = ℝ ∨ S = ℂ
4 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
5 4 remet ⊢ abs ∘ − ↾ ℝ 2 ∈ Met ⁡ ℝ
6 xpeq12 ⊢ S = ℝ ∧ S = ℝ → S × S = ℝ 2
7 6 anidms ⊢ S = ℝ → S × S = ℝ 2
8 7 reseq2d ⊢ S = ℝ → abs ∘ − ↾ S × S = abs ∘ − ↾ ℝ 2
9 fveq2 ⊢ S = ℝ → Met ⁡ S = Met ⁡ ℝ
10 8 9 eleq12d ⊢ S = ℝ → abs ∘ − ↾ S × S ∈ Met ⁡ S ↔ abs ∘ − ↾ ℝ 2 ∈ Met ⁡ ℝ
11 5 10 mpbiri ⊢ S = ℝ → abs ∘ − ↾ S × S ∈ Met ⁡ S
12 2 11 eqeltrid ⊢ S = ℝ → D ∈ Met ⁡ S
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 ⊢ S = ℂ ∧ S = ℂ → S × S = ℂ × ℂ
29 28 anidms ⊢ S = ℂ → S × S = ℂ × ℂ
30 29 reseq2d ⊢ S = ℂ → abs ∘ − ↾ S × S = abs ∘ − ↾ ℂ × ℂ
31 fveq2 ⊢ S = ℂ → Met ⁡ S = Met ⁡ ℂ
32 30 31 eleq12d ⊢ S = ℂ → abs ∘ − ↾ S × S ∈ Met ⁡ S ↔ abs ∘ − ↾ ℂ × ℂ ∈ Met ⁡ ℂ
33 27 32 mpbiri ⊢ S = ℂ → abs ∘ − ↾ S × S ∈ Met ⁡ S
34 2 33 eqeltrid ⊢ S = ℂ → D ∈ Met ⁡ S
35 12 34 jaoi ⊢ S = ℝ ∨ S = ℂ → D ∈ Met ⁡ S
36 1 3 35 3syl ⊢ φ → D ∈ Met ⁡ S
37 blpnf ⊢ D ∈ Met ⁡ S ∧ P ∈ S → P ball ⁡ D +∞ = S
38 36 37 sylan ⊢ φ ∧ P ∈ S → P ball ⁡ D +∞ = S