Definition df-mon1 23890

Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)

Assertion

Ref	Expression
df-mon1	|- Monic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )

Distinct variable group:   f, r

Detailed syntax breakdown of Definition df-mon1

Step	Hyp	Ref	Expression
1		cmn1 23885	. 2 class Monic1p
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vf	. . . . . . 7 setvar f
5	4	cv 1482	. . . . . 6 class f
6	2	cv 1482	. . . . . . . 8 class r
7		cpl1 19547	. . . . . . . 8 class Poly1
8	6, 7	cfv 5888	. . . . . . 7 class (Poly1 ` r )
9		c0g 16100	. . . . . . 7 class 0g
10	8, 9	cfv 5888	. . . . . 6 class ( 0g ` (Poly1 ` r ) )
11	5, 10	wne 2794	. . . . 5 wff f =/= ( 0g ` (Poly1 ` r ) )
12		cdg1 23814	. . . . . . . . 9 class deg1
13	6, 12	cfv 5888	. . . . . . . 8 class ( deg1 ` r )
14	5, 13	cfv 5888	. . . . . . 7 class ( ( deg1 ` r ) ` f )
15		cco1 19548	. . . . . . . 8 class coe1
16	5, 15	cfv 5888	. . . . . . 7 class (coe1 ` f )
17	14, 16	cfv 5888	. . . . . 6 class ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) )
18		cur 18501	. . . . . . 7 class 1r
19	6, 18	cfv 5888	. . . . . 6 class ( 1r ` r )
20	17, 19	wceq 1483	. . . . 5 wff ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r )
21	11, 20	wa 384	. . . 4 wff ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) )
22		cbs 15857	. . . . 5 class Base
23	8, 22	cfv 5888	. . . 4 class ( Base ` (Poly1 ` r ) )
24	21, 4, 23	crab 2916	. . 3 class { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) }
25	2, 3, 24	cmpt 4729	. 2 class ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )
26	1, 25	wceq 1483	1 wff Monic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )

This definition is referenced by:  mon1pval  23901