Step |
Hyp |
Ref |
Expression |
1 |
|
rrhcne.j |
|- J = ( topGen ` ran (,) ) |
2 |
|
rrhcne.k |
|- K = ( TopOpen ` R ) |
3 |
|
eqid |
|- ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) |
4 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
5 |
|
eqid |
|- ( ZMod ` R ) = ( ZMod ` R ) |
6 |
|
rrextdrg |
|- ( R e. RRExt -> R e. DivRing ) |
7 |
|
rrextnrg |
|- ( R e. RRExt -> R e. NrmRing ) |
8 |
5
|
rrextnlm |
|- ( R e. RRExt -> ( ZMod ` R ) e. NrmMod ) |
9 |
|
rrextchr |
|- ( R e. RRExt -> ( chr ` R ) = 0 ) |
10 |
|
rrextcusp |
|- ( R e. RRExt -> R e. CUnifSp ) |
11 |
4 3
|
rrextust |
|- ( R e. RRExt -> ( UnifSt ` R ) = ( metUnif ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) ) |
12 |
3 1 4 2 5 6 7 8 9 10 11
|
rrhcn |
|- ( R e. RRExt -> ( RRHom ` R ) e. ( J Cn K ) ) |