Theorem cnmpt1mulr

Description: Continuity of ring multiplication; analogue of cnmpt12f which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	mulrcn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
	cnmpt1mulr.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	cnmpt1mulr.r	$$⊢\phi \to R\in \mathrm{TopRing}$$
	cnmpt1mulr.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(X\right)$$
	cnmpt1mulr.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(K\mathrm{Cn}J\right)$$
	cnmpt1mulr.b	$$⊢\phi \to \left(x\in X⟼B\right)\in \left(K\mathrm{Cn}J\right)$$
Assertion	cnmpt1mulr	$$⊢\phi \to \left(x\in X⟼A\underset{\dot{}}{·}B\right)\in \left(K\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
2		cnmpt1mulr.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		cnmpt1mulr.r	$$⊢\phi \to R\in \mathrm{TopRing}$$
4		cnmpt1mulr.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(X\right)$$
5		cnmpt1mulr.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(K\mathrm{Cn}J\right)$$
6		cnmpt1mulr.b	$$⊢\phi \to \left(x\in X⟼B\right)\in \left(K\mathrm{Cn}J\right)$$
7		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
8	7 1	mgptopn	$$⊢J=\mathrm{TopOpen}\left({\mathrm{mulGrp}}_R\right)$$
9	7 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
10	7	trgtmd	$$⊢R\in \mathrm{TopRing}\to {\mathrm{mulGrp}}_R\in \mathrm{TopMnd}$$
11	3 10	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{TopMnd}$$
12	8 9 11 4 5 6	cnmpt1plusg	$$⊢\phi \to \left(x\in X⟼A\underset{\dot{}}{·}B\right)\in \left(K\mathrm{Cn}J\right)$$