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	|- J = ( TopOpen ` R )
	mulrcn.t	|- T = ( +f ` ( mulGrp ` R ) )
Assertion	mulrcn	|- ( R e. TopRing -> T e. ( ( J tX J ) Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	|- J = ( TopOpen ` R )
2		mulrcn.t	|- T = ( +f ` ( mulGrp ` R ) )
3		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
4	3	trgtmd	|- ( R e. TopRing -> ( mulGrp ` R ) e. TopMnd )
5	3 1	mgptopn	|- J = ( TopOpen ` ( mulGrp ` R ) )
6	5 2	tmdcn	|- ( ( mulGrp ` R ) e. TopMnd -> T e. ( ( J tX J ) Cn J ) )
7	4 6	syl	|- ( R e. TopRing -> T e. ( ( J tX J ) Cn J ) )