Metamath Proof Explorer


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 = Base R
rrextust.d D = dist R B × B
Assertion rrextust R ℝExt UnifSt R = metUnif D

Proof

Step Hyp Ref Expression
1 rrextust.b B = Base R
2 rrextust.d D = dist R B × B
3 eqid ℤMod R = ℤMod R
4 1 2 3 isrrext R ℝExt R NrmRing R DivRing ℤMod R NrmMod chr R = 0 R CUnifSp UnifSt R = metUnif D
5 4 simp3bi R ℝExt R CUnifSp UnifSt R = metUnif D
6 5 simprd R ℝExt UnifSt R = metUnif D