Theorem rrextust

Description: The uniformity of an extension of RR is the uniformity generated by its distance. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Hypotheses	rrextust.b	$$⊢B={\mathrm{Base}}_R$$
	rrextust.d	$$⊢D={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
Assertion	rrextust	$$⊢R\in \mathrm{ℝExt}\to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrextust.b	$$⊢B={\mathrm{Base}}_R$$
2		rrextust.d	$$⊢D={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
3		eqid	$$⊢\mathrm{\mathbb{Z}Mod}\left(R\right)=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
4	1 2 3	isrrext	$$⊢R\in \mathrm{ℝExt}\leftrightarrow \left(\left(R\in \mathrm{NrmRing}\wedge R\in \mathrm{DivRing}\right)\wedge \left(\mathrm{\mathbb{Z}Mod}\left(R\right)\in \mathrm{NrmMod}\wedge \mathrm{chr}\left(R\right)=0\right)\wedge \left(R\in \mathrm{CUnifSp}\wedge \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)\right)\right)$$
5	4	simp3bi	$$⊢R\in \mathrm{ℝExt}\to \left(R\in \mathrm{CUnifSp}\wedge \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)\right)$$
6	5	simprd	$$⊢R\in \mathrm{ℝExt}\to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$