Step | Hyp | Ref
| Expression |
1 | | tsmsid.2 |
. . . . . . 7
β’ (π β πΊ β TopSp) |
2 | | tsmsid.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
3 | | tsmsgsum.j |
. . . . . . . 8
β’ π½ = (TopOpenβπΊ) |
4 | 2, 3 | istps 22299 |
. . . . . . 7
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
5 | 1, 4 | sylib 217 |
. . . . . 6
β’ (π β π½ β (TopOnβπ΅)) |
6 | | toponuni 22279 |
. . . . . 6
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β π΅ = βͺ π½) |
8 | 7 | eleq2d 2820 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β βͺ π½)) |
9 | | elfpw 9301 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π« π΄ β© Fin) β (π¦ β π΄ β§ π¦ β Fin)) |
10 | 9 | simplbi 499 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π΄ β© Fin) β π¦ β π΄) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π¦ β π΄) |
12 | | suppssdm 8109 |
. . . . . . . . . . . . . . 15
β’ (πΉ supp 0 ) β dom πΉ |
13 | | tsmsid.f |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆπ΅) |
14 | 12, 13 | fssdm 6689 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ supp 0 ) β π΄) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β π΄) |
16 | 11, 15 | unssd 4147 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β π΄) |
17 | | elinel2 4157 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π΄ β© Fin) β π¦ β Fin) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π¦ β Fin) |
19 | | tsmsid.w |
. . . . . . . . . . . . . . 15
β’ (π β πΉ finSupp 0 ) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΉ finSupp 0 ) |
21 | 20 | fsuppimpd 9316 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β
Fin) |
22 | | unfi 9119 |
. . . . . . . . . . . . 13
β’ ((π¦ β Fin β§ (πΉ supp 0 ) β Fin) β
(π¦ βͺ (πΉ supp 0 )) β
Fin) |
23 | 18, 21, 22 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β
Fin) |
24 | | elfpw 9301 |
. . . . . . . . . . . 12
β’ ((π¦ βͺ (πΉ supp 0 )) β (π« π΄ β© Fin) β ((π¦ βͺ (πΉ supp 0 )) β π΄ β§ (π¦ βͺ (πΉ supp 0 )) β
Fin)) |
25 | 16, 23, 24 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β (π« π΄ β© Fin)) |
26 | | ssun1 4133 |
. . . . . . . . . . . . . . 15
β’ π¦ β (π¦ βͺ (πΉ supp 0 )) |
27 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β π§ = (π¦ βͺ (πΉ supp 0 ))) |
28 | 26, 27 | sseqtrrid 3998 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β π¦ β π§) |
29 | | pm5.5 362 |
. . . . . . . . . . . . . 14
β’ (π¦ β π§ β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
31 | | reseq2 5933 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β (πΉ βΎ π§) = (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) |
32 | 31 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β (πΊ Ξ£g
(πΉ βΎ π§)) = (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 ))))) |
33 | 32 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((πΊ Ξ£g
(πΉ βΎ π§)) β π’ β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
34 | 30, 33 | bitrd 279 |
. . . . . . . . . . . 12
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
35 | 34 | rspcv 3576 |
. . . . . . . . . . 11
β’ ((π¦ βͺ (πΉ supp 0 )) β (π« π΄ β© Fin) β
(βπ§ β
(π« π΄ β©
Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
36 | 25, 35 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
37 | | tsmsid.z |
. . . . . . . . . . . 12
β’ 0 =
(0gβπΊ) |
38 | | tsmsid.1 |
. . . . . . . . . . . . 13
β’ (π β πΊ β CMnd) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΊ β CMnd) |
40 | | tsmsid.a |
. . . . . . . . . . . . 13
β’ (π β π΄ β π) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π΄ β π) |
42 | 13 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΉ:π΄βΆπ΅) |
43 | | ssun2 4134 |
. . . . . . . . . . . . 13
β’ (πΉ supp 0 ) β (π¦ βͺ (πΉ supp 0 )) |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β (π¦ βͺ (πΉ supp 0 ))) |
45 | 2, 37, 39, 41, 42, 44, 20 | gsumres 19695 |
. . . . . . . . . . 11
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) = (πΊ Ξ£g πΉ)) |
46 | 45 | eleq1d 2819 |
. . . . . . . . . 10
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’ β (πΊ Ξ£g πΉ) β π’)) |
47 | 36, 46 | sylibd 238 |
. . . . . . . . 9
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
48 | 47 | rexlimdva 3149 |
. . . . . . . 8
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
49 | 19 | fsuppimpd 9316 |
. . . . . . . . . . 11
β’ (π β (πΉ supp 0 ) β
Fin) |
50 | | elfpw 9301 |
. . . . . . . . . . 11
β’ ((πΉ supp 0 ) β (π« π΄ β© Fin) β ((πΉ supp 0 ) β π΄ β§ (πΉ supp 0 ) β
Fin)) |
51 | 14, 49, 50 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β (πΉ supp 0 ) β (π« π΄ β© Fin)) |
52 | 38 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΊ β CMnd) |
53 | 40 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β π΄ β π) |
54 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΉ:π΄βΆπ΅) |
55 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΉ supp 0 ) β π§) |
56 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΉ finSupp 0 ) |
57 | 2, 37, 52, 53, 54, 55, 56 | gsumres 19695 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g (πΉ βΎ π§)) = (πΊ Ξ£g πΉ)) |
58 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g πΉ) β π’) |
59 | 57, 58 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g (πΉ βΎ π§)) β π’) |
60 | 59 | expr 458 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ π§ β (π« π΄ β© Fin)) β ((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
61 | 60 | ralrimiva 3140 |
. . . . . . . . . 10
β’ ((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β βπ§ β (π« π΄ β© Fin)((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
62 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π¦ = (πΉ supp 0 ) β (π¦ β π§ β (πΉ supp 0 ) β π§)) |
63 | 62 | rspceaimv 3584 |
. . . . . . . . . 10
β’ (((πΉ supp 0 ) β (π« π΄ β© Fin) β§ βπ§ β (π« π΄ β© Fin)((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
64 | 51, 61, 63 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
65 | 64 | expr 458 |
. . . . . . . 8
β’ ((π β§ π’ β π½) β ((πΊ Ξ£g πΉ) β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
66 | 48, 65 | impbid 211 |
. . . . . . 7
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
67 | | disjsn 4673 |
. . . . . . . 8
β’ ((π’ β© {(πΊ Ξ£g πΉ)}) = β
β Β¬
(πΊ
Ξ£g πΉ) β π’) |
68 | 67 | necon2abii 2991 |
. . . . . . 7
β’ ((πΊ Ξ£g
πΉ) β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
) |
69 | 66, 68 | bitrdi 287 |
. . . . . 6
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)) |
70 | 69 | imbi2d 341 |
. . . . 5
β’ ((π β§ π’ β π½) β ((π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
))) |
71 | 70 | ralbidva 3169 |
. . . 4
β’ (π β (βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
))) |
72 | 8, 71 | anbi12d 632 |
. . 3
β’ (π β ((π₯ β π΅ β§ βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
73 | | eqid 2733 |
. . . 4
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
74 | 2, 3, 73, 38, 1, 40, 13 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β (π₯ β π΅ β§ βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))))) |
75 | | topontop 22278 |
. . . . 5
β’ (π½ β (TopOnβπ΅) β π½ β Top) |
76 | 5, 75 | syl 17 |
. . . 4
β’ (π β π½ β Top) |
77 | 2, 37, 38, 40, 13, 19 | gsumcl 19697 |
. . . . . 6
β’ (π β (πΊ Ξ£g πΉ) β π΅) |
78 | 77 | snssd 4770 |
. . . . 5
β’ (π β {(πΊ Ξ£g πΉ)} β π΅) |
79 | 78, 7 | sseqtrd 3985 |
. . . 4
β’ (π β {(πΊ Ξ£g πΉ)} β βͺ π½) |
80 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
81 | 80 | elcls2 22441 |
. . . 4
β’ ((π½ β Top β§ {(πΊ Ξ£g
πΉ)} β βͺ π½)
β (π₯ β
((clsβπ½)β{(πΊ Ξ£g πΉ)}) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
82 | 76, 79, 81 | syl2anc 585 |
. . 3
β’ (π β (π₯ β ((clsβπ½)β{(πΊ Ξ£g πΉ)}) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
83 | 72, 74, 82 | 3bitr4d 311 |
. 2
β’ (π β (π₯ β (πΊ tsums πΉ) β π₯ β ((clsβπ½)β{(πΊ Ξ£g πΉ)}))) |
84 | 83 | eqrdv 2731 |
1
β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{(πΊ Ξ£g πΉ)})) |