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

Metamath Proof Explorer

Theorem mdegval

Description: Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by AV, 25-Jun-2019)

Ref Expression
Hypotheses mdegval.d 
|- D = ( I mDeg R )
mdegval.p 
|- P = ( I mPoly R )
mdegval.b 
|- B = ( Base ` P )
mdegval.z 
|- .0. = ( 0g ` R )
mdegval.a 
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
mdegval.h 
|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion mdegval 
|- ( F e. B -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 mdegval.d 
 |-  D = ( I mDeg R )
2 mdegval.p 
 |-  P = ( I mPoly R )
3 mdegval.b 
 |-  B = ( Base ` P )
4 mdegval.z 
 |-  .0. = ( 0g ` R )
5 mdegval.a 
 |-  A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
6 mdegval.h 
 |-  H = ( h e. A |-> ( CCfld gsum h ) )
7 oveq1 
 |-  ( f = F -> ( f supp .0. ) = ( F supp .0. ) )
8 7 imaeq2d 
 |-  ( f = F -> ( H " ( f supp .0. ) ) = ( H " ( F supp .0. ) ) )
9 8 supeq1d 
 |-  ( f = F -> sup ( ( H " ( f supp .0. ) ) , RR* , < ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
10 1 2 3 4 5 6 mdegfval 
 |-  D = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) )
11 xrltso 
 |-  < Or RR*
12 11 supex 
 |-  sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. _V
13 9 10 12 fvmpt 
 |-  ( F e. B -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )