Theorem cnfldcusp

Description: The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

	Ref	Expression
Assertion	cnfldcusp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2	1	ne0ii	$$⊢ℂ\ne \varnothing$$
3		cncms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
4		eqid	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4	cnflduss	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$
6		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
7		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
8		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
9		fco	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ\times ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
10	7 8 9	mp2an	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
11		ffn	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ\to \left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)$$
12		fnresdm	$$⊢\left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}=\mathrm{abs}\circ -$$
13	10 11 12	mp2b	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}=\mathrm{abs}\circ -$$
14		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
15	14	reseq1i	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
16	13 15	eqtr3i	$$⊢\mathrm{abs}\circ -={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
17	6 16 4	cmetcusp1	$$⊢\left(ℂ\ne \varnothing \wedge {ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}\wedge \mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$
18	2 3 5 17	mp3an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$