Metamath Proof Explorer


Theorem isuc1p

Description: Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pval.p
|- P = ( Poly1 ` R )
uc1pval.b
|- B = ( Base ` P )
uc1pval.z
|- .0. = ( 0g ` P )
uc1pval.d
|- D = ( deg1 ` R )
uc1pval.c
|- C = ( Unic1p ` R )
uc1pval.u
|- U = ( Unit ` R )
Assertion isuc1p
|- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )

Proof

Step Hyp Ref Expression
1 uc1pval.p
 |-  P = ( Poly1 ` R )
2 uc1pval.b
 |-  B = ( Base ` P )
3 uc1pval.z
 |-  .0. = ( 0g ` P )
4 uc1pval.d
 |-  D = ( deg1 ` R )
5 uc1pval.c
 |-  C = ( Unic1p ` R )
6 uc1pval.u
 |-  U = ( Unit ` R )
7 neeq1
 |-  ( f = F -> ( f =/= .0. <-> F =/= .0. ) )
8 fveq2
 |-  ( f = F -> ( coe1 ` f ) = ( coe1 ` F ) )
9 fveq2
 |-  ( f = F -> ( D ` f ) = ( D ` F ) )
10 8 9 fveq12d
 |-  ( f = F -> ( ( coe1 ` f ) ` ( D ` f ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
11 10 eleq1d
 |-  ( f = F -> ( ( ( coe1 ` f ) ` ( D ` f ) ) e. U <-> ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )
12 7 11 anbi12d
 |-  ( f = F -> ( ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) <-> ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
13 1 2 3 4 5 6 uc1pval
 |-  C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) }
14 12 13 elrab2
 |-  ( F e. C <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
15 3anass
 |-  ( ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
16 14 15 bitr4i
 |-  ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )