Definition df-coe1 19374

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 ↦ (𝑓‘(1𝑜 × {𝑛}))))

Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-coe1

Step	Hyp	Ref	Expression
1		cco1 19369	. 2 class coe1
2		vf	. . 3 setvar 𝑓
3		cvv 3173	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		cn0 11169	. . . 4 class ℕ0
6		c1o 7440	. . . . . 6 class 1𝑜
7	4	cv 1474	. . . . . . 7 class 𝑛
8	7	csn 4125	. . . . . 6 class {𝑛}
9	6, 8	cxp 5036	. . . . 5 class (1𝑜 × {𝑛})
10	2	cv 1474	. . . . 5 class 𝑓
11	9, 10	cfv 5804	. . . 4 class (𝑓‘(1𝑜 × {𝑛}))
12	4, 5, 11	cmpt 4643	. . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛})))
13	2, 3, 12	cmpt 4643	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
14	1, 13	wceq 1475	1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))

This definition is referenced by:  coe1fval  19396