Step |
Hyp |
Ref |
Expression |
1 |
|
rrhf.d |
⊢ 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) |
2 |
|
rrhf.j |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
3 |
|
rrhf.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
4 |
|
rrhf.k |
⊢ 𝐾 = ( TopOpen ‘ 𝑅 ) |
5 |
|
rrhf.z |
⊢ 𝑍 = ( ℤMod ‘ 𝑅 ) |
6 |
|
rrhf.1 |
⊢ ( 𝜑 → 𝑅 ∈ DivRing ) |
7 |
|
rrhf.2 |
⊢ ( 𝜑 → 𝑅 ∈ NrmRing ) |
8 |
|
rrhf.3 |
⊢ ( 𝜑 → 𝑍 ∈ NrmMod ) |
9 |
|
rrhf.4 |
⊢ ( 𝜑 → ( chr ‘ 𝑅 ) = 0 ) |
10 |
|
rrhf.5 |
⊢ ( 𝜑 → 𝑅 ∈ CUnifSp ) |
11 |
|
rrhf.6 |
⊢ ( 𝜑 → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) |
12 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
13 |
1 12 3 4 5 6 7 8 9 10 11
|
rrhcn |
⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) ∈ ( ( topGen ‘ ran (,) ) Cn 𝐾 ) ) |
14 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
15 |
|
eqid |
⊢ ∪ 𝐾 = ∪ 𝐾 |
16 |
14 15
|
cnf |
⊢ ( ( ℝHom ‘ 𝑅 ) ∈ ( ( topGen ‘ ran (,) ) Cn 𝐾 ) → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ ∪ 𝐾 ) |
17 |
13 16
|
syl |
⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ ∪ 𝐾 ) |
18 |
|
nrgngp |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp ) |
19 |
|
ngpxms |
⊢ ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp ) |
20 |
7 18 19
|
3syl |
⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp ) |
21 |
|
xmstps |
⊢ ( 𝑅 ∈ ∞MetSp → 𝑅 ∈ TopSp ) |
22 |
3 4
|
tpsuni |
⊢ ( 𝑅 ∈ TopSp → 𝐵 = ∪ 𝐾 ) |
23 |
20 21 22
|
3syl |
⊢ ( 𝜑 → 𝐵 = ∪ 𝐾 ) |
24 |
23
|
feq3d |
⊢ ( 𝜑 → ( ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 ↔ ( ℝHom ‘ 𝑅 ) : ℝ ⟶ ∪ 𝐾 ) ) |
25 |
17 24
|
mpbird |
⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 ) |