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	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	deg1n0ima	⊢ ( 𝑅 ∈ Ring → ( 𝐷 “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
6		eldifi	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
7	6	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
8		eldifsni	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ≠ 0 )
9	8	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ≠ 0 )
10	1 2 3 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
11	5 7 9 10	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
12	11	ralrimiva	⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
13	1 2 4	deg1xrf	⊢ 𝐷 : 𝐵 ⟶ ℝ*
14		ffun	⊢ ( 𝐷 : 𝐵 ⟶ ℝ* → Fun 𝐷 )
15	13 14	ax-mp	⊢ Fun 𝐷
16		difss	⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
17	13	fdmi	⊢ dom 𝐷 = 𝐵
18	16 17	sseqtrri	⊢ ( 𝐵 ∖ { 0 } ) ⊆ dom 𝐷
19		funimass4	⊢ ( ( Fun 𝐷 ∧ ( 𝐵 ∖ { 0 } ) ⊆ dom 𝐷 ) → ( ( 𝐷 “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 ) )
20	15 18 19	mp2an	⊢ ( ( 𝐷 “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ( 𝐷 ‘ 𝑥 ) ∈ ℕ0 )
21	12 20	sylibr	⊢ ( 𝑅 ∈ Ring → ( 𝐷 “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 )