Step | Hyp | Ref
| Expression |
1 | | tsmspropd.j |
. . . 4
β’ (π β (TopOpenβπΊ) = (TopOpenβπ»)) |
2 | 1 | oveq1d 7373 |
. . 3
β’ (π β ((TopOpenβπΊ) fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦}))) = ((TopOpenβπ») fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦})))) |
3 | | tsmspropd.f |
. . . . . 6
β’ (π β πΉ β π) |
4 | 3 | resexd 5985 |
. . . . 5
β’ (π β (πΉ βΎ π¦) β V) |
5 | | tsmspropd.g |
. . . . 5
β’ (π β πΊ β π) |
6 | | tsmspropd.h |
. . . . 5
β’ (π β π» β π) |
7 | | tsmspropd.b |
. . . . 5
β’ (π β (BaseβπΊ) = (Baseβπ»)) |
8 | | tsmspropd.p |
. . . . 5
β’ (π β (+gβπΊ) = (+gβπ»)) |
9 | 4, 5, 6, 7, 8 | gsumpropd 18538 |
. . . 4
β’ (π β (πΊ Ξ£g (πΉ βΎ π¦)) = (π» Ξ£g (πΉ βΎ π¦))) |
10 | 9 | mpteq2dv 5208 |
. . 3
β’ (π β (π¦ β (π« dom πΉ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))) = (π¦ β (π« dom πΉ β© Fin) β¦ (π» Ξ£g (πΉ βΎ π¦)))) |
11 | 2, 10 | fveq12d 6850 |
. 2
β’ (π β (((TopOpenβπΊ) fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦})))β(π¦ β (π« dom πΉ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) = (((TopOpenβπ») fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦})))β(π¦ β (π« dom πΉ β© Fin) β¦ (π» Ξ£g (πΉ βΎ π¦))))) |
12 | | eqid 2733 |
. . 3
β’
(BaseβπΊ) =
(BaseβπΊ) |
13 | | eqid 2733 |
. . 3
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
14 | | eqid 2733 |
. . 3
β’
(π« dom πΉ
β© Fin) = (π« dom πΉ β© Fin) |
15 | | eqid 2733 |
. . 3
β’ ran
(π§ β (π« dom
πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦}) = ran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦}) |
16 | | eqidd 2734 |
. . 3
β’ (π β dom πΉ = dom πΉ) |
17 | 12, 13, 14, 15, 5, 3, 16 | tsmsval2 23497 |
. 2
β’ (π β (πΊ tsums πΉ) = (((TopOpenβπΊ) fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦})))β(π¦ β (π« dom πΉ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |
18 | | eqid 2733 |
. . 3
β’
(Baseβπ») =
(Baseβπ») |
19 | | eqid 2733 |
. . 3
β’
(TopOpenβπ») =
(TopOpenβπ») |
20 | 18, 19, 14, 15, 6, 3, 16 | tsmsval2 23497 |
. 2
β’ (π β (π» tsums πΉ) = (((TopOpenβπ») fLimf ((π« dom πΉ β© Fin)filGenran (π§ β (π« dom πΉ β© Fin) β¦ {π¦ β (π« dom πΉ β© Fin) β£ π§ β π¦})))β(π¦ β (π« dom πΉ β© Fin) β¦ (π» Ξ£g (πΉ βΎ π¦))))) |
21 | 11, 17, 20 | 3eqtr4d 2783 |
1
β’ (π β (πΊ tsums πΉ) = (π» tsums πΉ)) |