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