Definition df-mnc 43145

Description: Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)

Assertion

Ref	Expression
df-mnc	⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})

Distinct variable group:   𝑠,𝑝

Detailed syntax breakdown of Definition df-mnc

Step	Hyp	Ref	Expression
1		cmnc 43143	. 2 class Monic
2		vs	. . 3 setvar 𝑠
3		cc 11153	. . . 4 class ℂ
4	3	cpw 4600	. . 3 class 𝒫 ℂ
5		vp	. . . . . . . 8 setvar 𝑝
6	5	cv 1539	. . . . . . 7 class 𝑝
7		cdgr 26226	. . . . . . 7 class deg
8	6, 7	cfv 6561	. . . . . 6 class (deg‘𝑝)
9		ccoe 26225	. . . . . . 7 class coeff
10	6, 9	cfv 6561	. . . . . 6 class (coeff‘𝑝)
11	8, 10	cfv 6561	. . . . 5 class ((coeff‘𝑝)‘(deg‘𝑝))
12		c1 11156	. . . . 5 class 1
13	11, 12	wceq 1540	. . . 4 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
14	2	cv 1539	. . . . 5 class 𝑠
15		cply 26223	. . . . 5 class Poly
16	14, 15	cfv 6561	. . . 4 class (Poly‘𝑠)
17	13, 5, 16	crab 3436	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}
18	2, 4, 17	cmpt 5225	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
19	1, 18	wceq 1540	1 wff Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})

This definition is referenced by:  elmnc  43148