Metamath Proof Explorer

Definition df-uc1p

Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg . (Contributed by Stefan O'Rear, 28-Mar-2015)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuc1p 
 |-  Unic1p
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 cui 
 |-  Unit
20 6 19 cfv 
 |-  ( Unit ` r )
21 18 20 wcel 
 |-  ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r )
22 12 21 wa 
 |-  ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) )
23 22 3 8 crab 
 |-  { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) }
24 1 2 23 cmpt 
 |-  ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } )
25 0 24 wceq 
 |-  Unic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } )