Description: The functionalization of the ring multiplication operation is a continuous function in a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulrcn.j | ⊢ 𝐽 = ( TopOpen ‘ 𝑅 ) | |
mulrcn.t | ⊢ 𝑇 = ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) | ||
Assertion | mulrcn | ⊢ ( 𝑅 ∈ TopRing → 𝑇 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulrcn.j | ⊢ 𝐽 = ( TopOpen ‘ 𝑅 ) | |
2 | mulrcn.t | ⊢ 𝑇 = ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) | |
3 | eqid | ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) | |
4 | 3 | trgtmd | ⊢ ( 𝑅 ∈ TopRing → ( mulGrp ‘ 𝑅 ) ∈ TopMnd ) |
5 | 3 1 | mgptopn | ⊢ 𝐽 = ( TopOpen ‘ ( mulGrp ‘ 𝑅 ) ) |
6 | 5 2 | tmdcn | ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ TopMnd → 𝑇 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
7 | 4 6 | syl | ⊢ ( 𝑅 ∈ TopRing → 𝑇 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |