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