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 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )