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=\mathrm{TopOpen}\left(R\right)$$
	mulrcn.t	$$⊢T={+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)$$
Assertion	mulrcn	$$⊢R\in \mathrm{TopRing}\to T\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
2		mulrcn.t	$$⊢T={+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
4	3	trgtmd	$$⊢R\in \mathrm{TopRing}\to {\mathrm{mulGrp}}_R\in \mathrm{TopMnd}$$
5	3 1	mgptopn	$$⊢J=\mathrm{TopOpen}\left({\mathrm{mulGrp}}_R\right)$$
6	5 2	tmdcn	$$⊢{\mathrm{mulGrp}}_R\in \mathrm{TopMnd}\to T\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$
7	4 6	syl	$$⊢R\in \mathrm{TopRing}\to T\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$