Theorem deg1fval

Description: Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypothesis	deg1fval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
Assertion	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$

Proof

Step	Hyp	Ref	Expression
1		deg1fval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		oveq2	$$⊢r=R\to 1_{𝑜}\mathrm{mDeg}r=1_{𝑜}\mathrm{mDeg}R$$
3		df-deg1	$$⊢{\mathrm{deg}}_1=\left(r\in \mathrm{V}⟼1_{𝑜}\mathrm{mDeg}r\right)$$
4		ovex	$$⊢1_{𝑜}\mathrm{mDeg}R\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢R\in \mathrm{V}\to {\mathrm{deg}}_1\left(R\right)=1_{𝑜}\mathrm{mDeg}R$$
6		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{deg}}_1\left(R\right)=\varnothing$$
7		reldmmdeg	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mDeg}$$
8	7	ovprc2	$$⊢\neg R\in \mathrm{V}\to 1_{𝑜}\mathrm{mDeg}R=\varnothing$$
9	6 8	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{deg}}_1\left(R\right)=1_{𝑜}\mathrm{mDeg}R$$
10	5 9	pm2.61i	$$⊢{\mathrm{deg}}_1\left(R\right)=1_{𝑜}\mathrm{mDeg}R$$
11	1 10	eqtri	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$