Metamath Proof Explorer


Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coelem ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 coeval ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
2 coeeu ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
3 riotacl2 ( ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) } )
4 2 3 syl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) } )
5 1 4 eqeltrd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) } )
6 imaeq1 ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) )
7 6 eqeq1d ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
8 fveq1 ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎𝑘 ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) )
9 8 oveq1d ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) )
10 9 sumeq2sdv ( 𝑎 = ( coeff ‘ 𝐹 ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) )
11 10 mpteq2dv ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )
12 11 eqeq2d ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
13 7 12 anbi12d ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
14 13 rexbidv ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
15 14 elrab ( ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) } ↔ ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
16 5 15 sylib ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )