Definition df-mnc 37703

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

Assertion

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

Distinct variable group:   s, p

Detailed syntax breakdown of Definition df-mnc

Step	Hyp	Ref	Expression
1		cmnc 37701	. 2 class Monic
2		vs	. . 3 setvar s
3		cc 9934	. . . 4 class CC
4	3	cpw 4158	. . 3 class ~P CC
5		vp	. . . . . . . 8 setvar p
6	5	cv 1482	. . . . . . 7 class p
7		cdgr 23943	. . . . . . 7 class deg
8	6, 7	cfv 5888	. . . . . 6 class (deg ` p )
9		ccoe 23942	. . . . . . 7 class coeff
10	6, 9	cfv 5888	. . . . . 6 class (coeff ` p )
11	8, 10	cfv 5888	. . . . 5 class ( (coeff ` p ) ` (deg ` p ) )
12		c1 9937	. . . . 5 class 1
13	11, 12	wceq 1483	. . . 4 wff ( (coeff ` p ) ` (deg ` p ) ) = 1
14	2	cv 1482	. . . . 5 class s
15		cply 23940	. . . . 5 class Poly
16	14, 15	cfv 5888	. . . 4 class (Poly ` s )
17	13, 5, 16	crab 2916	. . 3 class { p e. (Poly ` s ) | ( (coeff ` p ) ` (deg ` p ) ) = 1 }
18	2, 4, 17	cmpt 4729	. 2 class ( s e. ~P CC |-> { p e. (Poly ` s ) | ( (coeff ` p ) ` (deg ` p ) ) = 1 } )
19	1, 18	wceq 1483	1 wff Monic = ( s e. ~P CC |-> { p e. (Poly ` s ) | ( (coeff ` p ) ` (deg ` p ) ) = 1 } )

This definition is referenced by:  elmnc  37706