| Step |
Hyp |
Ref |
Expression |
| 1 |
|
deg1z.d |
|- D = ( deg1 ` R ) |
| 2 |
|
deg1z.p |
|- P = ( Poly1 ` R ) |
| 3 |
|
deg1z.z |
|- .0. = ( 0g ` P ) |
| 4 |
|
deg1nn0cl.b |
|- B = ( Base ` P ) |
| 5 |
|
simpl |
|- ( ( R e. Ring /\ x e. ( B \ { .0. } ) ) -> R e. Ring ) |
| 6 |
|
eldifi |
|- ( x e. ( B \ { .0. } ) -> x e. B ) |
| 7 |
6
|
adantl |
|- ( ( R e. Ring /\ x e. ( B \ { .0. } ) ) -> x e. B ) |
| 8 |
|
eldifsni |
|- ( x e. ( B \ { .0. } ) -> x =/= .0. ) |
| 9 |
8
|
adantl |
|- ( ( R e. Ring /\ x e. ( B \ { .0. } ) ) -> x =/= .0. ) |
| 10 |
1 2 3 4
|
deg1nn0cl |
|- ( ( R e. Ring /\ x e. B /\ x =/= .0. ) -> ( D ` x ) e. NN0 ) |
| 11 |
5 7 9 10
|
syl3anc |
|- ( ( R e. Ring /\ x e. ( B \ { .0. } ) ) -> ( D ` x ) e. NN0 ) |
| 12 |
11
|
ralrimiva |
|- ( R e. Ring -> A. x e. ( B \ { .0. } ) ( D ` x ) e. NN0 ) |
| 13 |
1 2 4
|
deg1xrf |
|- D : B --> RR* |
| 14 |
|
ffun |
|- ( D : B --> RR* -> Fun D ) |
| 15 |
13 14
|
ax-mp |
|- Fun D |
| 16 |
|
difss |
|- ( B \ { .0. } ) C_ B |
| 17 |
13
|
fdmi |
|- dom D = B |
| 18 |
16 17
|
sseqtrri |
|- ( B \ { .0. } ) C_ dom D |
| 19 |
|
funimass4 |
|- ( ( Fun D /\ ( B \ { .0. } ) C_ dom D ) -> ( ( D " ( B \ { .0. } ) ) C_ NN0 <-> A. x e. ( B \ { .0. } ) ( D ` x ) e. NN0 ) ) |
| 20 |
15 18 19
|
mp2an |
|- ( ( D " ( B \ { .0. } ) ) C_ NN0 <-> A. x e. ( B \ { .0. } ) ( D ` x ) e. NN0 ) |
| 21 |
12 20
|
sylibr |
|- ( R e. Ring -> ( D " ( B \ { .0. } ) ) C_ NN0 ) |