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	|- J = ( TopOpen ` R )
	cnmpt1mulr.t	|- .x. = ( .r ` R )
	cnmpt1mulr.r	|- ( ph -> R e. TopRing )
	cnmpt1mulr.k	|- ( ph -> K e. ( TopOn ` X ) )
	cnmpt2mulr.l	|- ( ph -> L e. ( TopOn ` Y ) )
	cnmpt2mulr.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
	cnmpt2mulr.b	|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
Assertion	cnmpt2mulr	|- ( ph -> ( x e. X , y e. Y |-> ( A .x. B ) ) e. ( ( K tX L ) 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		cnmpt2mulr.l	|- ( ph -> L e. ( TopOn ` Y ) )
6		cnmpt2mulr.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
7		cnmpt2mulr.b	|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
8		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
9	8 1	mgptopn	|- J = ( TopOpen ` ( mulGrp ` R ) )
10	8 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
11	8	trgtmd	|- ( R e. TopRing -> ( mulGrp ` R ) e. TopMnd )
12	3 11	syl	|- ( ph -> ( mulGrp ` R ) e. TopMnd )
13	9 10 12 4 5 6 7	cnmpt2plusg	|- ( ph -> ( x e. X , y e. Y |-> ( A .x. B ) ) e. ( ( K tX L ) Cn J ) )