Theorem 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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cnmpt1vsca.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	cnmpt1vsca.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	cnmpt1vsca.k	⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
	cnmpt1vsca.w	⊢ ( 𝜑 → 𝑊 ∈ TopMod )
	cnmpt1vsca.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt2vsca.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt2vsca.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐾 ) )
	cnmpt2vsca.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) )
Assertion	cnmpt2vsca	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cnmpt1vsca.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		cnmpt1vsca.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4		cnmpt1vsca.k	⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
5		cnmpt1vsca.w	⊢ ( 𝜑 → 𝑊 ∈ TopMod )
6		cnmpt1vsca.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑋 ) )
7		cnmpt2vsca.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑌 ) )
8		cnmpt2vsca.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐾 ) )
9		cnmpt2vsca.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) )
10		txtopon	⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11	6 7 10	syl2anc	⊢ ( 𝜑 → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
12	1	tlmscatps	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp )
13	5 12	syl	⊢ ( 𝜑 → 𝐹 ∈ TopSp )
14		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
15	14 4	istps	⊢ ( 𝐹 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) )
16	13 15	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) )
17		cnf2	⊢ ( ( ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐹 ) )
18	11 16 8 17	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐹 ) )
19		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
20	19	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐹 ) )
21	18 20	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐹 ) )
22	21	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐹 ) )
23	22	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐹 ) )
24		tlmtps	⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopSp )
25	5 24	syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
26		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
27	26 3	istps	⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
28	25 27	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
29		cnf2	⊢ ( ( ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
30	11 28 9 29	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
31		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
32	31	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
33	30 32	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
34	33	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
35	34	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝑊 ) )
36		eqid	⊢ ( ·sf ‘ 𝑊 ) = ( ·sf ‘ 𝑊 )
37	26 1 14 36 2	scafval	⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐹 ) ∧ 𝐵 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ( ·sf ‘ 𝑊 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
38	23 35 37	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·sf ‘ 𝑊 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
39	38	3impa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·sf ‘ 𝑊 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
40	39	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·sf ‘ 𝑊 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 · 𝐵 ) ) )
41	36 3 1 4	vscacn	⊢ ( 𝑊 ∈ TopMod → ( ·sf ‘ 𝑊 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
42	5 41	syl	⊢ ( 𝜑 → ( ·sf ‘ 𝑊 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
43	6 7 8 9 42	cnmpt22f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·sf ‘ 𝑊 ) 𝐵 ) ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) )
44	40 43	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝐽 ) )