This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )