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 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyco.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyco.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plyco.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
Assertion plyco ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

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