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

Metamath Proof Explorer

Theorem plyval

Description: Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyval ( 𝑆 ⊆ ℂ → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 1 elpw2 ⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
3 uneq1 ⊢ ( 𝑥 = 𝑆 → ( 𝑥 ∪ { 0 } ) = ( 𝑆 ∪ { 0 } ) )
4 3 oveq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) = ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
5 4 rexeqdv ⊢ ( 𝑥 = 𝑆 → ( ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
6 5 rexbidv ⊢ ( 𝑥 = 𝑆 → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
7 6 abbidv ⊢ ( 𝑥 = 𝑆 → { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
8 df-ply ⊢ Poly = ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
9 nn0ex ⊢ ℕ0 ∈ V
10 ovex ⊢ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∈ V
11 9 10 ab2rexex ⊢ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } ∈ V
12 7 8 11 fvmpt ⊢ ( 𝑆 ∈ 𝒫 ℂ → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
13 2 12 sylbir ⊢ ( 𝑆 ⊆ ℂ → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )