cnmpt2vsca

Description: Continuity of scalar multiplication; analogue of cnmpt22f which cannot be used directly because .s is not a function. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	tlmtrg.f	$⊢ F = Scalar (W)$
	cnmpt1vsca.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	cnmpt1vsca.j	$⊢ J = TopOpen (W)$
	cnmpt1vsca.k	$⊢ K = TopOpen (F)$
	cnmpt1vsca.w	$⊢ φ \to W \in TopMod$
	cnmpt1vsca.l	$⊢ φ \to L \in TopOn (X)$
	cnmpt2vsca.m	$⊢ φ \to M \in TopOn (Y)$
	cnmpt2vsca.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((L \times_{t} M) Cn K)$
	cnmpt2vsca.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((L \times_{t} M) Cn J)$
Assertion	cnmpt2vsca	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{\cdot} B) \in ((L \times_{t} M) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	$⊢ F = Scalar (W)$
2		cnmpt1vsca.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		cnmpt1vsca.j	$⊢ J = TopOpen (W)$
4		cnmpt1vsca.k	$⊢ K = TopOpen (F)$
5		cnmpt1vsca.w	$⊢ φ \to W \in TopMod$
6		cnmpt1vsca.l	$⊢ φ \to L \in TopOn (X)$
7		cnmpt2vsca.m	$⊢ φ \to M \in TopOn (Y)$
8		cnmpt2vsca.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((L \times_{t} M) Cn K)$
9		cnmpt2vsca.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((L \times_{t} M) Cn J)$
10		txtopon	$⊢ (L \in TopOn (X) \land M \in TopOn (Y)) \to L \times_{t} M \in TopOn (X \times Y)$
11	6 7 10	syl2anc	$⊢ φ \to L \times_{t} M \in TopOn (X \times Y)$
12	1	tlmscatps	$⊢ W \in TopMod \to F \in TopSp$
13	5 12	syl	$⊢ φ \to F \in TopSp$
14		eqid	$⊢ {Base}_{F} = {Base}_{F}$
15	14 4	istps	$⊢ F \in TopSp \leftrightarrow K \in TopOn ({Base}_{F})$
16	13 15	sylib	$⊢ φ \to K \in TopOn ({Base}_{F})$
17		cnf2	$⊢ (L \times_{t} M \in TopOn (X \times Y) \land K \in TopOn ({Base}_{F}) \land (x \in X, y \in Y ⟼ A) \in ((L \times_{t} M) Cn K)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{F}$
18	11 16 8 17	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{F}$
19		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
20	19	fmpo	$⊢ \forall x \in X \forall y \in Y A \in {Base}_{F} \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{F}$
21	18 20	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in {Base}_{F}$
22	21	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y A \in {Base}_{F}$
23	22	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in {Base}_{F}$
24		tlmtps	$⊢ W \in TopMod \to W \in TopSp$
25	5 24	syl	$⊢ φ \to W \in TopSp$
26		eqid	$⊢ {Base}_{W} = {Base}_{W}$
27	26 3	istps	$⊢ W \in TopSp \leftrightarrow J \in TopOn ({Base}_{W})$
28	25 27	sylib	$⊢ φ \to J \in TopOn ({Base}_{W})$
29		cnf2	$⊢ (L \times_{t} M \in TopOn (X \times Y) \land J \in TopOn ({Base}_{W}) \land (x \in X, y \in Y ⟼ B) \in ((L \times_{t} M) Cn J)) \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
30	11 28 9 29	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
31		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
32	31	fmpo	$⊢ \forall x \in X \forall y \in Y B \in {Base}_{W} \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
33	30 32	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in {Base}_{W}$
34	33	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y B \in {Base}_{W}$
35	34	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to B \in {Base}_{W}$
36		eqid	$⊢ \cdot_{𝑠𝑓} (W) = \cdot_{𝑠𝑓} (W)$
37	26 1 14 36 2	scafval	$⊢ (A \in {Base}_{F} \land B \in {Base}_{W}) \to A \cdot_{𝑠𝑓} (W) B = A \underset{˙}{\cdot} B$
38	23 35 37	syl2anc	$⊢ ((φ \land x \in X) \land y \in Y) \to A \cdot_{𝑠𝑓} (W) B = A \underset{˙}{\cdot} B$
39	38	3impa	$⊢ (φ \land x \in X \land y \in Y) \to A \cdot_{𝑠𝑓} (W) B = A \underset{˙}{\cdot} B$
40	39	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ A \cdot_{𝑠𝑓} (W) B) = (x \in X, y \in Y ⟼ A \underset{˙}{\cdot} B)$
41	36 3 1 4	vscacn	$⊢ W \in TopMod \to \cdot_{𝑠𝑓} (W) \in ((K \times_{t} J) Cn J)$
42	5 41	syl	$⊢ φ \to \cdot_{𝑠𝑓} (W) \in ((K \times_{t} J) Cn J)$
43	6 7 8 9 42	cnmpt22f	$⊢ φ \to (x \in X, y \in Y ⟼ A \cdot_{𝑠𝑓} (W) B) \in ((L \times_{t} M) Cn J)$
44	40 43	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{\cdot} B) \in ((L \times_{t} M) Cn J)$

Metamath Proof Explorer

Theorem cnmpt2vsca

Proof