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

Metamath Proof Explorer

Theorem plymul

Proof