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* , < ) )