Metamath Proof Explorer


Theorem mulrcn

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 𝐽 ) )

Proof

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 𝐽 ) )