Step | Hyp | Ref
| Expression |
1 | | tsmsmhm.2 |
. . . 4
β’ (π β πΊ β TopSp) |
2 | | tsmsmhm.b |
. . . . 5
β’ π΅ = (BaseβπΊ) |
3 | | tsmsmhm.j |
. . . . 5
β’ π½ = (TopOpenβπΊ) |
4 | 2, 3 | istps 22299 |
. . . 4
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
5 | 1, 4 | sylib 217 |
. . 3
β’ (π β π½ β (TopOnβπ΅)) |
6 | | eqid 2733 |
. . . . 5
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
7 | | eqid 2733 |
. . . . 5
β’ (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
8 | | eqid 2733 |
. . . . 5
β’ ran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
9 | | tsmsmhm.a |
. . . . 5
β’ (π β π΄ β π) |
10 | 6, 7, 8, 9 | tsmsfbas 23495 |
. . . 4
β’ (π β ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) β (fBasβ(π« π΄ β© Fin))) |
11 | | fgcl 23245 |
. . . 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 23496 |
. . . 4
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π§)) β π΅) |
16 | 15 | fmpttd 7064 |
. . 3
β’ (π β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))):(π« π΄ β© Fin)βΆπ΅) |
17 | | tsmsmhm.x |
. . . 4
β’ (π β π β (πΊ tsums πΉ)) |
18 | 2, 3, 6, 8, 1, 9, 14 | tsmsval 23498 |
. . . 4
β’ (π β (πΊ tsums πΉ) = ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
19 | 17, 18 | eleqtrd 2836 |
. . 3
β’ (π β π β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
20 | | tsmsmhm.6 |
. . . 4
β’ (π β πΆ β (π½ Cn πΎ)) |
21 | 2, 13, 1, 9, 14 | tsmscl 23502 |
. . . . . 6
β’ (π β (πΊ tsums πΉ) β π΅) |
22 | 21, 17 | sseldd 3946 |
. . . . 5
β’ (π β π β π΅) |
23 | | toponuni 22279 |
. . . . . 6
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) |
24 | 5, 23 | syl 17 |
. . . . 5
β’ (π β π΅ = βͺ π½) |
25 | 22, 24 | eleqtrd 2836 |
. . . 4
β’ (π β π β βͺ π½) |
26 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
27 | 26 | cncnpi 22645 |
. . . 4
β’ ((πΆ β (π½ Cn πΎ) β§ π β βͺ π½) β πΆ β ((π½ CnP πΎ)βπ)) |
28 | 20, 25, 27 | syl2anc 585 |
. . 3
β’ (π β πΆ β ((π½ CnP πΎ)βπ)) |
29 | | flfcnp 23371 |
. . 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 (πΉ βΎ π§)))))) |
30 | 5, 12, 16, 19, 28, 29 | syl32anc 1379 |
. 2
β’ (π β (πΆβπ) β ((πΎ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(πΆ β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))))) |
31 | | eqid 2733 |
. . . 4
β’
(Baseβπ») =
(Baseβπ») |
32 | | tsmsmhm.k |
. . . 4
β’ πΎ = (TopOpenβπ») |
33 | | tsmsmhm.3 |
. . . 4
β’ (π β π» β CMnd) |
34 | | tsmsmhm.4 |
. . . . . . 7
β’ (π β π» β TopSp) |
35 | 31, 32 | istps 22299 |
. . . . . . 7
β’ (π» β TopSp β πΎ β
(TopOnβ(Baseβπ»))) |
36 | 34, 35 | sylib 217 |
. . . . . 6
β’ (π β πΎ β (TopOnβ(Baseβπ»))) |
37 | | cnf2 22616 |
. . . . . 6
β’ ((π½ β (TopOnβπ΅) β§ πΎ β (TopOnβ(Baseβπ»)) β§ πΆ β (π½ Cn πΎ)) β πΆ:π΅βΆ(Baseβπ»)) |
38 | 5, 36, 20, 37 | syl3anc 1372 |
. . . . 5
β’ (π β πΆ:π΅βΆ(Baseβπ»)) |
39 | | fco 6693 |
. . . . 5
β’ ((πΆ:π΅βΆ(Baseβπ») β§ πΉ:π΄βΆπ΅) β (πΆ β πΉ):π΄βΆ(Baseβπ»)) |
40 | 38, 14, 39 | syl2anc 585 |
. . . 4
β’ (π β (πΆ β πΉ):π΄βΆ(Baseβπ»)) |
41 | 31, 32, 6, 8, 33, 9,
40 | tsmsval 23498 |
. . 3
β’ (π β (π» tsums (πΆ β πΉ)) = ((πΎ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (π» Ξ£g ((πΆ β πΉ) βΎ π§))))) |
42 | 38, 15 | cofmpt 7079 |
. . . . 5
β’ (π β (πΆ β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))) = (π§ β (π« π΄ β© Fin) β¦ (πΆβ(πΊ Ξ£g (πΉ βΎ π§))))) |
43 | | resco 6203 |
. . . . . . . 8
β’ ((πΆ β πΉ) βΎ π§) = (πΆ β (πΉ βΎ π§)) |
44 | 43 | oveq2i 7369 |
. . . . . . 7
β’ (π» Ξ£g
((πΆ β πΉ) βΎ π§)) = (π» Ξ£g (πΆ β (πΉ βΎ π§))) |
45 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπΊ) = (0gβπΊ) |
46 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β πΊ β CMnd) |
47 | 33 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β (π« π΄ β© Fin)) β π» β CMnd) |
48 | | cmnmnd 19584 |
. . . . . . . . 9
β’ (π» β CMnd β π» β Mnd) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β π» β Mnd) |
50 | | elinel2 4157 |
. . . . . . . . 9
β’ (π§ β (π« π΄ β© Fin) β π§ β Fin) |
51 | 50 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β π§ β Fin) |
52 | | tsmsmhm.5 |
. . . . . . . . 9
β’ (π β πΆ β (πΊ MndHom π»)) |
53 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β πΆ β (πΊ MndHom π»)) |
54 | | elfpw 9301 |
. . . . . . . . . 10
β’ (π§ β (π« π΄ β© Fin) β (π§ β π΄ β§ π§ β Fin)) |
55 | 54 | simplbi 499 |
. . . . . . . . 9
β’ (π§ β (π« π΄ β© Fin) β π§ β π΄) |
56 | | fssres 6709 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π§ β π΄) β (πΉ βΎ π§):π§βΆπ΅) |
57 | 14, 55, 56 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§):π§βΆπ΅) |
58 | | fvexd 6858 |
. . . . . . . . 9
β’ ((π β§ π§ β (π« π΄ β© Fin)) β
(0gβπΊ)
β V) |
59 | 57, 51, 58 | fdmfifsupp 9320 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§) finSupp (0gβπΊ)) |
60 | 2, 45, 46, 49, 51, 53, 57, 59 | gsummhm 19720 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (π» Ξ£g (πΆ β (πΉ βΎ π§))) = (πΆβ(πΊ Ξ£g (πΉ βΎ π§)))) |
61 | 44, 60 | eqtrid 2785 |
. . . . . 6
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (π» Ξ£g ((πΆ β πΉ) βΎ π§)) = (πΆβ(πΊ Ξ£g (πΉ βΎ π§)))) |
62 | 61 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π§ β (π« π΄ β© Fin) β¦ (π» Ξ£g ((πΆ β πΉ) βΎ π§))) = (π§ β (π« π΄ β© Fin) β¦ (πΆβ(πΊ Ξ£g (πΉ βΎ π§))))) |
63 | 42, 62 | eqtr4d 2776 |
. . . 4
β’ (π β (πΆ β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))) = (π§ β (π« π΄ β© Fin) β¦ (π» Ξ£g ((πΆ β πΉ) βΎ π§)))) |
64 | 63 | fveq2d 6847 |
. . 3
β’ (π β ((πΎ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(πΆ β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) = ((πΎ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (π» Ξ£g ((πΆ β πΉ) βΎ π§))))) |
65 | 41, 64 | eqtr4d 2776 |
. 2
β’ (π β (π» tsums (πΆ β πΉ)) = ((πΎ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(πΆ β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))))) |
66 | 30, 65 | eleqtrrd 2837 |
1
β’ (π β (πΆβπ) β (π» tsums (πΆ β πΉ))) |