Step | Hyp | Ref
| Expression |
1 | | df-tsms 23494 |
. . 3
β’ tsums =
(π€ β V, π β V β¦
β¦(π« dom π β© Fin) / π β¦(((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦))))) |
2 | 1 | a1i 11 |
. 2
β’ (π β tsums = (π€ β V, π β V β¦ β¦(π«
dom π β© Fin) / π β¦(((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦)))))) |
3 | | vex 3448 |
. . . . . . 7
β’ π β V |
4 | 3 | dmex 7849 |
. . . . . 6
β’ dom π β V |
5 | 4 | pwex 5336 |
. . . . 5
β’ π«
dom π β
V |
6 | 5 | inex1 5275 |
. . . 4
β’
(π« dom π
β© Fin) β V |
7 | 6 | a1i 11 |
. . 3
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β (π« dom π β© Fin) β V) |
8 | | simplrl 776 |
. . . . . . 7
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β π€ = πΊ) |
9 | 8 | fveq2d 6847 |
. . . . . 6
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (TopOpenβπ€) = (TopOpenβπΊ)) |
10 | | tsmsval.j |
. . . . . 6
β’ π½ = (TopOpenβπΊ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . 5
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (TopOpenβπ€) = π½) |
12 | | id 22 |
. . . . . . 7
β’ (π = (π« dom π β© Fin) β π = (π« dom π β© Fin)) |
13 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β π = πΉ) |
14 | 13 | dmeqd 5862 |
. . . . . . . . . . 11
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β dom π = dom πΉ) |
15 | | tsmsval2.a |
. . . . . . . . . . . 12
β’ (π β dom πΉ = π΄) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β dom πΉ = π΄) |
17 | 14, 16 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β dom π = π΄) |
18 | 17 | pweqd 4578 |
. . . . . . . . 9
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β π« dom π = π« π΄) |
19 | 18 | ineq1d 4172 |
. . . . . . . 8
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β (π« dom π β© Fin) = (π« π΄ β© Fin)) |
20 | | tsmsval.s |
. . . . . . . 8
β’ π = (π« π΄ β© Fin) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β (π« dom π β© Fin) = π) |
22 | 12, 21 | sylan9eqr 2795 |
. . . . . 6
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β π = π) |
23 | 22 | rabeqdv 3421 |
. . . . . . . . 9
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β {π¦ β π β£ π§ β π¦} = {π¦ β π β£ π§ β π¦}) |
24 | 22, 23 | mpteq12dv 5197 |
. . . . . . . 8
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = (π§ β π β¦ {π¦ β π β£ π§ β π¦})) |
25 | 24 | rneqd 5894 |
. . . . . . 7
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})) |
26 | | tsmsval.l |
. . . . . . 7
β’ πΏ = ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) |
27 | 25, 26 | eqtr4di 2791 |
. . . . . 6
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = πΏ) |
28 | 22, 27 | oveq12d 7376 |
. . . . 5
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})) = (πfilGenπΏ)) |
29 | 11, 28 | oveq12d 7376 |
. . . 4
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β ((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦}))) = (π½ fLimf (πfilGenπΏ))) |
30 | | simplrr 777 |
. . . . . . 7
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β π = πΉ) |
31 | 30 | reseq1d 5937 |
. . . . . 6
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (π βΎ π¦) = (πΉ βΎ π¦)) |
32 | 8, 31 | oveq12d 7376 |
. . . . 5
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (π€ Ξ£g (π βΎ π¦)) = (πΊ Ξ£g (πΉ βΎ π¦))) |
33 | 22, 32 | mpteq12dv 5197 |
. . . 4
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (π¦ β π β¦ (π€ Ξ£g (π βΎ π¦))) = (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) |
34 | 29, 33 | fveq12d 6850 |
. . 3
β’ (((π β§ (π€ = πΊ β§ π = πΉ)) β§ π = (π« dom π β© Fin)) β (((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦)))) = ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |
35 | 7, 34 | csbied 3894 |
. 2
β’ ((π β§ (π€ = πΊ β§ π = πΉ)) β β¦(π« dom
π β© Fin) / π β¦(((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦)))) = ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |
36 | | tsmsval.g |
. . 3
β’ (π β πΊ β π) |
37 | 36 | elexd 3464 |
. 2
β’ (π β πΊ β V) |
38 | | tsmsval2.f |
. . 3
β’ (π β πΉ β π) |
39 | 38 | elexd 3464 |
. 2
β’ (π β πΉ β V) |
40 | | fvexd 6858 |
. 2
β’ (π β ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) β V) |
41 | 2, 35, 37, 39, 40 | ovmpod 7508 |
1
β’ (π β (πΊ tsums πΉ) = ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |