Step | Hyp | Ref
| Expression |
1 | | plycj.2 |
. . 3
β’ πΊ = ((β β πΉ) β
β) |
2 | | cjcl 15052 |
. . . . 5
β’ (π§ β β β
(ββπ§) β
β) |
3 | 2 | adantl 483 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β (ββπ§) β
β) |
4 | | cjf 15051 |
. . . . . 6
β’
β:ββΆβ |
5 | 4 | a1i 11 |
. . . . 5
β’ (πΉ β (Polyβπ) β
β:ββΆβ) |
6 | 5 | feqmptd 6961 |
. . . 4
β’ (πΉ β (Polyβπ) β β = (π§ β β β¦
(ββπ§))) |
7 | | fzfid 13938 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β (0...π) β Fin) |
8 | | plycjlem.3 |
. . . . . . . . . 10
β’ π΄ = (coeffβπΉ) |
9 | 8 | coef3 25746 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β π΄:β0βΆβ) |
11 | | elfznn0 13594 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
12 | | ffvelcdm 7084 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
13 | 10, 11, 12 | syl2an 597 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β (π΄βπ) β β) |
14 | | expcl 14045 |
. . . . . . . . 9
β’ ((π₯ β β β§ π β β0)
β (π₯βπ) β
β) |
15 | 11, 14 | sylan2 594 |
. . . . . . . 8
β’ ((π₯ β β β§ π β (0...π)) β (π₯βπ) β β) |
16 | 15 | adantll 713 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β (π₯βπ) β β) |
17 | 13, 16 | mulcld 11234 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β ((π΄βπ) Β· (π₯βπ)) β β) |
18 | 7, 17 | fsumcl 15679 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) β β) |
19 | | plycj.1 |
. . . . . 6
β’ π = (degβπΉ) |
20 | 8, 19 | coeid 25752 |
. . . . 5
β’ (πΉ β (Polyβπ) β πΉ = (π₯ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)))) |
21 | | fveq2 6892 |
. . . . 5
β’ (π§ = Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) β (ββπ§) = (ββΞ£π β (0...π)((π΄βπ) Β· (π₯βπ)))) |
22 | 18, 20, 6, 21 | fmptco 7127 |
. . . 4
β’ (πΉ β (Polyβπ) β (β β πΉ) = (π₯ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· (π₯βπ))))) |
23 | | oveq1 7416 |
. . . . . . 7
β’ (π₯ = (ββπ§) β (π₯βπ) = ((ββπ§)βπ)) |
24 | 23 | oveq2d 7425 |
. . . . . 6
β’ (π₯ = (ββπ§) β ((π΄βπ) Β· (π₯βπ)) = ((π΄βπ) Β· ((ββπ§)βπ))) |
25 | 24 | sumeq2sdv 15650 |
. . . . 5
β’ (π₯ = (ββπ§) β Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) = Ξ£π β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) |
26 | 25 | fveq2d 6896 |
. . . 4
β’ (π₯ = (ββπ§) β
(ββΞ£π
β (0...π)((π΄βπ) Β· (π₯βπ))) = (ββΞ£π β (0...π)((π΄βπ) Β· ((ββπ§)βπ)))) |
27 | 3, 6, 22, 26 | fmptco 7127 |
. . 3
β’ (πΉ β (Polyβπ) β ((β β
πΉ) β β) =
(π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))))) |
28 | 1, 27 | eqtrid 2785 |
. 2
β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))))) |
29 | | fzfid 13938 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π§ β β) β (0...π) β Fin) |
30 | 9 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ π§ β β) β π΄:β0βΆβ) |
31 | 30, 11, 12 | syl2an 597 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (π΄βπ) β β) |
32 | | expcl 14045 |
. . . . . . 7
β’
(((ββπ§)
β β β§ π
β β0) β ((ββπ§)βπ) β β) |
33 | 3, 11, 32 | syl2an 597 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((ββπ§)βπ) β β) |
34 | 31, 33 | mulcld 11234 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((π΄βπ) Β· ((ββπ§)βπ)) β β) |
35 | 29, 34 | fsumcj 15756 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(ββ((π΄βπ) Β· ((ββπ§)βπ)))) |
36 | 31, 33 | cjmuld 15168 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (ββ((π΄βπ) Β· ((ββπ§)βπ))) = ((ββ(π΄βπ)) Β·
(ββ((ββπ§)βπ)))) |
37 | | fvco3 6991 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β ((β β π΄)βπ) = (ββ(π΄βπ))) |
38 | 30, 11, 37 | syl2an 597 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((β β π΄)βπ) = (ββ(π΄βπ))) |
39 | | cjexp 15097 |
. . . . . . . . 9
β’
(((ββπ§)
β β β§ π
β β0) β (ββ((ββπ§)βπ)) = ((ββ(ββπ§))βπ)) |
40 | 3, 11, 39 | syl2an 597 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
(ββ((ββπ§)βπ)) = ((ββ(ββπ§))βπ)) |
41 | | cjcj 15087 |
. . . . . . . . . 10
β’ (π§ β β β
(ββ(ββπ§)) = π§) |
42 | 41 | ad2antlr 726 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
(ββ(ββπ§)) = π§) |
43 | 42 | oveq1d 7424 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
((ββ(ββπ§))βπ) = (π§βπ)) |
44 | 40, 43 | eqtr2d 2774 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (π§βπ) = (ββ((ββπ§)βπ))) |
45 | 38, 44 | oveq12d 7427 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (((β β π΄)βπ) Β· (π§βπ)) = ((ββ(π΄βπ)) Β·
(ββ((ββπ§)βπ)))) |
46 | 36, 45 | eqtr4d 2776 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (ββ((π΄βπ) Β· ((ββπ§)βπ))) = (((β β π΄)βπ) Β· (π§βπ))) |
47 | 46 | sumeq2dv 15649 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β Ξ£π β (0...π)(ββ((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ))) |
48 | 35, 47 | eqtrd 2773 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π§ β β) β
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ))) |
49 | 48 | mpteq2dva 5249 |
. 2
β’ (πΉ β (Polyβπ) β (π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ)))) = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) |
50 | 28, 49 | eqtrd 2773 |
1
β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) |