Step |
Hyp |
Ref |
Expression |
1 |
|
rrhcne.j |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
2 |
|
rrhcne.k |
⊢ 𝐾 = ( TopOpen ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
5 |
|
eqid |
⊢ ( ℤMod ‘ 𝑅 ) = ( ℤMod ‘ 𝑅 ) |
6 |
|
rrextdrg |
⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ DivRing ) |
7 |
|
rrextnrg |
⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing ) |
8 |
5
|
rrextnlm |
⊢ ( 𝑅 ∈ ℝExt → ( ℤMod ‘ 𝑅 ) ∈ NrmMod ) |
9 |
|
rrextchr |
⊢ ( 𝑅 ∈ ℝExt → ( chr ‘ 𝑅 ) = 0 ) |
10 |
|
rrextcusp |
⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp ) |
11 |
4 3
|
rrextust |
⊢ ( 𝑅 ∈ ℝExt → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ) |
12 |
3 1 4 2 5 6 7 8 9 10 11
|
rrhcn |
⊢ ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) ) |