Metamath Proof Explorer


Theorem uc1pn0

Description: Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pn0.p
|- P = ( Poly1 ` R )
uc1pn0.z
|- .0. = ( 0g ` P )
uc1pn0.c
|- C = ( Unic1p ` R )
Assertion uc1pn0
|- ( F e. C -> F =/= .0. )

Proof

Step Hyp Ref Expression
1 uc1pn0.p
 |-  P = ( Poly1 ` R )
2 uc1pn0.z
 |-  .0. = ( 0g ` P )
3 uc1pn0.c
 |-  C = ( Unic1p ` R )
4 eqid
 |-  ( Base ` P ) = ( Base ` P )
5 eqid
 |-  ( deg1 ` R ) = ( deg1 ` R )
6 eqid
 |-  ( Unit ` R ) = ( Unit ` R )
7 1 4 2 5 3 6 isuc1p
 |-  ( F e. C <-> ( F e. ( Base ` P ) /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) ) )
8 7 simp2bi
 |-  ( F e. C -> F =/= .0. )