Metamath Proof Explorer


Theorem rrextnrg

Description: An extension of RR is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018)

Ref Expression
Assertion rrextnrg R ℝExt R NrmRing

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 eqid dist R Base R × Base R = dist R Base R × Base R
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 dist R Base R × Base R
5 4 simp1bi R ℝExt R NrmRing R DivRing
6 5 simpld R ℝExt R NrmRing