Step | Hyp | Ref
| Expression |
1 | | plycj.4 |
. . . 4
β’ (π β πΉ β (Polyβπ)) |
2 | | plycj.1 |
. . . . 5
β’ π = (degβπΉ) |
3 | | plycj.2 |
. . . . 5
β’ πΊ = ((β β πΉ) β
β) |
4 | | eqid 2733 |
. . . . 5
β’
(coeffβπΉ) =
(coeffβπΉ) |
5 | 2, 3, 4 | plycjlem 25790 |
. . . 4
β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β (coeffβπΉ))βπ) Β· (π§βπ)))) |
6 | 1, 5 | syl 17 |
. . 3
β’ (π β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β (coeffβπΉ))βπ) Β· (π§βπ)))) |
7 | | plybss 25708 |
. . . . . 6
β’ (πΉ β (Polyβπ) β π β β) |
8 | 1, 7 | syl 17 |
. . . . 5
β’ (π β π β β) |
9 | | 0cnd 11207 |
. . . . . 6
β’ (π β 0 β
β) |
10 | 9 | snssd 4813 |
. . . . 5
β’ (π β {0} β
β) |
11 | 8, 10 | unssd 4187 |
. . . 4
β’ (π β (π βͺ {0}) β
β) |
12 | | dgrcl 25747 |
. . . . . 6
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
13 | 1, 12 | syl 17 |
. . . . 5
β’ (π β (degβπΉ) β
β0) |
14 | 2, 13 | eqeltrid 2838 |
. . . 4
β’ (π β π β
β0) |
15 | 4 | coef 25744 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆ(π βͺ {0})) |
16 | 1, 15 | syl 17 |
. . . . . 6
β’ (π β (coeffβπΉ):β0βΆ(π βͺ {0})) |
17 | | elfznn0 13594 |
. . . . . 6
β’ (π β (0...π) β π β β0) |
18 | | fvco3 6991 |
. . . . . 6
β’
(((coeffβπΉ):β0βΆ(π βͺ {0}) β§ π β β0)
β ((β β (coeffβπΉ))βπ) = (ββ((coeffβπΉ)βπ))) |
19 | 16, 17, 18 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (0...π)) β ((β β
(coeffβπΉ))βπ) = (ββ((coeffβπΉ)βπ))) |
20 | | ffvelcdm 7084 |
. . . . . . 7
β’
(((coeffβπΉ):β0βΆ(π βͺ {0}) β§ π β β0)
β ((coeffβπΉ)βπ) β (π βͺ {0})) |
21 | 16, 17, 20 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((coeffβπΉ)βπ) β (π βͺ {0})) |
22 | | plycj.3 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (ββπ₯) β π) |
23 | 22 | ralrimiva 3147 |
. . . . . . . . . 10
β’ (π β βπ₯ β π (ββπ₯) β π) |
24 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π₯ = ((coeffβπΉ)βπ) β (ββπ₯) = (ββ((coeffβπΉ)βπ))) |
25 | 24 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ = ((coeffβπΉ)βπ) β ((ββπ₯) β π β (ββ((coeffβπΉ)βπ)) β π)) |
26 | 25 | rspccv 3610 |
. . . . . . . . . 10
β’
(βπ₯ β
π (ββπ₯) β π β (((coeffβπΉ)βπ) β π β (ββ((coeffβπΉ)βπ)) β π)) |
27 | 23, 26 | syl 17 |
. . . . . . . . 9
β’ (π β (((coeffβπΉ)βπ) β π β (ββ((coeffβπΉ)βπ)) β π)) |
28 | | elsni 4646 |
. . . . . . . . . . . . 13
β’
(((coeffβπΉ)βπ) β {0} β ((coeffβπΉ)βπ) = 0) |
29 | 28 | fveq2d 6896 |
. . . . . . . . . . . 12
β’
(((coeffβπΉ)βπ) β {0} β
(ββ((coeffβπΉ)βπ)) = (ββ0)) |
30 | | cj0 15105 |
. . . . . . . . . . . 12
β’
(ββ0) = 0 |
31 | 29, 30 | eqtrdi 2789 |
. . . . . . . . . . 11
β’
(((coeffβπΉ)βπ) β {0} β
(ββ((coeffβπΉ)βπ)) = 0) |
32 | | fvex 6905 |
. . . . . . . . . . . 12
β’
(ββ((coeffβπΉ)βπ)) β V |
33 | 32 | elsn 4644 |
. . . . . . . . . . 11
β’
((ββ((coeffβπΉ)βπ)) β {0} β
(ββ((coeffβπΉ)βπ)) = 0) |
34 | 31, 33 | sylibr 233 |
. . . . . . . . . 10
β’
(((coeffβπΉ)βπ) β {0} β
(ββ((coeffβπΉ)βπ)) β {0}) |
35 | 34 | a1i 11 |
. . . . . . . . 9
β’ (π β (((coeffβπΉ)βπ) β {0} β
(ββ((coeffβπΉ)βπ)) β {0})) |
36 | 27, 35 | orim12d 964 |
. . . . . . . 8
β’ (π β ((((coeffβπΉ)βπ) β π β¨ ((coeffβπΉ)βπ) β {0}) β
((ββ((coeffβπΉ)βπ)) β π β¨ (ββ((coeffβπΉ)βπ)) β {0}))) |
37 | | elun 4149 |
. . . . . . . 8
β’
(((coeffβπΉ)βπ) β (π βͺ {0}) β (((coeffβπΉ)βπ) β π β¨ ((coeffβπΉ)βπ) β {0})) |
38 | | elun 4149 |
. . . . . . . 8
β’
((ββ((coeffβπΉ)βπ)) β (π βͺ {0}) β
((ββ((coeffβπΉ)βπ)) β π β¨ (ββ((coeffβπΉ)βπ)) β {0})) |
39 | 36, 37, 38 | 3imtr4g 296 |
. . . . . . 7
β’ (π β (((coeffβπΉ)βπ) β (π βͺ {0}) β
(ββ((coeffβπΉ)βπ)) β (π βͺ {0}))) |
40 | 39 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (((coeffβπΉ)βπ) β (π βͺ {0}) β
(ββ((coeffβπΉ)βπ)) β (π βͺ {0}))) |
41 | 21, 40 | mpd 15 |
. . . . 5
β’ ((π β§ π β (0...π)) β
(ββ((coeffβπΉ)βπ)) β (π βͺ {0})) |
42 | 19, 41 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β (0...π)) β ((β β
(coeffβπΉ))βπ) β (π βͺ {0})) |
43 | 11, 14, 42 | elplyd 25716 |
. . 3
β’ (π β (π§ β β β¦ Ξ£π β (0...π)(((β β (coeffβπΉ))βπ) Β· (π§βπ))) β (Polyβ(π βͺ {0}))) |
44 | 6, 43 | eqeltrd 2834 |
. 2
β’ (π β πΊ β (Polyβ(π βͺ {0}))) |
45 | | plyun0 25711 |
. 2
β’
(Polyβ(π βͺ
{0})) = (Polyβπ) |
46 | 44, 45 | eleqtrdi 2844 |
1
β’ (π β πΊ β (Polyβπ)) |