Metamath Proof Explorer


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 )