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