Theorem cnmpt2mulr

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

	Ref	Expression
Hypotheses	mulrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
	cnmpt1mulr.t	⊢ · = ( .r ‘ 𝑅 )
	cnmpt1mulr.r	⊢ ( 𝜑 → 𝑅 ∈ TopRing )
	cnmpt1mulr.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt2mulr.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt2mulr.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
	cnmpt2mulr.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
Assertion	cnmpt2mulr	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2		cnmpt1mulr.t	⊢ · = ( .r ‘ 𝑅 )
3		cnmpt1mulr.r	⊢ ( 𝜑 → 𝑅 ∈ TopRing )
4		cnmpt1mulr.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
5		cnmpt2mulr.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
6		cnmpt2mulr.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
7		cnmpt2mulr.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
8		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
9	8 1	mgptopn	⊢ 𝐽 = ( TopOpen ‘ ( mulGrp ‘ 𝑅 ) )
10	8 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
11	8	trgtmd	⊢ ( 𝑅 ∈ TopRing → ( mulGrp ‘ 𝑅 ) ∈ TopMnd )
12	3 11	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ TopMnd )
13	9 10 12 4 5 6 7	cnmpt2plusg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )