This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coeval

Description: Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Assertion	coeval	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
2	1	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
3		eqeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
4	3	anbi2d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
5	4	rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
6	5	riotabidv	⊢ ( 𝑓 = 𝐹 → ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
7		df-coe	⊢ coeff = ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
8		riotaex	⊢ ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
10	2 9	syl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )