Metamath Proof Explorer

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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		cnmpt1mulr.r	$⊢ φ \to R \in TopRing$
		cnmpt1mulr.k	$⊢ φ \to K \in TopOn (X)$
		cnmpt2mulr.l	$⊢ φ \to L \in TopOn (Y)$
		cnmpt2mulr.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
		cnmpt2mulr.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
	Assertion	cnmpt2mulr	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{\cdot} B) \in ((K \times_{t} L) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	$⊢ J = TopOpen (R)$
2		cnmpt1mulr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		cnmpt1mulr.r	$⊢ φ \to R \in TopRing$
4		cnmpt1mulr.k	$⊢ φ \to K \in TopOn (X)$
5		cnmpt2mulr.l	$⊢ φ \to L \in TopOn (Y)$
6		cnmpt2mulr.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
7		cnmpt2mulr.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
8		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
9	8 1	mgptopn	$⊢ J = TopOpen ({mulGrp}_{R})$
10	8 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
11	8	trgtmd	$⊢ R \in TopRing \to {mulGrp}_{R} \in TopMnd$
12	3 11	syl	$⊢ φ \to {mulGrp}_{R} \in TopMnd$
13	9 10 12 4 5 6 7	cnmpt2plusg	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{\cdot} B) \in ((K \times_{t} L) Cn J)$