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
|- J = ( TopOpen ` R )
cnmpt1mulr.t
|- .x. = ( .r ` R )
cnmpt1mulr.r
|- ( ph -> R e. TopRing )
cnmpt1mulr.k
|- ( ph -> K e. ( TopOn ` X ) )
cnmpt1mulr.a
|- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
cnmpt1mulr.b
|- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
Assertion cnmpt1mulr
|- ( ph -> ( x e. X |-> ( A .x. B ) ) e. ( K Cn J ) )

Proof

Step Hyp Ref Expression
1 mulrcn.j
 |-  J = ( TopOpen ` R )
2 cnmpt1mulr.t
 |-  .x. = ( .r ` R )
3 cnmpt1mulr.r
 |-  ( ph -> R e. TopRing )
4 cnmpt1mulr.k
 |-  ( ph -> K e. ( TopOn ` X ) )
5 cnmpt1mulr.a
 |-  ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
6 cnmpt1mulr.b
 |-  ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
7 eqid
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
8 7 1 mgptopn
 |-  J = ( TopOpen ` ( mulGrp ` R ) )
9 7 2 mgpplusg
 |-  .x. = ( +g ` ( mulGrp ` R ) )
10 7 trgtmd
 |-  ( R e. TopRing -> ( mulGrp ` R ) e. TopMnd )
11 3 10 syl
 |-  ( ph -> ( mulGrp ` R ) e. TopMnd )
12 8 9 11 4 5 6 cnmpt1plusg
 |-  ( ph -> ( x e. X |-> ( A .x. B ) ) e. ( K Cn J ) )