Definition df-mnc 39726

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 39724	. 2 class Monic
2		vs	. . 3 setvar 𝑠
3		cc 10529	. . . 4 class ℂ
4	3	cpw 4539	. . 3 class 𝒫 ℂ
5		vp	. . . . . . . 8 setvar 𝑝
6	5	cv 1532	. . . . . . 7 class 𝑝
7		cdgr 24771	. . . . . . 7 class deg
8	6, 7	cfv 6350	. . . . . 6 class (deg‘𝑝)
9		ccoe 24770	. . . . . . 7 class coeff
10	6, 9	cfv 6350	. . . . . 6 class (coeff‘𝑝)
11	8, 10	cfv 6350	. . . . 5 class ((coeff‘𝑝)‘(deg‘𝑝))
12		c1 10532	. . . . 5 class 1
13	11, 12	wceq 1533	. . . 4 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
14	2	cv 1532	. . . . 5 class 𝑠
15		cply 24768	. . . . 5 class Poly
16	14, 15	cfv 6350	. . . 4 class (Poly‘𝑠)
17	13, 5, 16	crab 3142	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}
18	2, 4, 17	cmpt 5139	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
19	1, 18	wceq 1533	1 wff Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})

This definition is referenced by:  elmnc  39729