Metamath Proof Explorer

Theorem rrextcusp

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

Ref Expression
Assertion rrextcusp ⊢ R ∈ ℝExt → R ∈ CUnifSp

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 simp3bi ⊢ R ∈ ℝExt → R ∈ CUnifSp ∧ UnifSt ⁡ R = metUnif ⁡ dist ⁡ R ↾ Base R × Base R
6 5 simpld ⊢ R ∈ ℝExt → R ∈ CUnifSp