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

Metamath Proof Explorer

Theorem uc1pdeg

Description: Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
uc1pdeg.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
Assertion uc1pdeg ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 uc1pdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 uc1pdeg.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
3 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ) → 𝑅 ∈ Ring )
4 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
6 4 5 2 uc1pcl ⊢ ( 𝐹 ∈ 𝐶 → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
7 6 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ) → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
8 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
9 4 8 2 uc1pn0 ⊢ ( 𝐹 ∈ 𝐶 → 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
10 9 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ) → 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
11 1 4 8 5 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
12 3 7 10 11 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )