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	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	sblpnf.d	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}$$
Assertion	sblpnf	$$⊢\left(\phi \wedge P\in S\right)\to P\mathrm{ball}\left(D\right)\mathrm{+\infty }=S$$

Proof

Step	Hyp	Ref	Expression
1		sblpnf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		sblpnf.d	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}$$
3		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
4		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
5	4	remet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)$$
6		xpeq12	$$⊢\left(S=ℝ\wedge S=ℝ\right)\to S\times S={ℝ}^2$$
7	6	anidms	$$⊢S=ℝ\to S\times S={ℝ}^2$$
8	7	reseq2d	$$⊢S=ℝ\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
9		fveq2	$$⊢S=ℝ\to \mathrm{Met}\left(S\right)=\mathrm{Met}\left(ℝ\right)$$
10	8 9	eleq12d	$$⊢S=ℝ\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}\in \mathrm{Met}\left(S\right)\leftrightarrow {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)\right)$$
11	5 10	mpbiri	$$⊢S=ℝ\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}\in \mathrm{Met}\left(S\right)$$
12	2 11	eqeltrid	$$⊢S=ℝ\to D\in \mathrm{Met}\left(S\right)$$
13		relco	$$⊢\mathrm{Rel}\left(\mathrm{abs}\circ -\right)$$
14		resdm	$$⊢\mathrm{Rel}\left(\mathrm{abs}\circ -\right)\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\mathrm{dom}\left(\mathrm{abs}\circ -\right)}=\mathrm{abs}\circ -$$
15	13 14	ax-mp	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\mathrm{dom}\left(\mathrm{abs}\circ -\right)}=\mathrm{abs}\circ -$$
16		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
17		ax-resscn	$$⊢ℝ\subseteq ℂ$$
18		fss	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \mathrm{abs}:ℂ⟶ℂ$$
19	16 17 18	mp2an	$$⊢\mathrm{abs}:ℂ⟶ℂ$$
20		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
21		fco	$$⊢\left(\mathrm{abs}:ℂ⟶ℂ\wedge -:ℂ\times ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℂ$$
22	19 20 21	mp2an	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℂ$$
23	22	fdmi	$$⊢\mathrm{dom}\left(\mathrm{abs}\circ -\right)=ℂ\times ℂ$$
24	23	reseq2i	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\mathrm{dom}\left(\mathrm{abs}\circ -\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
25	15 24	eqtr3i	$$⊢\mathrm{abs}\circ -={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
26		cnmet	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$$
27	25 26	eqeltrri	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}\in \mathrm{Met}\left(ℂ\right)$$
28		xpeq12	$$⊢\left(S=ℂ\wedge S=ℂ\right)\to S\times S=ℂ\times ℂ$$
29	28	anidms	$$⊢S=ℂ\to S\times S=ℂ\times ℂ$$
30	29	reseq2d	$$⊢S=ℂ\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
31		fveq2	$$⊢S=ℂ\to \mathrm{Met}\left(S\right)=\mathrm{Met}\left(ℂ\right)$$
32	30 31	eleq12d	$$⊢S=ℂ\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}\in \mathrm{Met}\left(S\right)\leftrightarrow {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}\in \mathrm{Met}\left(ℂ\right)\right)$$
33	27 32	mpbiri	$$⊢S=ℂ\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(S\times S\right)}\in \mathrm{Met}\left(S\right)$$
34	2 33	eqeltrid	$$⊢S=ℂ\to D\in \mathrm{Met}\left(S\right)$$
35	12 34	jaoi	$$⊢\left(S=ℝ\vee S=ℂ\right)\to D\in \mathrm{Met}\left(S\right)$$
36	1 3 35	3syl	$$⊢\phi \to D\in \mathrm{Met}\left(S\right)$$
37		blpnf	$$⊢\left(D\in \mathrm{Met}\left(S\right)\wedge P\in S\right)\to P\mathrm{ball}\left(D\right)\mathrm{+\infty }=S$$
38	36 37	sylan	$$⊢\left(\phi \wedge P\in S\right)\to P\mathrm{ball}\left(D\right)\mathrm{+\infty }=S$$