Theorem deg1n0ima

Description: Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	|- D = ( deg1 ` R )
	deg1z.p	|- P = ( Poly1 ` R )
	deg1z.z	|- .0. = ( 0g ` P )
	deg1nn0cl.b	|- B = ( Base ` P )
Assertion	deg1n0ima	|- ( R e. Ring -> ( D " ( B \ { .0. } ) ) C_ NN0 )

Proof

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 )