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 )