Step |
Hyp |
Ref |
Expression |
1 |
|
uc1pdeg.d |
|- D = ( deg1 ` R ) |
2 |
|
uc1pdeg.c |
|- C = ( Unic1p ` R ) |
3 |
|
simpl |
|- ( ( R e. Ring /\ F e. C ) -> R e. Ring ) |
4 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
5 |
|
eqid |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) ) |
6 |
4 5 2
|
uc1pcl |
|- ( F e. C -> F e. ( Base ` ( Poly1 ` R ) ) ) |
7 |
6
|
adantl |
|- ( ( R e. Ring /\ F e. C ) -> F e. ( Base ` ( Poly1 ` R ) ) ) |
8 |
|
eqid |
|- ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) ) |
9 |
4 8 2
|
uc1pn0 |
|- ( F e. C -> F =/= ( 0g ` ( Poly1 ` R ) ) ) |
10 |
9
|
adantl |
|- ( ( R e. Ring /\ F e. C ) -> F =/= ( 0g ` ( Poly1 ` R ) ) ) |
11 |
1 4 8 5
|
deg1nn0cl |
|- ( ( R e. Ring /\ F e. ( Base ` ( Poly1 ` R ) ) /\ F =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( D ` F ) e. NN0 ) |
12 |
3 7 10 11
|
syl3anc |
|- ( ( R e. Ring /\ F e. C ) -> ( D ` F ) e. NN0 ) |