rrextcusp

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

		Ref	Expression
	Assertion	rrextcusp	$⊢ R \in ℝExt \to R \in CUnifSp$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
3		eqid	$⊢ ℤMod (R) = ℤMod (R)$
4	1 2 3	isrrext	$⊢ R \in ℝExt \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land (ℤMod (R) \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})))$
5	4	simp3bi	$⊢ R \in ℝExt \to (R \in CUnifSp \land UnifSt (R) = metUnif ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}))$
6	5	simpld	$⊢ R \in ℝExt \to R \in CUnifSp$

Metamath Proof Explorer