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 ) ) } )