This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐽 ) )