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 X. B ) )
Assertion	rrextust	|- ( R e. RRExt -> ( UnifSt ` R ) = ( metUnif ` D ) )

Proof

Step	Hyp	Ref	Expression
1		rrextust.b	|- B = ( Base ` R )
2		rrextust.d	|- D = ( ( dist ` R ) |` ( B X. B ) )
3		eqid	|- ( ZMod ` R ) = ( ZMod ` R )
4	1 2 3	isrrext	|- ( R e. RRExt <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( ( ZMod ` R ) e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) )
5	4	simp3bi	|- ( R e. RRExt -> ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) )
6	5	simprd	|- ( R e. RRExt -> ( UnifSt ` R ) = ( metUnif ` D ) )