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
|
syl5bir |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ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
|
syl5bir |
⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑏 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) ) |
50 |
7 10 49
|
mp2and |
⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) |