Definition df-mnc

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

	Ref	Expression
Assertion	df-mnc	|- Monic = ( s e. ~P CC |-> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnc	|- Monic
1		vs	|- s
2		cc	|- CC
3	2	cpw	|- ~P CC
4		vp	|- p
5		cply	|- Poly
6	1	cv	|- s
7	6 5	cfv	|- ( Poly ` s )
8		ccoe	|- coeff
9	4	cv	|- p
10	9 8	cfv	|- ( coeff ` p )
11		cdgr	|- deg
12	9 11	cfv	|- ( deg ` p )
13	12 10	cfv	|- ( ( coeff ` p ) ` ( deg ` p ) )
14		c1	|- 1
15	13 14	wceq	|- ( ( coeff ` p ) ` ( deg ` p ) ) = 1
16	15 4 7	crab	|- { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 }
17	1 3 16	cmpt	|- ( s e. ~P CC |-> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } )
18	0 17	wceq	|- Monic = ( s e. ~P CC |-> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } )