Step | Hyp | Ref
| Expression |
1 | | tsmsadd.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
2 | | tsmsadd.1 |
. . . . . 6
β’ (π β πΊ β CMnd) |
3 | | tsmsadd.2 |
. . . . . . 7
β’ (π β πΊ β TopMnd) |
4 | | tmdtps 23379 |
. . . . . . 7
β’ (πΊ β TopMnd β πΊ β TopSp) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π β πΊ β TopSp) |
6 | | tsmsadd.a |
. . . . . 6
β’ (π β π΄ β π) |
7 | | tsmsadd.f |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
8 | 1, 2, 5, 6, 7 | tsmscl 23438 |
. . . . 5
β’ (π β (πΊ tsums πΉ) β π΅) |
9 | | tsmsadd.x |
. . . . 5
β’ (π β π β (πΊ tsums πΉ)) |
10 | 8, 9 | sseldd 3943 |
. . . 4
β’ (π β π β π΅) |
11 | | tsmsadd.h |
. . . . . 6
β’ (π β π»:π΄βΆπ΅) |
12 | 1, 2, 5, 6, 11 | tsmscl 23438 |
. . . . 5
β’ (π β (πΊ tsums π») β π΅) |
13 | | tsmsadd.y |
. . . . 5
β’ (π β π β (πΊ tsums π»)) |
14 | 12, 13 | sseldd 3943 |
. . . 4
β’ (π β π β π΅) |
15 | | tsmsadd.p |
. . . . 5
β’ + =
(+gβπΊ) |
16 | | eqid 2737 |
. . . . 5
β’
(+πβπΊ) = (+πβπΊ) |
17 | 1, 15, 16 | plusfval 18464 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β (π(+πβπΊ)π) = (π + π)) |
18 | 10, 14, 17 | syl2anc 584 |
. . 3
β’ (π β (π(+πβπΊ)π) = (π + π)) |
19 | | eqid 2737 |
. . . . . 6
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
20 | 1, 19 | istps 22235 |
. . . . 5
β’ (πΊ β TopSp β
(TopOpenβπΊ) β
(TopOnβπ΅)) |
21 | 5, 20 | sylib 217 |
. . . 4
β’ (π β (TopOpenβπΊ) β (TopOnβπ΅)) |
22 | | eqid 2737 |
. . . . . 6
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
23 | | eqid 2737 |
. . . . . 6
β’ (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
24 | | eqid 2737 |
. . . . . 6
β’ ran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
25 | 22, 23, 24, 6 | tsmsfbas 23431 |
. . . . 5
β’ (π β ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) β (fBasβ(π« π΄ β© Fin))) |
26 | | fgcl 23181 |
. . . . 5
β’ (ran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) β (fBasβ(π« π΄ β© Fin)) β ((π«
π΄ β© Fin)filGenran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})) β (Filβ(π« π΄ β© Fin))) |
27 | 25, 26 | syl 17 |
. . . 4
β’ (π β ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})) β (Filβ(π« π΄ β© Fin))) |
28 | 1, 22, 2, 6, 7 | tsmslem1 23432 |
. . . 4
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π§)) β π΅) |
29 | 1, 22, 2, 6, 11 | tsmslem1 23432 |
. . . 4
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (π» βΎ π§)) β π΅) |
30 | 1, 19, 22, 24, 2, 6, 7 | tsmsval 23434 |
. . . . 5
β’ (π β (πΊ tsums πΉ) = (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
31 | 9, 30 | eleqtrd 2840 |
. . . 4
β’ (π β π β (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
32 | 1, 19, 22, 24, 2, 6, 11 | tsmsval 23434 |
. . . . 5
β’ (π β (πΊ tsums π») = (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (π» βΎ π§))))) |
33 | 13, 32 | eleqtrd 2840 |
. . . 4
β’ (π β π β (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (π» βΎ π§))))) |
34 | 19, 16 | tmdcn 23386 |
. . . . . 6
β’ (πΊ β TopMnd β
(+πβπΊ) β (((TopOpenβπΊ) Γt (TopOpenβπΊ)) Cn (TopOpenβπΊ))) |
35 | 3, 34 | syl 17 |
. . . . 5
β’ (π β
(+πβπΊ) β (((TopOpenβπΊ) Γt (TopOpenβπΊ)) Cn (TopOpenβπΊ))) |
36 | 10, 14 | opelxpd 5669 |
. . . . . 6
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
37 | | txtopon 22894 |
. . . . . . . 8
β’
(((TopOpenβπΊ)
β (TopOnβπ΅)
β§ (TopOpenβπΊ)
β (TopOnβπ΅))
β ((TopOpenβπΊ)
Γt (TopOpenβπΊ)) β (TopOnβ(π΅ Γ π΅))) |
38 | 21, 21, 37 | syl2anc 584 |
. . . . . . 7
β’ (π β ((TopOpenβπΊ) Γt
(TopOpenβπΊ)) β
(TopOnβ(π΅ Γ
π΅))) |
39 | | toponuni 22215 |
. . . . . . 7
β’
(((TopOpenβπΊ)
Γt (TopOpenβπΊ)) β (TopOnβ(π΅ Γ π΅)) β (π΅ Γ π΅) = βͺ
((TopOpenβπΊ)
Γt (TopOpenβπΊ))) |
40 | 38, 39 | syl 17 |
. . . . . 6
β’ (π β (π΅ Γ π΅) = βͺ
((TopOpenβπΊ)
Γt (TopOpenβπΊ))) |
41 | 36, 40 | eleqtrd 2840 |
. . . . 5
β’ (π β β¨π, πβ© β βͺ
((TopOpenβπΊ)
Γt (TopOpenβπΊ))) |
42 | | eqid 2737 |
. . . . . 6
β’ βͺ ((TopOpenβπΊ) Γt (TopOpenβπΊ)) = βͺ ((TopOpenβπΊ) Γt (TopOpenβπΊ)) |
43 | 42 | cncnpi 22581 |
. . . . 5
β’
(((+πβπΊ) β (((TopOpenβπΊ) Γt (TopOpenβπΊ)) Cn (TopOpenβπΊ)) β§ β¨π, πβ© β βͺ
((TopOpenβπΊ)
Γt (TopOpenβπΊ))) β
(+πβπΊ) β ((((TopOpenβπΊ) Γt (TopOpenβπΊ)) CnP (TopOpenβπΊ))ββ¨π, πβ©)) |
44 | 35, 41, 43 | syl2anc 584 |
. . . 4
β’ (π β
(+πβπΊ) β ((((TopOpenβπΊ) Γt (TopOpenβπΊ)) CnP (TopOpenβπΊ))ββ¨π, πβ©)) |
45 | 21, 21, 27, 28, 29, 31, 33, 44 | flfcnp2 23310 |
. . 3
β’ (π β (π(+πβπΊ)π) β (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§)))))) |
46 | 18, 45 | eqeltrrd 2839 |
. 2
β’ (π β (π + π) β (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§)))))) |
47 | | cmnmnd 19538 |
. . . . . . 7
β’ (πΊ β CMnd β πΊ β Mnd) |
48 | 2, 47 | syl 17 |
. . . . . 6
β’ (π β πΊ β Mnd) |
49 | 1, 15 | mndcl 18524 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
50 | 49 | 3expb 1120 |
. . . . . 6
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
51 | 48, 50 | sylan 580 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
52 | | inidm 4176 |
. . . . 5
β’ (π΄ β© π΄) = π΄ |
53 | 51, 7, 11, 6, 6, 52 | off 7627 |
. . . 4
β’ (π β (πΉ βf + π»):π΄βΆπ΅) |
54 | 1, 19, 22, 24, 2, 6, 53 | tsmsval 23434 |
. . 3
β’ (π β (πΊ tsums (πΉ βf + π»)) = (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g ((πΉ βf + π») βΎ π§))))) |
55 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
56 | 2 | adantr 481 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β πΊ β CMnd) |
57 | | elinel2 4154 |
. . . . . . . 8
β’ (π§ β (π« π΄ β© Fin) β π§ β Fin) |
58 | 57 | adantl 482 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β π§ β Fin) |
59 | | elfpw 9256 |
. . . . . . . . 9
β’ (π§ β (π« π΄ β© Fin) β (π§ β π΄ β§ π§ β Fin)) |
60 | 59 | simplbi 498 |
. . . . . . . 8
β’ (π§ β (π« π΄ β© Fin) β π§ β π΄) |
61 | | fssres 6705 |
. . . . . . . 8
β’ ((πΉ:π΄βΆπ΅ β§ π§ β π΄) β (πΉ βΎ π§):π§βΆπ΅) |
62 | 7, 60, 61 | syl2an 596 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§):π§βΆπ΅) |
63 | | fssres 6705 |
. . . . . . . 8
β’ ((π»:π΄βΆπ΅ β§ π§ β π΄) β (π» βΎ π§):π§βΆπ΅) |
64 | 11, 60, 63 | syl2an 596 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (π» βΎ π§):π§βΆπ΅) |
65 | | fvexd 6854 |
. . . . . . . 8
β’ ((π β§ π§ β (π« π΄ β© Fin)) β
(0gβπΊ)
β V) |
66 | 62, 58, 65 | fdmfifsupp 9273 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§) finSupp (0gβπΊ)) |
67 | 64, 58, 65 | fdmfifsupp 9273 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (π» βΎ π§) finSupp (0gβπΊ)) |
68 | 1, 55, 15, 56, 58, 62, 64, 66, 67 | gsumadd 19659 |
. . . . . 6
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g ((πΉ βΎ π§) βf + (π» βΎ π§))) = ((πΊ Ξ£g (πΉ βΎ π§)) + (πΊ Ξ£g (π» βΎ π§)))) |
69 | 7, 6 | fexd 7173 |
. . . . . . . . 9
β’ (π β πΉ β V) |
70 | 11, 6 | fexd 7173 |
. . . . . . . . 9
β’ (π β π» β V) |
71 | | offres 7908 |
. . . . . . . . 9
β’ ((πΉ β V β§ π» β V) β ((πΉ βf + π») βΎ π§) = ((πΉ βΎ π§) βf + (π» βΎ π§))) |
72 | 69, 70, 71 | syl2anc 584 |
. . . . . . . 8
β’ (π β ((πΉ βf + π») βΎ π§) = ((πΉ βΎ π§) βf + (π» βΎ π§))) |
73 | 72 | adantr 481 |
. . . . . . 7
β’ ((π β§ π§ β (π« π΄ β© Fin)) β ((πΉ βf + π») βΎ π§) = ((πΉ βΎ π§) βf + (π» βΎ π§))) |
74 | 73 | oveq2d 7367 |
. . . . . 6
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g ((πΉ βf + π») βΎ π§)) = (πΊ Ξ£g ((πΉ βΎ π§) βf + (π» βΎ π§)))) |
75 | 1, 15, 16 | plusfval 18464 |
. . . . . . 7
β’ (((πΊ Ξ£g
(πΉ βΎ π§)) β π΅ β§ (πΊ Ξ£g (π» βΎ π§)) β π΅) β ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§))) = ((πΊ Ξ£g (πΉ βΎ π§)) + (πΊ Ξ£g (π» βΎ π§)))) |
76 | 28, 29, 75 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π§ β (π« π΄ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§))) = ((πΊ Ξ£g (πΉ βΎ π§)) + (πΊ Ξ£g (π» βΎ π§)))) |
77 | 68, 74, 76 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g ((πΉ βf + π») βΎ π§)) = ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§)))) |
78 | 77 | mpteq2dva 5203 |
. . . 4
β’ (π β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g ((πΉ βf + π») βΎ π§))) = (π§ β (π« π΄ β© Fin) β¦ ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§))))) |
79 | 78 | fveq2d 6843 |
. . 3
β’ (π β (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g ((πΉ βf + π») βΎ π§)))) = (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§)))))) |
80 | 54, 79 | eqtrd 2777 |
. 2
β’ (π β (πΊ tsums (πΉ βf + π»)) = (((TopOpenβπΊ) fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ ((πΊ Ξ£g (πΉ βΎ π§))(+πβπΊ)(πΊ Ξ£g (π» βΎ π§)))))) |
81 | 46, 80 | eleqtrrd 2841 |
1
β’ (π β (π + π) β (πΊ tsums (πΉ βf + π»))) |