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 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
6 5 simprbi ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑚 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
7 1 6 syl ( 𝜑 → ∃ 𝑚 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
8 elply2 ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
9 8 simprbi ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
10 2 9 syl ( 𝜑 → ∃ 𝑛 ∈ ℕ0𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
11 reeanv ( ∃ 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑛 ∈ ℕ0𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
12 reeanv ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ↔ ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
13 simp1l ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝜑 )
14 13 1 syl ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
15 13 2 syl ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
16 13 3 sylan ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
17 simp1rl ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑚 ∈ ℕ0 )
18 simp1rr ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑛 ∈ ℕ0 )
19 simp2l ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
20 simp2r ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
21 simp3ll ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } )
22 simp3rl ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
23 simp3lr ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 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 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) ) ) )
34 simp3rr ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 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 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐺 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) ) ) )
43 13 4 sylan ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
44 14 15 16 17 18 19 20 21 22 33 42 43 plymullem ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )
45 44 3expia ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) ∧ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∧ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
46 45 rexlimdvva ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
47 12 46 syl5bir ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ) ) → ( ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
48 47 rexlimdvva ( 𝜑 → ( ∃ 𝑚 ∈ ℕ0𝑛 ∈ ℕ0 ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
49 11 48 syl5bir ( 𝜑 → ( ( ∃ 𝑚 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑛 ∈ ℕ0𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) )
50 7 10 49 mp2and ( 𝜑 → ( 𝐹f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )