cnmpt1vsca

Description: Continuity of scalar multiplication; analogue of cnmpt12f 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 ‘ 𝑋 ) )
	cnmpt1vsca.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐿 Cn 𝐾 ) )
	cnmpt1vsca.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐿 Cn 𝐽 ) )
Assertion	cnmpt1vsca	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝐿 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		cnmpt1vsca.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐿 Cn 𝐾 ) )
8		cnmpt1vsca.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐿 Cn 𝐽 ) )
9	1	tlmscatps	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp )
10	5 9	syl	⊢ ( 𝜑 → 𝐹 ∈ TopSp )
11		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
12	11 4	istps	⊢ ( 𝐹 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) )
13	10 12	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) )
14		cnf2	⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐿 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐹 ) )
15	6 13 7 14	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐹 ) )
16	15	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ( Base ‘ 𝐹 ) )
17		tlmtps	⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopSp )
18	5 17	syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
19		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
20	19 3	istps	⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
21	18 20	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
22		cnf2	⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐿 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
23	6 21 8 22	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
24	23	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( Base ‘ 𝑊 ) )
25		eqid	⊢ ( ·_sf ‘ 𝑊 ) = ( ·_sf ‘ 𝑊 )
26	19 1 11 25 2	scafval	⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐹 ) ∧ 𝐵 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ( ·_sf ‘ 𝑊 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
27	16 24 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( ·_sf ‘ 𝑊 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
28	27	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( ·_sf ‘ 𝑊 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) )
29	25 3 1 4	vscacn	⊢ ( 𝑊 ∈ TopMod → ( ·_sf ‘ 𝑊 ) ∈ ( ( 𝐾 ×_t 𝐽 ) Cn 𝐽 ) )
30	5 29	syl	⊢ ( 𝜑 → ( ·_sf ‘ 𝑊 ) ∈ ( ( 𝐾 ×_t 𝐽 ) Cn 𝐽 ) )
31	6 7 8 30	cnmpt12f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( ·_sf ‘ 𝑊 ) 𝐵 ) ) ∈ ( 𝐿 Cn 𝐽 ) )
32	28 31	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝐿 Cn 𝐽 ) )

Metamath Proof Explorer

Theorem cnmpt1vsca

Proof