Step | Hyp | Ref
| Expression |
1 | | tsmsmhm.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) |
2 | | tsmsmhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
3 | | tsmsmhm.j |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝐺) |
4 | 2, 3 | istps 20738 |
. . . 4
⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵)) |
5 | 1, 4 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
6 | | eqid 2622 |
. . . . 5
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
7 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) |
8 | | eqid 2622 |
. . . . 5
⊢ ran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) |
9 | | tsmsmhm.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
10 | 6, 7, 8, 9 | tsmsfbas 21931 |
. . . 4
⊢ (𝜑 → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin))) |
11 | | fgcl 21682 |
. . . 4
⊢ (ran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)) → ((𝒫
𝐴 ∩ Fin)filGenran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin))) |
12 | 10, 11 | syl 17 |
. . 3
⊢ (𝜑 → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin))) |
13 | | tsmsmhm.1 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ CMnd) |
14 | | tsmsmhm.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | 2, 6, 13, 9, 14 | tsmslem1 21932 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝐵) |
16 | | eqid 2622 |
. . . 4
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))) |
17 | 15, 16 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))):(𝒫 𝐴 ∩ Fin)⟶𝐵) |
18 | | tsmsmhm.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
19 | 2, 3, 6, 8, 1, 9, 14 | tsmsval 21934 |
. . . 4
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) |
20 | 18, 19 | eleqtrd 2703 |
. . 3
⊢ (𝜑 → 𝑋 ∈ ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) |
21 | | tsmsmhm.6 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐽 Cn 𝐾)) |
22 | 2, 13, 1, 9, 14 | tsmscl 21938 |
. . . . . 6
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
23 | 22, 18 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | | toponuni 20719 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
25 | 5, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
26 | 23, 25 | eleqtrd 2703 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ∪ 𝐽) |
27 | | eqid 2622 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
28 | 27 | cncnpi 21082 |
. . . 4
⊢ ((𝐶 ∈ (𝐽 Cn 𝐾) ∧ 𝑋 ∈ ∪ 𝐽) → 𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋)) |
29 | 21, 26, 28 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋)) |
30 | | flfcnp 21808 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝐵) ∧ ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑧))):(𝒫 𝐴 ∩ Fin)⟶𝐵) ∧ (𝑋 ∈ ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋))) → (𝐶‘𝑋) ∈ ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))))) |
31 | 5, 12, 17, 20, 29, 30 | syl32anc 1334 |
. 2
⊢ (𝜑 → (𝐶‘𝑋) ∈ ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))))) |
32 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
33 | | tsmsmhm.k |
. . . 4
⊢ 𝐾 = (TopOpen‘𝐻) |
34 | | tsmsmhm.3 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ CMnd) |
35 | | tsmsmhm.4 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ TopSp) |
36 | 32, 33 | istps 20738 |
. . . . . . 7
⊢ (𝐻 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐻))) |
37 | 35, 36 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝐻))) |
38 | | cnf2 21053 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐶 ∈ (𝐽 Cn 𝐾)) → 𝐶:𝐵⟶(Base‘𝐻)) |
39 | 5, 37, 21, 38 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐶:𝐵⟶(Base‘𝐻)) |
40 | | fco 6058 |
. . . . 5
⊢ ((𝐶:𝐵⟶(Base‘𝐻) ∧ 𝐹:𝐴⟶𝐵) → (𝐶 ∘ 𝐹):𝐴⟶(Base‘𝐻)) |
41 | 39, 14, 40 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐶 ∘ 𝐹):𝐴⟶(Base‘𝐻)) |
42 | 32, 33, 6, 8, 34, 9,
41 | tsmsval 21934 |
. . 3
⊢ (𝜑 → (𝐻 tsums (𝐶 ∘ 𝐹)) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶 ∘ 𝐹) ↾ 𝑧))))) |
43 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))) |
44 | 39 | feqmptd 6249 |
. . . . . 6
⊢ (𝜑 → 𝐶 = (𝑤 ∈ 𝐵 ↦ (𝐶‘𝑤))) |
45 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝐶‘𝑤) = (𝐶‘(𝐺 Σg (𝐹 ↾ 𝑧)))) |
46 | 15, 43, 44, 45 | fmptco 6396 |
. . . . 5
⊢ (𝜑 → (𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐶‘(𝐺 Σg (𝐹 ↾ 𝑧))))) |
47 | | resco 5639 |
. . . . . . . 8
⊢ ((𝐶 ∘ 𝐹) ↾ 𝑧) = (𝐶 ∘ (𝐹 ↾ 𝑧)) |
48 | 47 | oveq2i 6661 |
. . . . . . 7
⊢ (𝐻 Σg
((𝐶 ∘ 𝐹) ↾ 𝑧)) = (𝐻 Σg (𝐶 ∘ (𝐹 ↾ 𝑧))) |
49 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
50 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
51 | 34 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ CMnd) |
52 | | cmnmnd 18208 |
. . . . . . . . 9
⊢ (𝐻 ∈ CMnd → 𝐻 ∈ Mnd) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ Mnd) |
54 | | elfpw 8268 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) |
55 | 54 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin) |
56 | 55 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin) |
57 | | tsmsmhm.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (𝐺 MndHom 𝐻)) |
58 | 57 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐶 ∈ (𝐺 MndHom 𝐻)) |
59 | 54 | simplbi 476 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ⊆ 𝐴) |
60 | | fssres 6070 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ⊆ 𝐴) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
61 | 14, 59, 60 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
62 | | fvexd 6203 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐺)
∈ V) |
63 | 61, 56, 62 | fdmfifsupp 8285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
64 | 2, 49, 50, 53, 56, 58, 61, 63 | gsummhm 18338 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐶 ∘ (𝐹 ↾ 𝑧))) = (𝐶‘(𝐺 Σg (𝐹 ↾ 𝑧)))) |
65 | 48, 64 | syl5eq 2668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg ((𝐶 ∘ 𝐹) ↾ 𝑧)) = (𝐶‘(𝐺 Σg (𝐹 ↾ 𝑧)))) |
66 | 65 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶 ∘ 𝐹) ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐶‘(𝐺 Σg (𝐹 ↾ 𝑧))))) |
67 | 46, 66 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → (𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶 ∘ 𝐹) ↾ 𝑧)))) |
68 | 67 | fveq2d 6195 |
. . 3
⊢ (𝜑 → ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶 ∘ 𝐹) ↾ 𝑧))))) |
69 | 42, 68 | eqtr4d 2659 |
. 2
⊢ (𝜑 → (𝐻 tsums (𝐶 ∘ 𝐹)) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))))) |
70 | 31, 69 | eleqtrrd 2704 |
1
⊢ (𝜑 → (𝐶‘𝑋) ∈ (𝐻 tsums (𝐶 ∘ 𝐹))) |