Step | Hyp | Ref
| Expression |
1 | | ssid 4005 |
. . . . 5
β’ β
β β |
2 | | plyconst 25720 |
. . . . 5
β’ ((β
β β β§ π΄
β β) β (β Γ {π΄}) β
(Polyββ)) |
3 | 1, 2 | mpan 689 |
. . . 4
β’ (π΄ β β β (β
Γ {π΄}) β
(Polyββ)) |
4 | | plyssc 25714 |
. . . . 5
β’
(Polyβπ)
β (Polyββ) |
5 | 4 | sseli 3979 |
. . . 4
β’ (πΉ β (Polyβπ) β πΉ β
(Polyββ)) |
6 | | plymulcl 25735 |
. . . 4
β’
(((β Γ {π΄}) β (Polyββ) β§ πΉ β (Polyββ))
β ((β Γ {π΄}) βf Β· πΉ) β
(Polyββ)) |
7 | 3, 5, 6 | syl2an 597 |
. . 3
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β ((β Γ
{π΄}) βf
Β· πΉ) β
(Polyββ)) |
8 | | eqid 2733 |
. . . 4
β’
(coeffβ((β Γ {π΄}) βf Β· πΉ)) = (coeffβ((β
Γ {π΄})
βf Β· πΉ)) |
9 | 8 | coef3 25746 |
. . 3
β’
(((β Γ {π΄}) βf Β· πΉ) β (Polyββ)
β (coeffβ((β Γ {π΄}) βf Β· πΉ)):β0βΆβ) |
10 | | ffn 6718 |
. . 3
β’
((coeffβ((β Γ {π΄}) βf Β· πΉ)):β0βΆβ β
(coeffβ((β Γ {π΄}) βf Β· πΉ)) Fn
β0) |
11 | 7, 9, 10 | 3syl 18 |
. 2
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβ((β
Γ {π΄})
βf Β· πΉ)) Fn β0) |
12 | | fconstg 6779 |
. . . . 5
β’ (π΄ β β β
(β0 Γ {π΄}):β0βΆ{π΄}) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (β0
Γ {π΄}):β0βΆ{π΄}) |
14 | 13 | ffnd 6719 |
. . 3
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (β0
Γ {π΄}) Fn
β0) |
15 | | eqid 2733 |
. . . . . 6
β’
(coeffβπΉ) =
(coeffβπΉ) |
16 | 15 | coef3 25746 |
. . . . 5
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆβ) |
17 | 16 | adantl 483 |
. . . 4
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβπΉ):β0βΆβ) |
18 | 17 | ffnd 6719 |
. . 3
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβπΉ) Fn
β0) |
19 | | nn0ex 12478 |
. . . 4
β’
β0 β V |
20 | 19 | a1i 11 |
. . 3
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β β0
β V) |
21 | | inidm 4219 |
. . 3
β’
(β0 β© β0) =
β0 |
22 | 14, 18, 20, 20, 21 | offn 7683 |
. 2
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β ((β0
Γ {π΄})
βf Β· (coeffβπΉ)) Fn β0) |
23 | 3 | ad2antrr 725 |
. . . . . 6
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β (β
Γ {π΄}) β
(Polyββ)) |
24 | | eqid 2733 |
. . . . . . 7
β’
(coeffβ(β Γ {π΄})) = (coeffβ(β Γ {π΄})) |
25 | 24 | coefv0 25762 |
. . . . . 6
β’ ((β
Γ {π΄}) β
(Polyββ) β ((β Γ {π΄})β0) = ((coeffβ(β Γ
{π΄}))β0)) |
26 | 23, 25 | syl 17 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β ((β
Γ {π΄})β0) =
((coeffβ(β Γ {π΄}))β0)) |
27 | | simpll 766 |
. . . . . 6
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β π΄ β
β) |
28 | | 0cn 11206 |
. . . . . 6
β’ 0 β
β |
29 | | fvconst2g 7203 |
. . . . . 6
β’ ((π΄ β β β§ 0 β
β) β ((β Γ {π΄})β0) = π΄) |
30 | 27, 28, 29 | sylancl 587 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β ((β
Γ {π΄})β0) =
π΄) |
31 | 26, 30 | eqtr3d 2775 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβ(β Γ {π΄}))β0) = π΄) |
32 | | simpr 486 |
. . . . . . 7
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β π β
β0) |
33 | 32 | nn0cnd 12534 |
. . . . . 6
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β π β
β) |
34 | 33 | subid1d 11560 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β (π β 0) = π) |
35 | 34 | fveq2d 6896 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβπΉ)β(π β 0)) = ((coeffβπΉ)βπ)) |
36 | 31, 35 | oveq12d 7427 |
. . 3
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
(((coeffβ(β Γ {π΄}))β0) Β· ((coeffβπΉ)β(π β 0))) = (π΄ Β· ((coeffβπΉ)βπ))) |
37 | 5 | ad2antlr 726 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β πΉ β
(Polyββ)) |
38 | 24, 15 | coemul 25766 |
. . . . 5
β’
(((β Γ {π΄}) β (Polyββ) β§ πΉ β (Polyββ)
β§ π β
β0) β ((coeffβ((β Γ {π΄}) βf Β· πΉ))βπ) = Ξ£π β (0...π)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π)))) |
39 | 23, 37, 32, 38 | syl3anc 1372 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβ((β Γ {π΄}) βf Β· πΉ))βπ) = Ξ£π β (0...π)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π)))) |
40 | | nn0uz 12864 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
41 | 32, 40 | eleqtrdi 2844 |
. . . . . 6
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β π β
(β€β₯β0)) |
42 | | fzss2 13541 |
. . . . . 6
β’ (π β
(β€β₯β0) β (0...0) β (0...π)) |
43 | 41, 42 | syl 17 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β (0...0)
β (0...π)) |
44 | | elfz1eq 13512 |
. . . . . . . 8
β’ (π β (0...0) β π = 0) |
45 | 44 | adantl 483 |
. . . . . . 7
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β (0...0)) β π = 0) |
46 | | fveq2 6892 |
. . . . . . . 8
β’ (π = 0 β
((coeffβ(β Γ {π΄}))βπ) = ((coeffβ(β Γ {π΄}))β0)) |
47 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = 0 β (π β π) = (π β 0)) |
48 | 47 | fveq2d 6896 |
. . . . . . . 8
β’ (π = 0 β ((coeffβπΉ)β(π β π)) = ((coeffβπΉ)β(π β 0))) |
49 | 46, 48 | oveq12d 7427 |
. . . . . . 7
β’ (π = 0 β
(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = (((coeffβ(β Γ {π΄}))β0) Β·
((coeffβπΉ)β(π β 0)))) |
50 | 45, 49 | syl 17 |
. . . . . 6
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β (0...0)) β
(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = (((coeffβ(β Γ {π΄}))β0) Β·
((coeffβπΉ)β(π β 0)))) |
51 | 17 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβπΉ)βπ) β β) |
52 | 27, 51 | mulcld 11234 |
. . . . . . . 8
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β (π΄ Β· ((coeffβπΉ)βπ)) β β) |
53 | 36, 52 | eqeltrd 2834 |
. . . . . . 7
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
(((coeffβ(β Γ {π΄}))β0) Β· ((coeffβπΉ)β(π β 0))) β
β) |
54 | 53 | adantr 482 |
. . . . . 6
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β (0...0)) β
(((coeffβ(β Γ {π΄}))β0) Β· ((coeffβπΉ)β(π β 0))) β
β) |
55 | 50, 54 | eqeltrd 2834 |
. . . . 5
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β (0...0)) β
(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) β β) |
56 | | eldifn 4128 |
. . . . . . . . 9
β’ (π β ((0...π) β (0...0)) β Β¬ π β
(0...0)) |
57 | 56 | adantl 483 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β Β¬ π β
(0...0)) |
58 | | eldifi 4127 |
. . . . . . . . . . . . 13
β’ (π β ((0...π) β (0...0)) β π β (0...π)) |
59 | | elfznn0 13594 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β0) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((0...π) β (0...0)) β π β β0) |
61 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(degβ(β Γ {π΄})) = (degβ(β Γ {π΄})) |
62 | 24, 61 | dgrub 25748 |
. . . . . . . . . . . . 13
β’
(((β Γ {π΄}) β (Polyββ) β§ π β β0
β§ ((coeffβ(β Γ {π΄}))βπ) β 0) β π β€ (degβ(β Γ {π΄}))) |
63 | 62 | 3expia 1122 |
. . . . . . . . . . . 12
β’
(((β Γ {π΄}) β (Polyββ) β§ π β β0)
β (((coeffβ(β Γ {π΄}))βπ) β 0 β π β€ (degβ(β Γ {π΄})))) |
64 | 23, 60, 63 | syl2an 597 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(((coeffβ(β Γ {π΄}))βπ) β 0 β π β€ (degβ(β Γ {π΄})))) |
65 | | 0dgr 25759 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(degβ(β Γ {π΄})) = 0) |
66 | 65 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(degβ(β Γ {π΄})) = 0) |
67 | 66 | breq2d 5161 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β (π β€ (degβ(β
Γ {π΄})) β π β€ 0)) |
68 | 60 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β π β β0) |
69 | | nn0le0eq0 12500 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π β€ 0 β
π = 0)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β (π β€ 0 β π = 0)) |
71 | 67, 70 | bitrd 279 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β (π β€ (degβ(β
Γ {π΄})) β π = 0)) |
72 | 64, 71 | sylibd 238 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(((coeffβ(β Γ {π΄}))βπ) β 0 β π = 0)) |
73 | | id 22 |
. . . . . . . . . . 11
β’ (π = 0 β π = 0) |
74 | | 0z 12569 |
. . . . . . . . . . . 12
β’ 0 β
β€ |
75 | | elfz3 13511 |
. . . . . . . . . . . 12
β’ (0 β
β€ β 0 β (0...0)) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . 11
β’ 0 β
(0...0) |
77 | 73, 76 | eqeltrdi 2842 |
. . . . . . . . . 10
β’ (π = 0 β π β (0...0)) |
78 | 72, 77 | syl6 35 |
. . . . . . . . 9
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(((coeffβ(β Γ {π΄}))βπ) β 0 β π β (0...0))) |
79 | 78 | necon1bd 2959 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β (Β¬ π β (0...0) β
((coeffβ(β Γ {π΄}))βπ) = 0)) |
80 | 57, 79 | mpd 15 |
. . . . . . 7
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
((coeffβ(β Γ {π΄}))βπ) = 0) |
81 | 80 | oveq1d 7424 |
. . . . . 6
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = (0 Β· ((coeffβπΉ)β(π β π)))) |
82 | 17 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
(coeffβπΉ):β0βΆβ) |
83 | | fznn0sub 13533 |
. . . . . . . . 9
β’ (π β (0...π) β (π β π) β
β0) |
84 | 58, 83 | syl 17 |
. . . . . . . 8
β’ (π β ((0...π) β (0...0)) β (π β π) β
β0) |
85 | | ffvelcdm 7084 |
. . . . . . . 8
β’
(((coeffβπΉ):β0βΆβ β§
(π β π) β β0)
β ((coeffβπΉ)β(π β π)) β β) |
86 | 82, 84, 85 | syl2an 597 |
. . . . . . 7
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
((coeffβπΉ)β(π β π)) β β) |
87 | 86 | mul02d 11412 |
. . . . . 6
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β (0 Β·
((coeffβπΉ)β(π β π))) = 0) |
88 | 81, 87 | eqtrd 2773 |
. . . . 5
β’ ((((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β§ π β ((0...π) β (0...0))) β
(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = 0) |
89 | | fzfid 13938 |
. . . . 5
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
(0...π) β
Fin) |
90 | 43, 55, 88, 89 | fsumss 15671 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
Ξ£π β
(0...0)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = Ξ£π β (0...π)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π)))) |
91 | 49 | fsum1 15693 |
. . . . 5
β’ ((0
β β€ β§ (((coeffβ(β Γ {π΄}))β0) Β· ((coeffβπΉ)β(π β 0))) β β) β
Ξ£π β
(0...0)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = (((coeffβ(β Γ {π΄}))β0) Β·
((coeffβπΉ)β(π β 0)))) |
92 | 74, 53, 91 | sylancr 588 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
Ξ£π β
(0...0)(((coeffβ(β Γ {π΄}))βπ) Β· ((coeffβπΉ)β(π β π))) = (((coeffβ(β Γ {π΄}))β0) Β·
((coeffβπΉ)β(π β 0)))) |
93 | 39, 90, 92 | 3eqtr2d 2779 |
. . 3
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβ((β Γ {π΄}) βf Β· πΉ))βπ) = (((coeffβ(β Γ {π΄}))β0) Β·
((coeffβπΉ)β(π β 0)))) |
94 | | simpl 484 |
. . . 4
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β π΄ β β) |
95 | | eqidd 2734 |
. . . 4
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβπΉ)βπ) = ((coeffβπΉ)βπ)) |
96 | 20, 94, 18, 95 | ofc1 7696 |
. . 3
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
(((β0 Γ {π΄}) βf Β·
(coeffβπΉ))βπ) = (π΄ Β· ((coeffβπΉ)βπ))) |
97 | 36, 93, 96 | 3eqtr4d 2783 |
. 2
β’ (((π΄ β β β§ πΉ β (Polyβπ)) β§ π β β0) β
((coeffβ((β Γ {π΄}) βf Β· πΉ))βπ) = (((β0 Γ {π΄}) βf Β·
(coeffβπΉ))βπ)) |
98 | 11, 22, 97 | eqfnfvd 7036 |
1
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβ((β
Γ {π΄})
βf Β· πΉ)) = ((β0 Γ {π΄}) βf Β·
(coeffβπΉ))) |