Metamath Proof Explorer

Definition df-mon1

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmn1 
 |-  Monic1p
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vf 
 |-  f
4 cbs 
 |-  Base
5 cpl1 
 |-  Poly1
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( Poly1 ` r )
8 7 4 cfv 
 |-  ( Base ` ( Poly1 ` r ) )
9 3 cv 
 |-  f
10 c0g 
 |-  0g
11 7 10 cfv 
 |-  ( 0g ` ( Poly1 ` r ) )
12 9 11 wne 
 |-  f =/= ( 0g ` ( Poly1 ` r ) )
13 cco1 
 |-  coe1
14 9 13 cfv 
 |-  ( coe1 ` f )
15 cdg1 
 |-  deg1
16 6 15 cfv 
 |-  ( deg1 ` r )
17 9 16 cfv 
 |-  ( ( deg1 ` r ) ` f )
18 17 14 cfv 
 |-  ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) )
19 cur 
 |-  1r
20 6 19 cfv 
 |-  ( 1r ` r )
21 18 20 wceq 
 |-  ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r )
22 12 21 wa 
 |-  ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) )
23 22 3 8 crab 
 |-  { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) }
24 1 2 23 cmpt 
 |-  ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )
25 0 24 wceq 
 |-  Monic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )