Metamath Proof Explorer


Theorem plyco

Description: The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses plyco.1 φ F Poly S
plyco.2 φ G Poly S
plyco.3 φ x S y S x + y S
plyco.4 φ x S y S x y S
Assertion plyco φ F G Poly S

Proof

Step Hyp Ref Expression
1 plyco.1 φ F Poly S
2 plyco.2 φ G Poly S
3 plyco.3 φ x S y S x + y S
4 plyco.4 φ x S y S x y S
5 plyf G Poly S G :
6 2 5 syl φ G :
7 6 ffvelrnda φ z G z
8 6 feqmptd φ G = z G z
9 eqid coeff F = coeff F
10 eqid deg F = deg F
11 9 10 coeid F Poly S F = x k = 0 deg F coeff F k x k
12 1 11 syl φ F = x k = 0 deg F coeff F k x k
13 oveq1 x = G z x k = G z k
14 13 oveq2d x = G z coeff F k x k = coeff F k G z k
15 14 sumeq2sdv x = G z k = 0 deg F coeff F k x k = k = 0 deg F coeff F k G z k
16 7 8 12 15 fmptco φ F G = z k = 0 deg F coeff F k G z k
17 dgrcl F Poly S deg F 0
18 1 17 syl φ deg F 0
19 oveq2 x = 0 0 x = 0 0
20 19 sumeq1d x = 0 k = 0 x coeff F k G z k = k = 0 0 coeff F k G z k
21 20 mpteq2dv x = 0 z k = 0 x coeff F k G z k = z k = 0 0 coeff F k G z k
22 21 eleq1d x = 0 z k = 0 x coeff F k G z k Poly S z k = 0 0 coeff F k G z k Poly S
23 22 imbi2d x = 0 φ z k = 0 x coeff F k G z k Poly S φ z k = 0 0 coeff F k G z k Poly S
24 oveq2 x = d 0 x = 0 d
25 24 sumeq1d x = d k = 0 x coeff F k G z k = k = 0 d coeff F k G z k
26 25 mpteq2dv x = d z k = 0 x coeff F k G z k = z k = 0 d coeff F k G z k
27 26 eleq1d x = d z k = 0 x coeff F k G z k Poly S z k = 0 d coeff F k G z k Poly S
28 27 imbi2d x = d φ z k = 0 x coeff F k G z k Poly S φ z k = 0 d coeff F k G z k Poly S
29 oveq2 x = d + 1 0 x = 0 d + 1
30 29 sumeq1d x = d + 1 k = 0 x coeff F k G z k = k = 0 d + 1 coeff F k G z k
31 30 mpteq2dv x = d + 1 z k = 0 x coeff F k G z k = z k = 0 d + 1 coeff F k G z k
32 31 eleq1d x = d + 1 z k = 0 x coeff F k G z k Poly S z k = 0 d + 1 coeff F k G z k Poly S
33 32 imbi2d x = d + 1 φ z k = 0 x coeff F k G z k Poly S φ z k = 0 d + 1 coeff F k G z k Poly S
34 oveq2 x = deg F 0 x = 0 deg F
35 34 sumeq1d x = deg F k = 0 x coeff F k G z k = k = 0 deg F coeff F k G z k
36 35 mpteq2dv x = deg F z k = 0 x coeff F k G z k = z k = 0 deg F coeff F k G z k
37 36 eleq1d x = deg F z k = 0 x coeff F k G z k Poly S z k = 0 deg F coeff F k G z k Poly S
38 37 imbi2d x = deg F φ z k = 0 x coeff F k G z k Poly S φ z k = 0 deg F coeff F k G z k Poly S
39 0z 0
40 7 exp0d φ z G z 0 = 1
41 40 oveq2d φ z coeff F 0 G z 0 = coeff F 0 1
42 plybss F Poly S S
43 1 42 syl φ S
44 0cnd φ 0
45 44 snssd φ 0
46 43 45 unssd φ S 0
47 9 coef F Poly S coeff F : 0 S 0
48 1 47 syl φ coeff F : 0 S 0
49 0nn0 0 0
50 ffvelrn coeff F : 0 S 0 0 0 coeff F 0 S 0
51 48 49 50 sylancl φ coeff F 0 S 0
52 46 51 sseldd φ coeff F 0
53 52 adantr φ z coeff F 0
54 53 mulid1d φ z coeff F 0 1 = coeff F 0
55 41 54 eqtrd φ z coeff F 0 G z 0 = coeff F 0
56 55 53 eqeltrd φ z coeff F 0 G z 0
57 fveq2 k = 0 coeff F k = coeff F 0
58 oveq2 k = 0 G z k = G z 0
59 57 58 oveq12d k = 0 coeff F k G z k = coeff F 0 G z 0
60 59 fsum1 0 coeff F 0 G z 0 k = 0 0 coeff F k G z k = coeff F 0 G z 0
61 39 56 60 sylancr φ z k = 0 0 coeff F k G z k = coeff F 0 G z 0
62 61 55 eqtrd φ z k = 0 0 coeff F k G z k = coeff F 0
63 62 mpteq2dva φ z k = 0 0 coeff F k G z k = z coeff F 0
64 fconstmpt × coeff F 0 = z coeff F 0
65 63 64 eqtr4di φ z k = 0 0 coeff F k G z k = × coeff F 0
66 plyconst S 0 coeff F 0 S 0 × coeff F 0 Poly S 0
67 46 51 66 syl2anc φ × coeff F 0 Poly S 0
68 plyun0 Poly S 0 = Poly S
69 67 68 eleqtrdi φ × coeff F 0 Poly S
70 65 69 eqeltrd φ z k = 0 0 coeff F k G z k Poly S
71 simprr φ d 0 z k = 0 d coeff F k G z k Poly S z k = 0 d coeff F k G z k Poly S
72 46 adantr φ d 0 S 0
73 peano2nn0 d 0 d + 1 0
74 ffvelrn coeff F : 0 S 0 d + 1 0 coeff F d + 1 S 0
75 48 73 74 syl2an φ d 0 coeff F d + 1 S 0
76 plyconst S 0 coeff F d + 1 S 0 × coeff F d + 1 Poly S 0
77 72 75 76 syl2anc φ d 0 × coeff F d + 1 Poly S 0
78 77 68 eleqtrdi φ d 0 × coeff F d + 1 Poly S
79 nn0p1nn d 0 d + 1
80 oveq2 x = 1 G z x = G z 1
81 80 mpteq2dv x = 1 z G z x = z G z 1
82 81 eleq1d x = 1 z G z x Poly S z G z 1 Poly S
83 82 imbi2d x = 1 φ z G z x Poly S φ z G z 1 Poly S
84 oveq2 x = d G z x = G z d
85 84 mpteq2dv x = d z G z x = z G z d
86 85 eleq1d x = d z G z x Poly S z G z d Poly S
87 86 imbi2d x = d φ z G z x Poly S φ z G z d Poly S
88 oveq2 x = d + 1 G z x = G z d + 1
89 88 mpteq2dv x = d + 1 z G z x = z G z d + 1
90 89 eleq1d x = d + 1 z G z x Poly S z G z d + 1 Poly S
91 90 imbi2d x = d + 1 φ z G z x Poly S φ z G z d + 1 Poly S
92 7 exp1d φ z G z 1 = G z
93 92 mpteq2dva φ z G z 1 = z G z
94 93 8 eqtr4d φ z G z 1 = G
95 94 2 eqeltrd φ z G z 1 Poly S
96 simprr φ d z G z d Poly S z G z d Poly S
97 2 adantr φ d z G z d Poly S G Poly S
98 3 adantlr φ d z G z d Poly S x S y S x + y S
99 4 adantlr φ d z G z d Poly S x S y S x y S
100 96 97 98 99 plymul φ d z G z d Poly S z G z d × f G Poly S
101 100 expr φ d z G z d Poly S z G z d × f G Poly S
102 cnex V
103 102 a1i φ d V
104 ovexd φ d z G z d V
105 7 adantlr φ d z G z
106 eqidd φ d z G z d = z G z d
107 8 adantr φ d G = z G z
108 103 104 105 106 107 offval2 φ d z G z d × f G = z G z d G z
109 nnnn0 d d 0
110 109 ad2antlr φ d z d 0
111 105 110 expp1d φ d z G z d + 1 = G z d G z
112 111 mpteq2dva φ d z G z d + 1 = z G z d G z
113 108 112 eqtr4d φ d z G z d × f G = z G z d + 1
114 113 eleq1d φ d z G z d × f G Poly S z G z d + 1 Poly S
115 101 114 sylibd φ d z G z d Poly S z G z d + 1 Poly S
116 115 expcom d φ z G z d Poly S z G z d + 1 Poly S
117 116 a2d d φ z G z d Poly S φ z G z d + 1 Poly S
118 83 87 91 91 95 117 nnind d + 1 φ z G z d + 1 Poly S
119 79 118 syl d 0 φ z G z d + 1 Poly S
120 119 impcom φ d 0 z G z d + 1 Poly S
121 3 adantlr φ d 0 x S y S x + y S
122 4 adantlr φ d 0 x S y S x y S
123 78 120 121 122 plymul φ d 0 × coeff F d + 1 × f z G z d + 1 Poly S
124 123 adantrr φ d 0 z k = 0 d coeff F k G z k Poly S × coeff F d + 1 × f z G z d + 1 Poly S
125 3 adantlr φ d 0 z k = 0 d coeff F k G z k Poly S x S y S x + y S
126 71 124 125 plyadd φ d 0 z k = 0 d coeff F k G z k Poly S z k = 0 d coeff F k G z k + f × coeff F d + 1 × f z G z d + 1 Poly S
127 126 expr φ d 0 z k = 0 d coeff F k G z k Poly S z k = 0 d coeff F k G z k + f × coeff F d + 1 × f z G z d + 1 Poly S
128 102 a1i φ d 0 V
129 sumex k = 0 d coeff F k G z k V
130 129 a1i φ d 0 z k = 0 d coeff F k G z k V
131 ovexd φ d 0 z coeff F d + 1 G z d + 1 V
132 eqidd φ d 0 z k = 0 d coeff F k G z k = z k = 0 d coeff F k G z k
133 fvexd φ d 0 z coeff F d + 1 V
134 ovexd φ d 0 z G z d + 1 V
135 fconstmpt × coeff F d + 1 = z coeff F d + 1
136 135 a1i φ d 0 × coeff F d + 1 = z coeff F d + 1
137 eqidd φ d 0 z G z d + 1 = z G z d + 1
138 128 133 134 136 137 offval2 φ d 0 × coeff F d + 1 × f z G z d + 1 = z coeff F d + 1 G z d + 1
139 128 130 131 132 138 offval2 φ d 0 z k = 0 d coeff F k G z k + f × coeff F d + 1 × f z G z d + 1 = z k = 0 d coeff F k G z k + coeff F d + 1 G z d + 1
140 simplr φ d 0 z d 0
141 nn0uz 0 = 0
142 140 141 eleqtrdi φ d 0 z d 0
143 9 coef3 F Poly S coeff F : 0
144 1 143 syl φ coeff F : 0
145 144 ad2antrr φ d 0 z coeff F : 0
146 elfznn0 k 0 d + 1 k 0
147 ffvelrn coeff F : 0 k 0 coeff F k
148 145 146 147 syl2an φ d 0 z k 0 d + 1 coeff F k
149 7 adantlr φ d 0 z G z
150 expcl G z k 0 G z k
151 149 146 150 syl2an φ d 0 z k 0 d + 1 G z k
152 148 151 mulcld φ d 0 z k 0 d + 1 coeff F k G z k
153 fveq2 k = d + 1 coeff F k = coeff F d + 1
154 oveq2 k = d + 1 G z k = G z d + 1
155 153 154 oveq12d k = d + 1 coeff F k G z k = coeff F d + 1 G z d + 1
156 142 152 155 fsump1 φ d 0 z k = 0 d + 1 coeff F k G z k = k = 0 d coeff F k G z k + coeff F d + 1 G z d + 1
157 156 mpteq2dva φ d 0 z k = 0 d + 1 coeff F k G z k = z k = 0 d coeff F k G z k + coeff F d + 1 G z d + 1
158 139 157 eqtr4d φ d 0 z k = 0 d coeff F k G z k + f × coeff F d + 1 × f z G z d + 1 = z k = 0 d + 1 coeff F k G z k
159 158 eleq1d φ d 0 z k = 0 d coeff F k G z k + f × coeff F d + 1 × f z G z d + 1 Poly S z k = 0 d + 1 coeff F k G z k Poly S
160 127 159 sylibd φ d 0 z k = 0 d coeff F k G z k Poly S z k = 0 d + 1 coeff F k G z k Poly S
161 160 expcom d 0 φ z k = 0 d coeff F k G z k Poly S z k = 0 d + 1 coeff F k G z k Poly S
162 161 a2d d 0 φ z k = 0 d coeff F k G z k Poly S φ z k = 0 d + 1 coeff F k G z k Poly S
163 23 28 33 38 70 162 nn0ind deg F 0 φ z k = 0 deg F coeff F k G z k Poly S
164 18 163 mpcom φ z k = 0 deg F coeff F k G z k Poly S
165 16 164 eqeltrd φ F G Poly S