This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
cnmpt1mulr.t ⊢ · = ( .r ‘ 𝑅 )
cnmpt1mulr.r ⊢ ( 𝜑 → 𝑅 ∈ TopRing )
cnmpt1mulr.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt1mulr.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
cnmpt1mulr.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
Assertion cnmpt1mulr ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) )

Proof

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