Theorem deg1z

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

	Ref	Expression
Hypotheses	deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
Assertion	deg1z	$$⊢R\in \mathrm{Ring}\to D\left(\underset{\dot{}}{0}\right)=\mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
5	1	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
7	6 2 3	ply1mpl0	$$⊢\underset{\dot{}}{0}=0_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	5 6 7	mdeg0	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge R\in \mathrm{Ring}\right)\to D\left(\underset{\dot{}}{0}\right)=\mathrm{-\infty }$$
9	4 8	mpan	$$⊢R\in \mathrm{Ring}\to D\left(\underset{\dot{}}{0}\right)=\mathrm{-\infty }$$