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	⊢ coe1 = ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cco1	⊢ coe1
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ0
5	1	cv	⊢ 𝑓
6		c1o	⊢ 1o
7	3	cv	⊢ 𝑛
8	7	csn	⊢ { 𝑛 }
9	6 8	cxp	⊢ ( 1o × { 𝑛 } )
10	9 5	cfv	⊢ ( 𝑓 ‘ ( 1o × { 𝑛 } ) )
11	3 4 10	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) )
12	1 2 11	cmpt	⊢ ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) ) )
13	0 12	wceq	⊢ coe1 = ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) ) )