Step | Hyp | Ref
| Expression |
1 | | plyf 25712 |
. . . . . 6
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
2 | 1 | adantl 483 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ:ββΆβ) |
3 | 2 | feqmptd 6961 |
. . . 4
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ = (π β β β¦ (πΉβπ))) |
4 | | simplr 768 |
. . . . . 6
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β) β πΉ β (Polyβπ)) |
5 | | dgrcl 25747 |
. . . . . . . . . 10
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
6 | 5 | adantl 483 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (degβπΉ) β
β0) |
7 | 6 | nn0zd 12584 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (degβπΉ) β β€) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β) β (degβπΉ) β
β€) |
9 | | uzid 12837 |
. . . . . . 7
β’
((degβπΉ)
β β€ β (degβπΉ) β
(β€β₯β(degβπΉ))) |
10 | | peano2uz 12885 |
. . . . . . 7
β’
((degβπΉ)
β (β€β₯β(degβπΉ)) β ((degβπΉ) + 1) β
(β€β₯β(degβπΉ))) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . 6
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β) β ((degβπΉ) + 1) β
(β€β₯β(degβπΉ))) |
12 | | simpr 486 |
. . . . . 6
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β) β π β β) |
13 | | eqid 2733 |
. . . . . . 7
β’
(coeffβπΉ) =
(coeffβπΉ) |
14 | | eqid 2733 |
. . . . . . 7
β’
(degβπΉ) =
(degβπΉ) |
15 | 13, 14 | coeid3 25754 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ ((degβπΉ) + 1) β
(β€β₯β(degβπΉ)) β§ π β β) β (πΉβπ) = Ξ£π β (0...((degβπΉ) + 1))(((coeffβπΉ)βπ) Β· (πβπ))) |
16 | 4, 11, 12, 15 | syl3anc 1372 |
. . . . 5
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β) β (πΉβπ) = Ξ£π β (0...((degβπΉ) + 1))(((coeffβπΉ)βπ) Β· (πβπ))) |
17 | 16 | mpteq2dva 5249 |
. . . 4
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (π β β β¦ (πΉβπ)) = (π β β β¦ Ξ£π β (0...((degβπΉ) + 1))(((coeffβπΉ)βπ) Β· (πβπ)))) |
18 | 3, 17 | eqtrd 2773 |
. . 3
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ = (π β β β¦ Ξ£π β (0...((degβπΉ) + 1))(((coeffβπΉ)βπ) Β· (πβπ)))) |
19 | 6 | nn0cnd 12534 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (degβπΉ) β β) |
20 | | ax-1cn 11168 |
. . . . . . . 8
β’ 1 β
β |
21 | | pncan 11466 |
. . . . . . . 8
β’
(((degβπΉ)
β β β§ 1 β β) β (((degβπΉ) + 1) β 1) = (degβπΉ)) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (((degβπΉ) + 1) β 1) = (degβπΉ)) |
23 | 22 | eqcomd 2739 |
. . . . . 6
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (degβπΉ) = (((degβπΉ) + 1) β 1)) |
24 | 23 | oveq2d 7425 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (0...(degβπΉ)) = (0...(((degβπΉ) + 1) β 1))) |
25 | 24 | sumeq1d 15647 |
. . . 4
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β Ξ£π β (0...(degβπΉ))(((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ)) = Ξ£π β (0...(((degβπΉ) + 1) β 1))(((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ))) |
26 | 25 | mpteq2dv 5251 |
. . 3
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (π β β β¦ Ξ£π β (0...(degβπΉ))(((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ))) = (π β β β¦ Ξ£π β (0...(((degβπΉ) + 1) β 1))(((π β β0
β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ)))) |
27 | 13 | coef3 25746 |
. . . 4
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆβ) |
28 | 27 | adantl 483 |
. . 3
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (coeffβπΉ):β0βΆβ) |
29 | | oveq1 7416 |
. . . . 5
β’ (π = π β (π + 1) = (π + 1)) |
30 | | fvoveq1 7432 |
. . . . 5
β’ (π = π β ((coeffβπΉ)β(π + 1)) = ((coeffβπΉ)β(π + 1))) |
31 | 29, 30 | oveq12d 7427 |
. . . 4
β’ (π = π β ((π + 1) Β· ((coeffβπΉ)β(π + 1))) = ((π + 1) Β· ((coeffβπΉ)β(π + 1)))) |
32 | 31 | cbvmptv 5262 |
. . 3
β’ (π β β0
β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1)))) = (π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1)))) |
33 | | peano2nn0 12512 |
. . . 4
β’
((degβπΉ)
β β0 β ((degβπΉ) + 1) β
β0) |
34 | 6, 33 | syl 17 |
. . 3
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((degβπΉ) + 1) β
β0) |
35 | 18, 26, 28, 32, 34 | dvply1 25797 |
. 2
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (β D πΉ) = (π β β β¦ Ξ£π β (0...(degβπΉ))(((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ)))) |
36 | | cnfldbas 20948 |
. . . . 5
β’ β =
(Baseββfld) |
37 | 36 | subrgss 20320 |
. . . 4
β’ (π β
(SubRingββfld) β π β β) |
38 | 37 | adantr 482 |
. . 3
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β π β β) |
39 | | elfznn0 13594 |
. . . 4
β’ (π β (0...(degβπΉ)) β π β β0) |
40 | | simpll 766 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β π β
(SubRingββfld)) |
41 | | zsssubrg 21003 |
. . . . . . . . 9
β’ (π β
(SubRingββfld) β β€ β π) |
42 | 41 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β β€
β π) |
43 | | peano2nn0 12512 |
. . . . . . . . . 10
β’ (π β β0
β (π + 1) β
β0) |
44 | 43 | adantl 483 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β (π + 1) β
β0) |
45 | 44 | nn0zd 12584 |
. . . . . . . 8
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β (π + 1) β
β€) |
46 | 42, 45 | sseldd 3984 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β (π + 1) β π) |
47 | | simplr 768 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β πΉ β (Polyβπ)) |
48 | | subrgsubg 20325 |
. . . . . . . . . . 11
β’ (π β
(SubRingββfld) β π β
(SubGrpββfld)) |
49 | | cnfld0 20969 |
. . . . . . . . . . . 12
β’ 0 =
(0gββfld) |
50 | 49 | subg0cl 19014 |
. . . . . . . . . . 11
β’ (π β
(SubGrpββfld) β 0 β π) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
β’ (π β
(SubRingββfld) β 0 β π) |
52 | 51 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β 0 β
π) |
53 | 13 | coef2 25745 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ 0 β π) β (coeffβπΉ):β0βΆπ) |
54 | 47, 52, 53 | syl2anc 585 |
. . . . . . . 8
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
(coeffβπΉ):β0βΆπ) |
55 | 54, 44 | ffvelcdmd 7088 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβπΉ)β(π + 1)) β π) |
56 | | cnfldmul 20950 |
. . . . . . . 8
β’ Β·
= (.rββfld) |
57 | 56 | subrgmcl 20331 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ (π + 1) β π β§ ((coeffβπΉ)β(π + 1)) β π) β ((π + 1) Β· ((coeffβπΉ)β(π + 1))) β π) |
58 | 40, 46, 55, 57 | syl3anc 1372 |
. . . . . 6
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β ((π + 1) Β·
((coeffβπΉ)β(π + 1))) β π) |
59 | 58 | fmpttd 7115 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1)))):β0βΆπ) |
60 | 59 | ffvelcdmda 7087 |
. . . 4
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β ((π β β0
β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) β π) |
61 | 39, 60 | sylan2 594 |
. . 3
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β (0...(degβπΉ))) β ((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) β π) |
62 | 38, 6, 61 | elplyd 25716 |
. 2
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (π β β β¦ Ξ£π β (0...(degβπΉ))(((π β β0 β¦ ((π + 1) Β·
((coeffβπΉ)β(π + 1))))βπ) Β· (πβπ))) β (Polyβπ)) |
63 | 35, 62 | eqeltrd 2834 |
1
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (β D πΉ) β (Polyβπ)) |