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 
|- ( ph -> F e. ( Poly ` S ) )
plyco.2 
|- ( ph -> G e. ( Poly ` S ) )
plyco.3 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
plyco.4 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
Assertion plyco 
|- ( ph -> ( F o. G ) e. ( Poly ` S ) )

Proof

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