Step | Hyp | Ref
| Expression |
1 | | plycj.2 |
. . 3
β’ πΊ = ((β β πΉ) β
β) |
2 | | cjcl 15057 |
. . . . 5
β’ (π§ β β β
(ββπ§) β
β) |
3 | 2 | adantl 481 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β (ββπ§) β
β) |
4 | | cjf 15056 |
. . . . . 6
β’
β:ββΆβ |
5 | 4 | a1i 11 |
. . . . 5
β’ (πΉ β (Polyβπ) β
β:ββΆβ) |
6 | 5 | feqmptd 6960 |
. . . 4
β’ (πΉ β (Polyβπ) β β = (π§ β β β¦
(ββπ§))) |
7 | | fzfid 13943 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β (0...π) β Fin) |
8 | | plycjlem.3 |
. . . . . . . . . 10
β’ π΄ = (coeffβπΉ) |
9 | 8 | coef3 25982 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
10 | 9 | adantr 480 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β π΄:β0βΆβ) |
11 | | elfznn0 13599 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
12 | | ffvelcdm 7083 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
13 | 10, 11, 12 | syl2an 595 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β (π΄βπ) β β) |
14 | | expcl 14050 |
. . . . . . . . 9
β’ ((π₯ β β β§ π β β0)
β (π₯βπ) β
β) |
15 | 11, 14 | sylan2 592 |
. . . . . . . 8
β’ ((π₯ β β β§ π β (0...π)) β (π₯βπ) β β) |
16 | 15 | adantll 711 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β (π₯βπ) β β) |
17 | 13, 16 | mulcld 11239 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π₯ β β) β§ π β (0...π)) β ((π΄βπ) Β· (π₯βπ)) β β) |
18 | 7, 17 | fsumcl 15684 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) β β) |
19 | | plycj.1 |
. . . . . 6
β’ π = (degβπΉ) |
20 | 8, 19 | coeid 25988 |
. . . . 5
β’ (πΉ β (Polyβπ) β πΉ = (π₯ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)))) |
21 | | fveq2 6891 |
. . . . 5
β’ (π§ = Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) β (ββπ§) = (ββΞ£π β (0...π)((π΄βπ) Β· (π₯βπ)))) |
22 | 18, 20, 6, 21 | fmptco 7129 |
. . . 4
β’ (πΉ β (Polyβπ) β (β β πΉ) = (π₯ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· (π₯βπ))))) |
23 | | oveq1 7419 |
. . . . . . 7
β’ (π₯ = (ββπ§) β (π₯βπ) = ((ββπ§)βπ)) |
24 | 23 | oveq2d 7428 |
. . . . . 6
β’ (π₯ = (ββπ§) β ((π΄βπ) Β· (π₯βπ)) = ((π΄βπ) Β· ((ββπ§)βπ))) |
25 | 24 | sumeq2sdv 15655 |
. . . . 5
β’ (π₯ = (ββπ§) β Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) = Ξ£π β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) |
26 | 25 | fveq2d 6895 |
. . . 4
β’ (π₯ = (ββπ§) β
(ββΞ£π
β (0...π)((π΄βπ) Β· (π₯βπ))) = (ββΞ£π β (0...π)((π΄βπ) Β· ((ββπ§)βπ)))) |
27 | 3, 6, 22, 26 | fmptco 7129 |
. . 3
β’ (πΉ β (Polyβπ) β ((β β
πΉ) β β) =
(π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))))) |
28 | 1, 27 | eqtrid 2783 |
. 2
β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))))) |
29 | | fzfid 13943 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π§ β β) β (0...π) β Fin) |
30 | 9 | adantr 480 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ π§ β β) β π΄:β0βΆβ) |
31 | 30, 11, 12 | syl2an 595 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (π΄βπ) β β) |
32 | | expcl 14050 |
. . . . . . 7
β’
(((ββπ§)
β β β§ π
β β0) β ((ββπ§)βπ) β β) |
33 | 3, 11, 32 | syl2an 595 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((ββπ§)βπ) β β) |
34 | 31, 33 | mulcld 11239 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((π΄βπ) Β· ((ββπ§)βπ)) β β) |
35 | 29, 34 | fsumcj 15761 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(ββ((π΄βπ) Β· ((ββπ§)βπ)))) |
36 | 31, 33 | cjmuld 15173 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (ββ((π΄βπ) Β· ((ββπ§)βπ))) = ((ββ(π΄βπ)) Β·
(ββ((ββπ§)βπ)))) |
37 | | fvco3 6990 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β ((β β π΄)βπ) = (ββ(π΄βπ))) |
38 | 30, 11, 37 | syl2an 595 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β ((β β π΄)βπ) = (ββ(π΄βπ))) |
39 | | cjexp 15102 |
. . . . . . . . 9
β’
(((ββπ§)
β β β§ π
β β0) β (ββ((ββπ§)βπ)) = ((ββ(ββπ§))βπ)) |
40 | 3, 11, 39 | syl2an 595 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
(ββ((ββπ§)βπ)) = ((ββ(ββπ§))βπ)) |
41 | | cjcj 15092 |
. . . . . . . . . 10
β’ (π§ β β β
(ββ(ββπ§)) = π§) |
42 | 41 | ad2antlr 724 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
(ββ(ββπ§)) = π§) |
43 | 42 | oveq1d 7427 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β
((ββ(ββπ§))βπ) = (π§βπ)) |
44 | 40, 43 | eqtr2d 2772 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (π§βπ) = (ββ((ββπ§)βπ))) |
45 | 38, 44 | oveq12d 7430 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (((β β π΄)βπ) Β· (π§βπ)) = ((ββ(π΄βπ)) Β·
(ββ((ββπ§)βπ)))) |
46 | 36, 45 | eqtr4d 2774 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π§ β β) β§ π β (0...π)) β (ββ((π΄βπ) Β· ((ββπ§)βπ))) = (((β β π΄)βπ) Β· (π§βπ))) |
47 | 46 | sumeq2dv 15654 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π§ β β) β Ξ£π β (0...π)(ββ((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ))) |
48 | 35, 47 | eqtrd 2771 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π§ β β) β
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ))) = Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ))) |
49 | 48 | mpteq2dva 5248 |
. 2
β’ (πΉ β (Polyβπ) β (π§ β β β¦
(ββΞ£π
β (0...π)((π΄βπ) Β· ((ββπ§)βπ)))) = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) |
50 | 28, 49 | eqtrd 2771 |
1
β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) |