Theorem recusp

Description: The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

	Ref	Expression
Assertion	recusp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2	1	ne0ii	$$⊢ℝ\ne \varnothing$$
3		recms	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
4		reust	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}\right)$$
5		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
6		eqid	$$⊢{\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}={\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}$$
7		eqid	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)$$
8	5 6 7	cmetcusp1	$$⊢\left(ℝ\ne \varnothing \wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}\wedge \mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}\right)\right)\to {ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$
9	2 3 4 8	mp3an	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$