This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )