Step | Hyp | Ref
| Expression |
1 | | fzfid 13941 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (0...(degβπΉ))
β Fin) |
2 | | 0re 11217 |
. . . . . . . . 9
β’ 0 β
β |
3 | | eqid 2726 |
. . . . . . . . . 10
β’
(coeffβπΉ) =
(coeffβπΉ) |
4 | 3 | coef2 26115 |
. . . . . . . . 9
β’ ((πΉ β (Polyββ)
β§ 0 β β) β (coeffβπΉ):β0βΆβ) |
5 | 2, 4 | mpan2 688 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β (coeffβπΉ):β0βΆβ) |
6 | 5 | adantr 480 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (coeffβπΉ):β0βΆβ) |
7 | | elfznn0 13597 |
. . . . . . 7
β’ (π₯ β (0...(degβπΉ)) β π₯ β β0) |
8 | | ffvelcdm 7076 |
. . . . . . 7
β’
(((coeffβπΉ):β0βΆβ β§
π₯ β
β0) β ((coeffβπΉ)βπ₯) β β) |
9 | 6, 7, 8 | syl2an 595 |
. . . . . 6
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
((coeffβπΉ)βπ₯) β β) |
10 | 9 | recnd 11243 |
. . . . 5
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
((coeffβπΉ)βπ₯) β β) |
11 | | simpr 484 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β π΄ β
β) |
12 | | expcl 14047 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β0)
β (π΄βπ₯) β
β) |
13 | 11, 7, 12 | syl2an 595 |
. . . . 5
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(π΄βπ₯) β β) |
14 | 10, 13 | mulcld 11235 |
. . . 4
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(((coeffβπΉ)βπ₯) Β· (π΄βπ₯)) β β) |
15 | 1, 14 | fsumcj 15759 |
. . 3
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (ββΞ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) = Ξ£π₯ β (0...(degβπΉ))(ββ(((coeffβπΉ)βπ₯) Β· (π΄βπ₯)))) |
16 | 10, 13 | cjmuld 15171 |
. . . . 5
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(ββ(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) = ((ββ((coeffβπΉ)βπ₯)) Β· (ββ(π΄βπ₯)))) |
17 | 9 | cjred 15176 |
. . . . . 6
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(ββ((coeffβπΉ)βπ₯)) = ((coeffβπΉ)βπ₯)) |
18 | | cjexp 15100 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β0)
β (ββ(π΄βπ₯)) = ((ββπ΄)βπ₯)) |
19 | 11, 7, 18 | syl2an 595 |
. . . . . 6
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(ββ(π΄βπ₯)) = ((ββπ΄)βπ₯)) |
20 | 17, 19 | oveq12d 7422 |
. . . . 5
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
((ββ((coeffβπΉ)βπ₯)) Β· (ββ(π΄βπ₯))) = (((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
21 | 16, 20 | eqtrd 2766 |
. . . 4
β’ (((πΉ β (Polyββ)
β§ π΄ β β)
β§ π₯ β
(0...(degβπΉ))) β
(ββ(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) = (((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
22 | 21 | sumeq2dv 15652 |
. . 3
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β Ξ£π₯ β
(0...(degβπΉ))(ββ(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) = Ξ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
23 | 15, 22 | eqtrd 2766 |
. 2
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (ββΞ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) = Ξ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
24 | | eqid 2726 |
. . . 4
β’
(degβπΉ) =
(degβπΉ) |
25 | 3, 24 | coeid2 26123 |
. . 3
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (πΉβπ΄) = Ξ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· (π΄βπ₯))) |
26 | 25 | fveq2d 6888 |
. 2
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (ββ(πΉβπ΄)) = (ββΞ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· (π΄βπ₯)))) |
27 | | cjcl 15055 |
. . 3
β’ (π΄ β β β
(ββπ΄) β
β) |
28 | 3, 24 | coeid2 26123 |
. . 3
β’ ((πΉ β (Polyββ)
β§ (ββπ΄)
β β) β (πΉβ(ββπ΄)) = Ξ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
29 | 27, 28 | sylan2 592 |
. 2
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (πΉβ(ββπ΄)) = Ξ£π₯ β (0...(degβπΉ))(((coeffβπΉ)βπ₯) Β· ((ββπ΄)βπ₯))) |
30 | 23, 26, 29 | 3eqtr4d 2776 |
1
β’ ((πΉ β (Polyββ)
β§ π΄ β β)
β (ββ(πΉβπ΄)) = (πΉβ(ββπ΄))) |