Step | Hyp | Ref
| Expression |
1 | | tsmsid.2 |
. . . . . . 7
β’ (π β πΊ β TopSp) |
2 | | tsmsid.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
3 | | tsmsgsum.j |
. . . . . . . 8
β’ π½ = (TopOpenβπΊ) |
4 | 2, 3 | istps 22427 |
. . . . . . 7
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
5 | 1, 4 | sylib 217 |
. . . . . 6
β’ (π β π½ β (TopOnβπ΅)) |
6 | | toponuni 22407 |
. . . . . 6
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β π΅ = βͺ π½) |
8 | 7 | eleq2d 2819 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β βͺ π½)) |
9 | | elfpw 9350 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π« π΄ β© Fin) β (π¦ β π΄ β§ π¦ β Fin)) |
10 | 9 | simplbi 498 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π΄ β© Fin) β π¦ β π΄) |
11 | 10 | adantl 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π¦ β π΄) |
12 | | suppssdm 8158 |
. . . . . . . . . . . . . . 15
β’ (πΉ supp 0 ) β dom πΉ |
13 | | tsmsid.f |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆπ΅) |
14 | 12, 13 | fssdm 6734 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ supp 0 ) β π΄) |
15 | 14 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β π΄) |
16 | 11, 15 | unssd 4185 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β π΄) |
17 | | elinel2 4195 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π΄ β© Fin) β π¦ β Fin) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π¦ β Fin) |
19 | | tsmsid.w |
. . . . . . . . . . . . . . 15
β’ (π β πΉ finSupp 0 ) |
20 | 19 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΉ finSupp 0 ) |
21 | 20 | fsuppimpd 9365 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β
Fin) |
22 | | unfi 9168 |
. . . . . . . . . . . . 13
β’ ((π¦ β Fin β§ (πΉ supp 0 ) β Fin) β
(π¦ βͺ (πΉ supp 0 )) β
Fin) |
23 | 18, 21, 22 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β
Fin) |
24 | | elfpw 9350 |
. . . . . . . . . . . 12
β’ ((π¦ βͺ (πΉ supp 0 )) β (π« π΄ β© Fin) β ((π¦ βͺ (πΉ supp 0 )) β π΄ β§ (π¦ βͺ (πΉ supp 0 )) β
Fin)) |
25 | 16, 23, 24 | sylanbrc 583 |
. . . . . . . . . . 11
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (π¦ βͺ (πΉ supp 0 )) β (π« π΄ β© Fin)) |
26 | | ssun1 4171 |
. . . . . . . . . . . . . . 15
β’ π¦ β (π¦ βͺ (πΉ supp 0 )) |
27 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β π§ = (π¦ βͺ (πΉ supp 0 ))) |
28 | 26, 27 | sseqtrrid 4034 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β π¦ β π§) |
29 | | pm5.5 361 |
. . . . . . . . . . . . . 14
β’ (π¦ β π§ β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
31 | | reseq2 5974 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β (πΉ βΎ π§) = (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) |
32 | 31 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β (πΊ Ξ£g
(πΉ βΎ π§)) = (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 ))))) |
33 | 32 | eleq1d 2818 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((πΊ Ξ£g
(πΉ βΎ π§)) β π’ β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
34 | 30, 33 | bitrd 278 |
. . . . . . . . . . . 12
β’ (π§ = (π¦ βͺ (πΉ supp 0 )) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’)) |
35 | 34 | rspcv 3608 |
. . . . . . . . . . 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 724 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΊ β CMnd) |
40 | | tsmsid.a |
. . . . . . . . . . . . 13
β’ (π β π΄ β π) |
41 | 40 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β π΄ β π) |
42 | 13 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β πΉ:π΄βΆπ΅) |
43 | | ssun2 4172 |
. . . . . . . . . . . . 13
β’ (πΉ supp 0 ) β (π¦ βͺ (πΉ supp 0 )) |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β (π¦ βͺ (πΉ supp 0 ))) |
45 | 2, 37, 39, 41, 42, 44, 20 | gsumres 19775 |
. . . . . . . . . . 11
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) = (πΊ Ξ£g πΉ)) |
46 | 45 | eleq1d 2818 |
. . . . . . . . . 10
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ (πΉ supp 0 )))) β π’ β (πΊ Ξ£g πΉ) β π’)) |
47 | 36, 46 | sylibd 238 |
. . . . . . . . 9
β’ (((π β§ π’ β π½) β§ π¦ β (π« π΄ β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
48 | 47 | rexlimdva 3155 |
. . . . . . . 8
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
49 | 19 | fsuppimpd 9365 |
. . . . . . . . . . 11
β’ (π β (πΉ supp 0 ) β
Fin) |
50 | | elfpw 9350 |
. . . . . . . . . . 11
β’ ((πΉ supp 0 ) β (π« π΄ β© Fin) β ((πΉ supp 0 ) β π΄ β§ (πΉ supp 0 ) β
Fin)) |
51 | 14, 49, 50 | sylanbrc 583 |
. . . . . . . . . 10
β’ (π β (πΉ supp 0 ) β (π« π΄ β© Fin)) |
52 | 38 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΊ β CMnd) |
53 | 40 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β π΄ β π) |
54 | 13 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΉ:π΄βΆπ΅) |
55 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΉ supp 0 ) β π§) |
56 | 19 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β πΉ finSupp 0 ) |
57 | 2, 37, 52, 53, 54, 55, 56 | gsumres 19775 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g (πΉ βΎ π§)) = (πΊ Ξ£g πΉ)) |
58 | | simplrr 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g πΉ) β π’) |
59 | 57, 58 | eqeltrd 2833 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ (π§ β (π« π΄ β© Fin) β§ (πΉ supp 0 ) β π§)) β (πΊ Ξ£g (πΉ βΎ π§)) β π’) |
60 | 59 | expr 457 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β§ π§ β (π« π΄ β© Fin)) β ((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
61 | 60 | ralrimiva 3146 |
. . . . . . . . . 10
β’ ((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β βπ§ β (π« π΄ β© Fin)((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
62 | | sseq1 4006 |
. . . . . . . . . . 11
β’ (π¦ = (πΉ supp 0 ) β (π¦ β π§ β (πΉ supp 0 ) β π§)) |
63 | 62 | rspceaimv 3616 |
. . . . . . . . . 10
β’ (((πΉ supp 0 ) β (π« π΄ β© Fin) β§ βπ§ β (π« π΄ β© Fin)((πΉ supp 0 ) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
64 | 51, 61, 63 | syl2an2r 683 |
. . . . . . . . 9
β’ ((π β§ (π’ β π½ β§ (πΊ Ξ£g πΉ) β π’)) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
65 | 64 | expr 457 |
. . . . . . . 8
β’ ((π β§ π’ β π½) β ((πΊ Ξ£g πΉ) β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
66 | 48, 65 | impbid 211 |
. . . . . . 7
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g πΉ) β π’)) |
67 | | disjsn 4714 |
. . . . . . . 8
β’ ((π’ β© {(πΊ Ξ£g πΉ)}) = β
β Β¬
(πΊ
Ξ£g πΉ) β π’) |
68 | 67 | necon2abii 2991 |
. . . . . . 7
β’ ((πΊ Ξ£g
πΉ) β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
) |
69 | 66, 68 | bitrdi 286 |
. . . . . 6
β’ ((π β§ π’ β π½) β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)) |
70 | 69 | imbi2d 340 |
. . . . 5
β’ ((π β§ π’ β π½) β ((π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
))) |
71 | 70 | ralbidva 3175 |
. . . 4
β’ (π β (βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
))) |
72 | 8, 71 | anbi12d 631 |
. . 3
β’ (π β ((π₯ β π΅ β§ βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
73 | | eqid 2732 |
. . . 4
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
74 | 2, 3, 73, 38, 1, 40, 13 | eltsms 23628 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β (π₯ β π΅ β§ βπ’ β π½ (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))))) |
75 | | topontop 22406 |
. . . . 5
β’ (π½ β (TopOnβπ΅) β π½ β Top) |
76 | 5, 75 | syl 17 |
. . . 4
β’ (π β π½ β Top) |
77 | 2, 37, 38, 40, 13, 19 | gsumcl 19777 |
. . . . . 6
β’ (π β (πΊ Ξ£g πΉ) β π΅) |
78 | 77 | snssd 4811 |
. . . . 5
β’ (π β {(πΊ Ξ£g πΉ)} β π΅) |
79 | 78, 7 | sseqtrd 4021 |
. . . 4
β’ (π β {(πΊ Ξ£g πΉ)} β βͺ π½) |
80 | | eqid 2732 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
81 | 80 | elcls2 22569 |
. . . 4
β’ ((π½ β Top β§ {(πΊ Ξ£g
πΉ)} β βͺ π½)
β (π₯ β
((clsβπ½)β{(πΊ Ξ£g πΉ)}) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
82 | 76, 79, 81 | syl2anc 584 |
. . 3
β’ (π β (π₯ β ((clsβπ½)β{(πΊ Ξ£g πΉ)}) β (π₯ β βͺ π½ β§ βπ’ β π½ (π₯ β π’ β (π’ β© {(πΊ Ξ£g πΉ)}) β
β
)))) |
83 | 72, 74, 82 | 3bitr4d 310 |
. 2
β’ (π β (π₯ β (πΊ tsums πΉ) β π₯ β ((clsβπ½)β{(πΊ Ξ£g πΉ)}))) |
84 | 83 | eqrdv 2730 |
1
β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{(πΊ Ξ£g πΉ)})) |