Definition df-coe1

Description: Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Assertion	df-coe1	$$⊢{\mathrm{coe}}_1=\left(f\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼f\left(1_{𝑜}\times \left\{n\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cco1	$$class{\mathrm{coe}}_1$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5	1	cv	$$setvarf$$
6		c1o	$$class{1}_{𝑜}$$
7	3	cv	$$setvarn$$
8	7	csn	$$class\left\{n\right\}$$
9	6 8	cxp	$$class\left(1_{𝑜}\times \left\{n\right\}\right)$$
10	9 5	cfv	$$classf\left(1_{𝑜}\times \left\{n\right\}\right)$$
11	3 4 10	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼f\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$
12	1 2 11	cmpt	$$class\left(f\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼f\left(1_{𝑜}\times \left\{n\right\}\right)\right)\right)$$
13	0 12	wceq	$$wff{\mathrm{coe}}_1=\left(f\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼f\left(1_{𝑜}\times \left\{n\right\}\right)\right)\right)$$