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={\mathrm{deg}}_1\left(R\right)$$
	deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
	deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	deg1n0ima	$$⊢R\in \mathrm{Ring}\to D\left[B\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
5		simpl	$$⊢\left(R\in \mathrm{Ring}\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to R\in \mathrm{Ring}$$
6		eldifi	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\in B$$
7	6	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x\in B$$
8		eldifsni	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\ne \underset{\dot{}}{0}$$
9	8	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x\ne \underset{\dot{}}{0}$$
10	1 2 3 4	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\wedge x\ne \underset{\dot{}}{0}\right)\to D\left(x\right)\in {\mathbb{N}}_0$$
11	5 7 9 10	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to D\left(x\right)\in {\mathbb{N}}_0$$
12	11	ralrimiva	$$⊢R\in \mathrm{Ring}\to \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)D\left(x\right)\in {\mathbb{N}}_0$$
13	1 2 4	deg1xrf	$$⊢D:B⟶{ℝ}^{*}$$
14		ffun	$$⊢D:B⟶{ℝ}^{*}\to \mathrm{Fun}D$$
15	13 14	ax-mp	$$⊢\mathrm{Fun}D$$
16		difss	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
17	13	fdmi	$$⊢\mathrm{dom}D=B$$
18	16 17	sseqtrri	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq \mathrm{dom}D$$
19		funimass4	$$⊢\left(\mathrm{Fun}D\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq \mathrm{dom}D\right)\to \left(D\left[B\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{N}}_0\leftrightarrow \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)D\left(x\right)\in {\mathbb{N}}_0\right)$$
20	15 18 19	mp2an	$$⊢D\left[B\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{N}}_0\leftrightarrow \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)D\left(x\right)\in {\mathbb{N}}_0$$
21	12 20	sylibr	$$⊢R\in \mathrm{Ring}\to D\left[B\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{N}}_0$$