Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
2 |
|
eqid |
|- ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) |
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 ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) ) ) ) |
5 |
4
|
simp1bi |
|- ( R e. RRExt -> ( R e. NrmRing /\ R e. DivRing ) ) |
6 |
5
|
simpld |
|- ( R e. RRExt -> R e. NrmRing ) |