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 𝐽 ) )