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 ‘ 𝐷 ) +∞ ) = 𝑆 ) |