Definition df-coe1 20351

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

Assertion

Ref	Expression
df-coe1	⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))

Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-coe1

Step	Hyp	Ref	Expression
1		cco1 20346	. 2 class coe1
2		vf	. . 3 setvar 𝑓
3		cvv 3494	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		cn0 11898	. . . 4 class ℕ0
6		c1o 8095	. . . . . 6 class 1o
7	4	cv 1536	. . . . . . 7 class 𝑛
8	7	csn 4567	. . . . . 6 class {𝑛}
9	6, 8	cxp 5553	. . . . 5 class (1o × {𝑛})
10	2	cv 1536	. . . . 5 class 𝑓
11	9, 10	cfv 6355	. . . 4 class (𝑓‘(1o × {𝑛}))
12	4, 5, 11	cmpt 5146	. . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛})))
13	2, 3, 12	cmpt 5146	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
14	1, 13	wceq 1537	1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))

This definition is referenced by:  coe1fval  20373