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 ‘ 𝐹 ) ∈ ( ℂ ↑_m ℕ₀ ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coeval	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
2		coeeu	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
3		riotacl2	⊢ ( ∃! 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∣ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } )
4	2 3	syl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∣ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } )
5	1 4	eqeltrd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∣ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 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 ‘ 𝐹 ) → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
15	14	elrab	⊢ ( ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∣ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ↔ ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑_m ℕ₀ ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
16	5 15	sylib	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑_m ℕ₀ ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )