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

Metamath Proof Explorer

Definition df-ply

Description: Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion df-ply Poly = ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cply ⊢ Poly
1 vx ⊢ 𝑥
2 cc ⊢ ℂ
3 2 cpw ⊢ 𝒫 ℂ
4 vf ⊢ 𝑓
5 vn ⊢ 𝑛
6 cn0 ⊢ ℕ0
7 va ⊢ 𝑎
8 1 cv ⊢ 𝑥
9 cc0 ⊢ 0
10 9 csn ⊢ { 0 }
11 8 10 cun ⊢ ( 𝑥 ∪ { 0 } )
12 cmap ⊢ ↑m
13 11 6 12 co ⊢ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 )
14 4 cv ⊢ 𝑓
15 vz ⊢ 𝑧
16 vk ⊢ 𝑘
17 cfz ⊢ ...
18 5 cv ⊢ 𝑛
19 9 18 17 co ⊢ ( 0 ... 𝑛 )
20 7 cv ⊢ 𝑎
21 16 cv ⊢ 𝑘
22 21 20 cfv ⊢ ( 𝑎 ‘ 𝑘 )
23 cmul ⊢ ·
24 15 cv ⊢ 𝑧
25 cexp ⊢ ↑
26 24 21 25 co ⊢ ( 𝑧 ↑ 𝑘 )
27 22 26 23 co ⊢ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
28 19 27 16 csu ⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
29 15 2 28 cmpt ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
30 14 29 wceq ⊢ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
31 30 7 13 wrex ⊢ ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
32 31 5 6 wrex ⊢ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
33 32 4 cab ⊢ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) }
34 1 3 33 cmpt ⊢ ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
35 0 34 wceq ⊢ Poly = ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )