Metamath Proof Explorer

Theorem 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 ⊢ F = Scalar ⁡ W
cnmpt1vsca.t ⊢ · ˙ = ⋅ W
cnmpt1vsca.j ⊢ J = TopOpen ⁡ W
cnmpt1vsca.k ⊢ K = TopOpen ⁡ F
cnmpt1vsca.w ⊢ φ → W ∈ TopMod
cnmpt1vsca.l ⊢ φ → L ∈ TopOn ⁡ X
cnmpt1vsca.a ⊢ φ → x ∈ X ⟼ A ∈ L Cn K
cnmpt1vsca.b ⊢ φ → x ∈ X ⟼ B ∈ L Cn J
Assertion cnmpt1vsca ⊢ φ → x ∈ X ⟼ A · ˙ B ∈ L Cn J

Proof

Step Hyp Ref Expression
1 tlmtrg.f ⊢ F = Scalar ⁡ W
2 cnmpt1vsca.t ⊢ · ˙ = ⋅ W
3 cnmpt1vsca.j ⊢ J = TopOpen ⁡ W
4 cnmpt1vsca.k ⊢ K = TopOpen ⁡ F
5 cnmpt1vsca.w ⊢ φ → W ∈ TopMod
6 cnmpt1vsca.l ⊢ φ → L ∈ TopOn ⁡ X
7 cnmpt1vsca.a ⊢ φ → x ∈ X ⟼ A ∈ L Cn K
8 cnmpt1vsca.b ⊢ φ → x ∈ X ⟼ B ∈ L Cn J
9 1 tlmscatps ⊢ W ∈ TopMod → F ∈ TopSp
10 5 9 syl ⊢ φ → F ∈ TopSp
11 eqid ⊢ Base F = Base F
12 11 4 istps ⊢ F ∈ TopSp ↔ K ∈ TopOn ⁡ Base F
13 10 12 sylib ⊢ φ → K ∈ TopOn ⁡ Base F
14 cnf2 ⊢ L ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Base F ∧ x ∈ X ⟼ A ∈ L Cn K → x ∈ X ⟼ A : X ⟶ Base F
15 6 13 7 14 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Base F
16 15 fvmptelrn ⊢ φ ∧ x ∈ X → A ∈ Base F
17 tlmtps ⊢ W ∈ TopMod → W ∈ TopSp
18 5 17 syl ⊢ φ → W ∈ TopSp
19 eqid ⊢ Base W = Base W
20 19 3 istps ⊢ W ∈ TopSp ↔ J ∈ TopOn ⁡ Base W
21 18 20 sylib ⊢ φ → J ∈ TopOn ⁡ Base W
22 cnf2 ⊢ L ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base W ∧ x ∈ X ⟼ B ∈ L Cn J → x ∈ X ⟼ B : X ⟶ Base W
23 6 21 8 22 syl3anc ⊢ φ → x ∈ X ⟼ B : X ⟶ Base W
24 23 fvmptelrn ⊢ φ ∧ x ∈ X → B ∈ Base W
25 eqid ⊢ ⋅ 𝑠𝑓 ⁡ W = ⋅ 𝑠𝑓 ⁡ W
26 19 1 11 25 2 scafval ⊢ A ∈ Base F ∧ B ∈ Base W → A ⋅ 𝑠𝑓 ⁡ W B = A · ˙ B
27 16 24 26 syl2anc ⊢ φ ∧ x ∈ X → A ⋅ 𝑠𝑓 ⁡ W B = A · ˙ B
28 27 mpteq2dva ⊢ φ → x ∈ X ⟼ A ⋅ 𝑠𝑓 ⁡ W B = x ∈ X ⟼ A · ˙ B
29 25 3 1 4 vscacn ⊢ W ∈ TopMod → ⋅ 𝑠𝑓 ⁡ W ∈ K × t J Cn J
30 5 29 syl ⊢ φ → ⋅ 𝑠𝑓 ⁡ W ∈ K × t J Cn J
31 6 7 8 30 cnmpt12f ⊢ φ → x ∈ X ⟼ A ⋅ 𝑠𝑓 ⁡ W B ∈ L Cn J
32 28 31 eqeltrrd ⊢ φ → x ∈ X ⟼ A · ˙ B ∈ L Cn J