Step | Hyp | Ref
| Expression |
1 | | elply 25709 |
. . 3
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
2 | 1 | simprbi 498 |
. 2
β’ (πΉ β (Polyβπ) β βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
3 | | fzfid 13938 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β (0...π) β Fin) |
4 | | plybss 25708 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β π β β) |
5 | | 0cnd 11207 |
. . . . . . . . . . . 12
β’ (πΉ β (Polyβπ) β 0 β
β) |
6 | 5 | snssd 4813 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β {0} β
β) |
7 | 4, 6 | unssd 4187 |
. . . . . . . . . 10
β’ (πΉ β (Polyβπ) β (π βͺ {0}) β
β) |
8 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β (π βͺ {0}) β
β) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β (π βͺ {0}) β
β) |
10 | | simplrr 777 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β π β ((π βͺ {0}) βm
β0)) |
11 | | cnex 11191 |
. . . . . . . . . . . 12
β’ β
β V |
12 | | ssexg 5324 |
. . . . . . . . . . . 12
β’ (((π βͺ {0}) β β
β§ β β V) β (π βͺ {0}) β V) |
13 | 8, 11, 12 | sylancl 587 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β (π βͺ {0}) β V) |
14 | | nn0ex 12478 |
. . . . . . . . . . 11
β’
β0 β V |
15 | | elmapg 8833 |
. . . . . . . . . . 11
β’ (((π βͺ {0}) β V β§
β0 β V) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
16 | 13, 14, 15 | sylancl 587 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
17 | 10, 16 | mpbid 231 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β π:β0βΆ(π βͺ {0})) |
18 | | elfznn0 13594 |
. . . . . . . . 9
β’ (π β (0...π) β π β β0) |
19 | | ffvelcdm 7084 |
. . . . . . . . 9
β’ ((π:β0βΆ(π βͺ {0}) β§ π β β0)
β (πβπ) β (π βͺ {0})) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . . . 8
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β (πβπ) β (π βͺ {0})) |
21 | 9, 20 | sseldd 3984 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β (πβπ) β β) |
22 | | simpr 486 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β π§ β β) |
23 | | expcl 14045 |
. . . . . . . 8
β’ ((π§ β β β§ π β β0)
β (π§βπ) β
β) |
24 | 22, 18, 23 | syl2an 597 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β (π§βπ) β β) |
25 | 21, 24 | mulcld 11234 |
. . . . . 6
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β ((πβπ) Β· (π§βπ)) β β) |
26 | 3, 25 | fsumcl 15679 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β Ξ£π β (0...π)((πβπ) Β· (π§βπ)) β β) |
27 | 26 | fmpttd 7115 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))):ββΆβ) |
28 | | feq1 6699 |
. . . 4
β’ (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (πΉ:ββΆβ β (π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))):ββΆβ)) |
29 | 27, 28 | syl5ibrcom 246 |
. . 3
β’ ((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β πΉ:ββΆβ)) |
30 | 29 | rexlimdvva 3212 |
. 2
β’ (πΉ β (Polyβπ) β (βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β πΉ:ββΆβ)) |
31 | 2, 30 | mpd 15 |
1
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |