Theorem deg1z

Description: Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		1on	⊢ 1o ∈ On
5	1	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
6		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
7	6 2 3	ply1mpl0	⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) )
8	5 6 7	mdeg0	⊢ ( ( 1o ∈ On ∧ 𝑅 ∈ Ring ) → ( 𝐷 ‘ 0 ) = -∞ )
9	4 8	mpan	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ )