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