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 = ( deg1 ` R )
Assertion	deg1fval	|- D = ( 1o mDeg R )

Proof

Step	Hyp	Ref	Expression
1		deg1fval.d	|- D = ( deg1 ` R )
2		oveq2	|- ( r = R -> ( 1o mDeg r ) = ( 1o mDeg R ) )
3		df-deg1	|- deg1 = ( r e. _V |-> ( 1o mDeg r ) )
4		ovex	|- ( 1o mDeg R ) e. _V
5	2 3 4	fvmpt	|- ( R e. _V -> ( deg1 ` R ) = ( 1o mDeg R ) )
6		fvprc	|- ( -. R e. _V -> ( deg1 ` R ) = (/) )
7		reldmmdeg	|- Rel dom mDeg
8	7	ovprc2	|- ( -. R e. _V -> ( 1o mDeg R ) = (/) )
9	6 8	eqtr4d	|- ( -. R e. _V -> ( deg1 ` R ) = ( 1o mDeg R ) )
10	5 9	pm2.61i	|- ( deg1 ` R ) = ( 1o mDeg R )
11	1 10	eqtri	|- D = ( 1o mDeg R )