Definition df-mnc

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

	Ref	Expression
Assertion	df-mnc	$$⊢\mathrm{Monic}=\left(s\in 𝒫ℂ⟼\left\{p\in \mathrm{Poly}\left(s\right)|\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)=1\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnc	$$class\mathrm{Monic}$$
1		vs	$$setvars$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vp	$$setvarp$$
5		cply	$$class\mathrm{Poly}$$
6	1	cv	$$setvars$$
7	6 5	cfv	$$class\mathrm{Poly}\left(s\right)$$
8		ccoe	$$class\mathrm{coeff}$$
9	4	cv	$$setvarp$$
10	9 8	cfv	$$class\mathrm{coeff}\left(p\right)$$
11		cdgr	$$class\mathrm{deg}$$
12	9 11	cfv	$$class\mathrm{deg}\left(p\right)$$
13	12 10	cfv	$$class\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)$$
14		c1	$$class1$$
15	13 14	wceq	$$wff\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)=1$$
16	15 4 7	crab	$$class\left\{p\in \mathrm{Poly}\left(s\right)|\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)=1\right\}$$
17	1 3 16	cmpt	$$class\left(s\in 𝒫ℂ⟼\left\{p\in \mathrm{Poly}\left(s\right)|\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)=1\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{Monic}=\left(s\in 𝒫ℂ⟼\left\{p\in \mathrm{Poly}\left(s\right)|\mathrm{coeff}\left(p\right)\left(\mathrm{deg}\left(p\right)\right)=1\right\}\right)$$