Proof of Theorem cnmpt1vsca
Step | Hyp | Ref
| Expression |
1 | | cnmpt1vsca.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋)) |
2 | | cnmpt1vsca.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ TopMod) |
3 | | tlmtrg.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
4 | 3 | tlmscatps 21804 |
. . . . . . . . 9
⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ TopSp) |
6 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐹) =
(Base‘𝐹) |
7 | | cnmpt1vsca.k |
. . . . . . . . 9
⊢ 𝐾 = (TopOpen‘𝐹) |
8 | 6, 7 | istps 20551 |
. . . . . . . 8
⊢ (𝐹 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐹))) |
9 | 5, 8 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝐹))) |
10 | | cnmpt1vsca.a |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐿 Cn 𝐾)) |
11 | | cnf2 20863 |
. . . . . . 7
⊢ ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐹)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐿 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶(Base‘𝐹)) |
12 | 1, 9, 10, 11 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶(Base‘𝐹)) |
13 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
14 | 13 | fmpt 6289 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ (Base‘𝐹) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶(Base‘𝐹)) |
15 | 12, 14 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐴 ∈ (Base‘𝐹)) |
16 | 15 | r19.21bi 2916 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ (Base‘𝐹)) |
17 | | tlmtps 21801 |
. . . . . . . . 9
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) |
18 | 2, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ TopSp) |
19 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) |
20 | | cnmpt1vsca.j |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝑊) |
21 | 19, 20 | istps 20551 |
. . . . . . . 8
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑊))) |
22 | 18, 21 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑊))) |
23 | | cnmpt1vsca.b |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐿 Cn 𝐽)) |
24 | | cnf2 20863 |
. . . . . . 7
⊢ ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘(Base‘𝑊)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐿 Cn 𝐽)) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶(Base‘𝑊)) |
25 | 1, 22, 23, 24 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶(Base‘𝑊)) |
26 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ 𝐵) |
27 | 26 | fmpt 6289 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 𝐵 ∈ (Base‘𝑊) ↔ (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶(Base‘𝑊)) |
28 | 25, 27 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ (Base‘𝑊)) |
29 | 28 | r19.21bi 2916 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (Base‘𝑊)) |
30 | | eqid 2610 |
. . . . 5
⊢ (
·sf ‘𝑊) = ( ·sf
‘𝑊) |
31 | | cnmpt1vsca.t |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
32 | 19, 3, 6, 30, 31 | scafval 18705 |
. . . 4
⊢ ((𝐴 ∈ (Base‘𝐹) ∧ 𝐵 ∈ (Base‘𝑊)) → (𝐴( ·sf
‘𝑊)𝐵) = (𝐴 · 𝐵)) |
33 | 16, 29, 32 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴( ·sf
‘𝑊)𝐵) = (𝐴 · 𝐵)) |
34 | 33 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴( ·sf
‘𝑊)𝐵)) = (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))) |
35 | 30, 20, 3, 7 | vscacn 21799 |
. . . 4
⊢ (𝑊 ∈ TopMod → (
·sf ‘𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) |
36 | 2, 35 | syl 17 |
. . 3
⊢ (𝜑 → (
·sf ‘𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) |
37 | 1, 10, 23, 36 | cnmpt12f 21279 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴( ·sf
‘𝑊)𝐵)) ∈ (𝐿 Cn 𝐽)) |
38 | 34, 37 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽)) |