plymul - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plymul		Structured version Visualization version GIF version

Theorem plymul 25368

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

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

**Assertion**
Ref	Expression
plymul	⊢ (𝜑 → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆))

Distinct variable groups: 𝑥,𝑦,𝐹 𝑥,𝑆,𝑦 𝑥,𝐺,𝑦 𝜑,𝑥,𝑦

Proof of Theorem plymul Dummy variables 𝑘 𝑚 𝑛 𝑧 𝑎 𝑏 𝑗 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		plyadd.1	. . 3 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
2		elply2 25346	. . . 4 ⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑚 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘))))))
3	2	simprbi 497	. . 3 ⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑚 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))))
4	1, 3	syl 17	. 2 ⊢ (𝜑 → ∃𝑚 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))))
5		plyadd.2	. . 3 ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
6		elply2 25346	. . . 4 ⊢ (𝐺 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ₀ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))))
7	6	simprbi 497	. . 3 ⊢ (𝐺 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ₀ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))
8	5, 7	syl 17	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))
9		reeanv 3293	. . 3 ⊢ (∃𝑚 ∈ ℕ₀ ∃𝑛 ∈ ℕ₀ (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) ↔ (∃𝑚 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑛 ∈ ℕ₀ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))))
10		reeanv 3293	. . . . 5 ⊢ (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)(((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) ↔ (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))))
11		simp1l 1196	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝜑)
12	11, 1	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 ∈ (Poly‘𝑆))
13	11, 5	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐺 ∈ (Poly‘𝑆))
14		plyadd.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
15	11, 14	sylan 580	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
16		simp1rl 1237	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑚 ∈ ℕ₀)
17		simp1rr 1238	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑛 ∈ ℕ₀)
18		simp2l 1198	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀))
19		simp2r 1199	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀))
20		simp3ll 1243	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0})
21		simp3rl 1245	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0})
22		simp3lr 1244	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘))))
23		oveq1 7276	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧↑𝑘) = (𝑤↑𝑘))
24	23	oveq2d 7285	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑎‘𝑘) · (𝑤↑𝑘)))
25	24	sumeq2sdv 15405	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑤↑𝑘)))
26		fveq2 6768	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝑎‘𝑘) = (𝑎‘𝑗))
27		oveq2 7277	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝑤↑𝑘) = (𝑤↑𝑗))
28	26, 27	oveq12d 7287	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → ((𝑎‘𝑘) · (𝑤↑𝑘)) = ((𝑎‘𝑗) · (𝑤↑𝑗)))
29	28	cbvsumv 15397	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑎‘𝑗) · (𝑤↑𝑗))
30	25, 29	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑎‘𝑗) · (𝑤↑𝑗)))
31	30	cbvmptv 5188	. . . . . . . . 9 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑎‘𝑗) · (𝑤↑𝑗)))
32	22, 31	eqtrdi 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑎‘𝑗) · (𝑤↑𝑗))))
33		simp3rr 1246	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))
34	23	oveq2d 7285	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑘) · (𝑧↑𝑘)) = ((𝑏‘𝑘) · (𝑤↑𝑘)))
35	34	sumeq2sdv 15405	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑤↑𝑘)))
36		fveq2 6768	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
37	36, 27	oveq12d 7287	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → ((𝑏‘𝑘) · (𝑤↑𝑘)) = ((𝑏‘𝑗) · (𝑤↑𝑗)))
38	37	cbvsumv 15397	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑏‘𝑗) · (𝑤↑𝑗))
39	35, 38	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑏‘𝑗) · (𝑤↑𝑗)))
40	39	cbvmptv 5188	. . . . . . . . 9 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑏‘𝑗) · (𝑤↑𝑗)))
41	33, 40	eqtrdi 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐺 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑏‘𝑗) · (𝑤↑𝑗))))
42		plymul.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)
43	11, 42	sylan 580	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)
44	12, 13, 15, 16, 17, 18, 19, 20, 21, 32, 41, 43	plymullem 25366	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)) ∧ (((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆))
45	44	3expia 1120	. . . . . 6 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) ∧ (𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀) ∧ 𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀))) → ((((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆)))
46	45	rexlimdvva 3222	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)(((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆)))
47	10, 46	syl5bir 242	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀)) → ((∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆)))
48	47	rexlimdvva 3222	. . 3 ⊢ (𝜑 → (∃𝑚 ∈ ℕ₀ ∃𝑛 ∈ ℕ₀ (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆)))
49	9, 48	syl5bir 242	. 2 ⊢ (𝜑 → ((∃𝑚 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑎 “ (ℤ_≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑛 ∈ ℕ₀ ∃𝑏 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)((𝑏 “ (ℤ_≥‘(𝑛 + 1))) = {0} ∧ 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆)))
50	4, 8, 49	mp2and 696	1 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺) ∈ (Poly‘𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∃wrex 3065 ∪ cun 3886 ⊆ wss 3888 {csn 4563 ↦ cmpt 5158 “ cima 5589 ‘cfv 6428 (class class class)co 7269 ∘_f cof 7523 ↑_m cmap 8604 ℂcc 10858 0cc0 10860 1c1 10861 + caddc 10863 · cmul 10865 ℕ₀cn0 12222 ℤ_≥cuz 12571 ...cfz 13228 ↑cexp 13771 Σcsu 15386 Polycply 25334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5210 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7580 ax-inf2 9388 ax-cnex 10916 ax-resscn 10917 ax-1cn 10918 ax-icn 10919 ax-addcl 10920 ax-addrcl 10921 ax-mulcl 10922 ax-mulrcl 10923 ax-mulcom 10924 ax-addass 10925 ax-mulass 10926 ax-distr 10927 ax-i2m1 10928 ax-1ne0 10929 ax-1rid 10930 ax-rnegex 10931 ax-rrecex 10932 ax-cnre 10933 ax-pre-lttri 10934 ax-pre-lttrn 10935 ax-pre-ltadd 10936 ax-pre-mulgt0 10937 ax-pre-sup 10938

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-int 4882 df-iun 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5486 df-eprel 5492 df-po 5500 df-so 5501 df-fr 5541 df-se 5542 df-we 5543 df-xp 5592 df-rel 5593 df-cnv 5594 df-co 5595 df-dm 5596 df-rn 5597 df-res 5598 df-ima 5599 df-pred 6197 df-ord 6264 df-on 6265 df-lim 6266 df-suc 6267 df-iota 6386 df-fun 6430 df-fn 6431 df-f 6432 df-f1 6433 df-fo 6434 df-f1o 6435 df-fv 6436 df-isom 6437 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-of 7525 df-om 7705 df-1st 7822 df-2nd 7823 df-frecs 8086 df-wrecs 8117 df-recs 8191 df-rdg 8230 df-1o 8286 df-er 8487 df-map 8606 df-en 8723 df-dom 8724 df-sdom 8725 df-fin 8726 df-sup 9190 df-oi 9258 df-card 9686 df-pnf 11000 df-mnf 11001 df-xr 11002 df-ltxr 11003 df-le 11004 df-sub 11196 df-neg 11197 df-div 11622 df-nn 11963 df-2 12025 df-3 12026 df-n0 12223 df-z 12309 df-uz 12572 df-rp 12720 df-fz 13229 df-fzo 13372 df-seq 13711 df-exp 13772 df-hash 14034 df-cj 14799 df-re 14800 df-im 14801 df-sqrt 14935 df-abs 14936 df-clim 15186 df-sum 15387 df-ply 25338

This theorem is referenced by: plysub 25369 plymulcl 25371 plyco 25391 plydivlem2 25443 plydivlem4 25445 plydiveu 25447 plymulx0 32513 mpaaeu 40962 rngunsnply 40985

W3C validator