Metamath Proof Explorer

Theorem plymul

Description: The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plymul.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
Assertion plymul ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3 plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 plymul.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
5 elply2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
6 5 simprbi ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
7 1 6 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
8 elply2 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
9 8 simprbi ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
10 2 9 syl ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
11 reeanv ⊢ ( ∃ 𝑚 ∈ ℕ0 ∃ 𝑛 ∈ ℕ0 ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
12 reeanv ⊢ ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ↔ ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
13 simp1l ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝜑 )
14 13 1 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
15 13 2 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
16 13 3 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
17 simp1rl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑚 ∈ ℕ0 )
18 simp1rr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑛 ∈ ℕ0 )
19 simp2l ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
20 simp2r ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
21 simp3ll ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } )
22 simp3rl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
23 simp3lr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
24 oveq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑘 ) )
25 24 oveq2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
26 25 sumeq2sdv ⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
27 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑎 ‘ 𝑘 ) = ( 𝑎 ‘ 𝑗 ) )
28 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑤 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑗 ) )
29 27 28 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
30 29 cbvsumv ⊢ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) )
31 26 30 eqtrdi ⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
32 31 cbvmptv ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
33 23 32 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) )
34 simp3rr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
35 24 oveq2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
36 35 sumeq2sdv ⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
37 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑗 ) )
38 37 28 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
39 38 cbvsumv ⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) )
40 36 39 eqtrdi ⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
41 40 cbvmptv ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
42 34 41 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐺 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) )
43 13 4 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
44 14 15 16 17 18 19 20 21 22 33 42 43 plymullem ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )
45 44 3expia ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
46 45 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
47 12 46 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
48 47 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ0 ∃ 𝑛 ∈ ℕ0 ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
49 11 48 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
50 7 10 49 mp2and ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )