Theorem reust

Description: The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018)

	Ref	Expression
Assertion	reust	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
2	1	fveq2i	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
3		reex	$$⊢ℝ\in \mathrm{V}$$
4		ressuss	$$⊢ℝ\in \mathrm{V}\to \mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^2$$
5	3 4	ax-mp	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^2$$
6		eqid	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
7	6	cnflduss	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$
8	7	oveq1i	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^2=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right){\upharpoonright }_{𝑡}{ℝ}^2$$
9	2 5 8	3eqtri	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right){\upharpoonright }_{𝑡}{ℝ}^2$$
10		0re	$$⊢0\in ℝ$$
11	10	ne0ii	$$⊢ℝ\ne \varnothing$$
12		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
13		xmetpsmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\to \mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)$$
14	12 13	ax-mp	$$⊢\mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)$$
15		ax-resscn	$$⊢ℝ\subseteq ℂ$$
16		restmetu	$$⊢\left(ℝ\ne \varnothing \wedge \mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)\wedge ℝ\subseteq ℂ\right)\to \mathrm{metUnif}\left(\mathrm{abs}\circ -\right){\upharpoonright }_{𝑡}{ℝ}^2=\mathrm{metUnif}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
17	11 14 15 16	mp3an	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right){\upharpoonright }_{𝑡}{ℝ}^2=\mathrm{metUnif}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
18		reds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)$$
19	18	reseq1i	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}$$
20	19	fveq2i	$$⊢\mathrm{metUnif}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}\right)$$
21	9 17 20	3eqtri	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{{ℝ}^2}\right)$$