Step | Hyp | Ref
| Expression |
1 | | tsmssubm.s |
. . . . . 6
β’ (π β π β (SubMndβπΊ)) |
2 | | tsmssubm.h |
. . . . . . 7
β’ π» = (πΊ βΎs π) |
3 | 2 | submbas 18630 |
. . . . . 6
β’ (π β (SubMndβπΊ) β π = (Baseβπ»)) |
4 | 1, 3 | syl 17 |
. . . . 5
β’ (π β π = (Baseβπ»)) |
5 | 4 | eleq2d 2820 |
. . . 4
β’ (π β (π₯ β π β π₯ β (Baseβπ»))) |
6 | 5 | anbi1d 631 |
. . 3
β’ (π β ((π₯ β π β§ βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£))) β (π₯ β (Baseβπ») β§ βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£))))) |
7 | | elin 3927 |
. . . . 5
β’ (π₯ β ((πΊ tsums πΉ) β© π) β (π₯ β (πΊ tsums πΉ) β§ π₯ β π)) |
8 | 7 | biancomi 464 |
. . . 4
β’ (π₯ β ((πΊ tsums πΉ) β© π) β (π₯ β π β§ π₯ β (πΊ tsums πΉ))) |
9 | | eqid 2733 |
. . . . . . . . . 10
β’
(BaseβπΊ) =
(BaseβπΊ) |
10 | 9 | submss 18625 |
. . . . . . . . 9
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
β’ (π β π β (BaseβπΊ)) |
12 | 11 | sselda 3945 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯ β (BaseβπΊ)) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
14 | | eqid 2733 |
. . . . . . . . 9
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
15 | | tsmssubm.1 |
. . . . . . . . 9
β’ (π β πΊ β CMnd) |
16 | | tsmssubm.2 |
. . . . . . . . 9
β’ (π β πΊ β TopSp) |
17 | | tsmssubm.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
18 | | tsmssubm.f |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆπ) |
19 | 18, 11 | fssd 6687 |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆ(BaseβπΊ)) |
20 | 9, 13, 14, 15, 16, 17, 19 | eltsms 23500 |
. . . . . . . 8
β’ (π β (π₯ β (πΊ tsums πΉ) β (π₯ β (BaseβπΊ) β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))))) |
21 | 20 | baibd 541 |
. . . . . . 7
β’ ((π β§ π₯ β (BaseβπΊ)) β (π₯ β (πΊ tsums πΉ) β βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
22 | 12, 21 | syldan 592 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π₯ β (πΊ tsums πΉ) β βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
23 | | vex 3448 |
. . . . . . . . 9
β’ π’ β V |
24 | 23 | inex1 5275 |
. . . . . . . 8
β’ (π’ β© π) β V |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π’ β (TopOpenβπΊ)) β (π’ β© π) β V) |
26 | 2, 13 | resstopn 22553 |
. . . . . . . . 9
β’
((TopOpenβπΊ)
βΎt π) =
(TopOpenβπ») |
27 | 26 | eleq2i 2826 |
. . . . . . . 8
β’ (π£ β ((TopOpenβπΊ) βΎt π) β π£ β (TopOpenβπ»)) |
28 | | fvex 6856 |
. . . . . . . . . 10
β’
(TopOpenβπΊ)
β V |
29 | | elrest 17314 |
. . . . . . . . . 10
β’
(((TopOpenβπΊ)
β V β§ π β
(SubMndβπΊ)) β
(π£ β
((TopOpenβπΊ)
βΎt π)
β βπ’ β
(TopOpenβπΊ)π£ = (π’ β© π))) |
30 | 28, 1, 29 | sylancr 588 |
. . . . . . . . 9
β’ (π β (π£ β ((TopOpenβπΊ) βΎt π) β βπ’ β (TopOpenβπΊ)π£ = (π’ β© π))) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π£ β ((TopOpenβπΊ) βΎt π) β βπ’ β (TopOpenβπΊ)π£ = (π’ β© π))) |
32 | 27, 31 | bitr3id 285 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π£ β (TopOpenβπ») β βπ’ β (TopOpenβπΊ)π£ = (π’ β© π))) |
33 | | eleq2 2823 |
. . . . . . . . 9
β’ (π£ = (π’ β© π) β (π₯ β π£ β π₯ β (π’ β© π))) |
34 | | elin 3927 |
. . . . . . . . . . 11
β’ (π₯ β (π’ β© π) β (π₯ β π’ β§ π₯ β π)) |
35 | 34 | rbaib 540 |
. . . . . . . . . 10
β’ (π₯ β π β (π₯ β (π’ β© π) β π₯ β π’)) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π₯ β (π’ β© π) β π₯ β π’)) |
37 | 33, 36 | sylan9bbr 512 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π£ = (π’ β© π)) β (π₯ β π£ β π₯ β π’)) |
38 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π£ = (π’ β© π) β ((π» Ξ£g (πΉ βΎ π¦)) β π£ β (π» Ξ£g (πΉ βΎ π¦)) β (π’ β© π))) |
39 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ») =
(Baseβπ») |
40 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(0gβπ») = (0gβπ») |
41 | 2 | submmnd 18629 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (SubMndβπΊ) β π» β Mnd) |
42 | 1, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π» β Mnd) |
43 | 2 | subcmn 19620 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β CMnd β§ π» β Mnd) β π» β CMnd) |
44 | 15, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π» β CMnd) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β π» β CMnd) |
46 | | elinel2 4157 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (π« π΄ β© Fin) β π¦ β Fin) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β π¦ β Fin) |
48 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β πΉ:π΄βΆπ) |
49 | | elfpw 9301 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β (π« π΄ β© Fin) β (π¦ β π΄ β§ π¦ β Fin)) |
50 | 49 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π« π΄ β© Fin) β π¦ β π΄) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β π¦ β π΄) |
52 | 48, 51 | fssresd 6710 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (πΉ βΎ π¦):π¦βΆπ) |
53 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β π = (Baseβπ»)) |
54 | 53 | feq3d 6656 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β ((πΉ βΎ π¦):π¦βΆπ β (πΉ βΎ π¦):π¦βΆ(Baseβπ»))) |
55 | 52, 54 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (πΉ βΎ π¦):π¦βΆ(Baseβπ»)) |
56 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’
(0gβπ») β V |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β
(0gβπ»)
β V) |
58 | 52, 47, 57 | fdmfifsupp 9320 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (πΉ βΎ π¦) finSupp (0gβπ»)) |
59 | 39, 40, 45, 47, 55, 58 | gsumcl 19697 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (π» Ξ£g (πΉ βΎ π¦)) β (Baseβπ»)) |
60 | 59, 53 | eleqtrrd 2837 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (π» Ξ£g (πΉ βΎ π¦)) β π) |
61 | | elin 3927 |
. . . . . . . . . . . . . . . 16
β’ ((π» Ξ£g
(πΉ βΎ π¦)) β (π’ β© π) β ((π» Ξ£g (πΉ βΎ π¦)) β π’ β§ (π» Ξ£g (πΉ βΎ π¦)) β π)) |
62 | 61 | rbaib 540 |
. . . . . . . . . . . . . . 15
β’ ((π» Ξ£g
(πΉ βΎ π¦)) β π β ((π» Ξ£g (πΉ βΎ π¦)) β (π’ β© π) β (π» Ξ£g (πΉ βΎ π¦)) β π’)) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β ((π» Ξ£g (πΉ βΎ π¦)) β (π’ β© π) β (π» Ξ£g (πΉ βΎ π¦)) β π’)) |
64 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β π β (SubMndβπΊ)) |
65 | 47, 64, 52, 2 | gsumsubm 18650 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π¦)) = (π» Ξ£g (πΉ βΎ π¦))) |
66 | 65 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ π¦)) β π’ β (π» Ξ£g (πΉ βΎ π¦)) β π’)) |
67 | 63, 66 | bitr4d 282 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β ((π» Ξ£g (πΉ βΎ π¦)) β (π’ β© π) β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
68 | 38, 67 | sylan9bbr 512 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π¦ β (π« π΄ β© Fin)) β§ π£ = (π’ β© π)) β ((π» Ξ£g (πΉ βΎ π¦)) β π£ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
69 | 68 | an32s 651 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π£ = (π’ β© π)) β§ π¦ β (π« π΄ β© Fin)) β ((π» Ξ£g (πΉ βΎ π¦)) β π£ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
70 | 69 | imbi2d 341 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π£ = (π’ β© π)) β§ π¦ β (π« π΄ β© Fin)) β ((π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£) β (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))) |
71 | 70 | ralbidva 3169 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π£ = (π’ β© π)) β (βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£) β βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))) |
72 | 71 | rexbidv 3172 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π£ = (π’ β© π)) β (βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£) β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))) |
73 | 37, 72 | imbi12d 345 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π£ = (π’ β© π)) β ((π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£)) β (π₯ β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
74 | 25, 32, 73 | ralxfr2d 5366 |
. . . . . 6
β’ ((π β§ π₯ β π) β (βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£)) β βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
75 | 22, 74 | bitr4d 282 |
. . . . 5
β’ ((π β§ π₯ β π) β (π₯ β (πΊ tsums πΉ) β βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£)))) |
76 | 75 | pm5.32da 580 |
. . . 4
β’ (π β ((π₯ β π β§ π₯ β (πΊ tsums πΉ)) β (π₯ β π β§ βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£))))) |
77 | 8, 76 | bitrid 283 |
. . 3
β’ (π β (π₯ β ((πΊ tsums πΉ) β© π) β (π₯ β π β§ βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£))))) |
78 | | eqid 2733 |
. . . 4
β’
(TopOpenβπ») =
(TopOpenβπ») |
79 | | resstps 22554 |
. . . . . 6
β’ ((πΊ β TopSp β§ π β (SubMndβπΊ)) β (πΊ βΎs π) β TopSp) |
80 | 16, 1, 79 | syl2anc 585 |
. . . . 5
β’ (π β (πΊ βΎs π) β TopSp) |
81 | 2, 80 | eqeltrid 2838 |
. . . 4
β’ (π β π» β TopSp) |
82 | 4 | feq3d 6656 |
. . . . 5
β’ (π β (πΉ:π΄βΆπ β πΉ:π΄βΆ(Baseβπ»))) |
83 | 18, 82 | mpbid 231 |
. . . 4
β’ (π β πΉ:π΄βΆ(Baseβπ»)) |
84 | 39, 78, 14, 44, 81, 17, 83 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (π» tsums πΉ) β (π₯ β (Baseβπ») β§ βπ£ β (TopOpenβπ»)(π₯ β π£ β βπ§ β (π« π΄ β© Fin)βπ¦ β (π« π΄ β© Fin)(π§ β π¦ β (π» Ξ£g (πΉ βΎ π¦)) β π£))))) |
85 | 6, 77, 84 | 3bitr4rd 312 |
. 2
β’ (π β (π₯ β (π» tsums πΉ) β π₯ β ((πΊ tsums πΉ) β© π))) |
86 | 85 | eqrdv 2731 |
1
β’ (π β (π» tsums πΉ) = ((πΊ tsums πΉ) β© π)) |