Metamath Proof Explorer

Theorem mdegfval

Description: Value of the multivariate degree function. (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 mdegfval 
|- D = ( f e. B |-> 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 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = ( I mPoly R ) )
8 7 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = P )
9 8 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = ( Base ` P ) )
10 9 3 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = B )
11 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
12 11 4 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
13 12 oveq2d 
 |-  ( r = R -> ( f supp ( 0g ` r ) ) = ( f supp .0. ) )
14 13 mpteq1d 
 |-  ( r = R -> ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) = ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) )
15 14 rneqd 
 |-  ( r = R -> ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) = ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) )
16 15 supeq1d 
 |-  ( r = R -> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) = sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) )
17 16 adantl 
 |-  ( ( i = I /\ r = R ) -> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) = sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) )
18 10 17 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) = ( f e. B |-> sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )
19 df-mdeg 
 |-  mDeg = ( i e. _V , r e. _V |-> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )
20 3 fvexi 
 |-  B e. _V
21 20 mptex 
 |-  ( f e. B |-> sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) ) e. _V
22 18 19 21 ovmpoa 
 |-  ( ( I e. _V /\ R e. _V ) -> ( I mDeg R ) = ( f e. B |-> sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )
23 6 reseq1i 
 |-  ( H |` ( f supp .0. ) ) = ( ( h e. A |-> ( CCfld gsum h ) ) |` ( f supp .0. ) )
24 suppssdm 
 |-  ( f supp .0. ) C_ dom f
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 simpr 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> f e. B )
27 2 25 3 5 26 mplelf 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> f : A --> ( Base ` R ) )
28 24 27 fssdm 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> ( f supp .0. ) C_ A )
29 28 resmptd 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> ( ( h e. A |-> ( CCfld gsum h ) ) |` ( f supp .0. ) ) = ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) )
30 23 29 syl5req 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) = ( H |` ( f supp .0. ) ) )
31 30 rneqd 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) = ran ( H |` ( f supp .0. ) ) )
32 df-ima 
 |-  ( H " ( f supp .0. ) ) = ran ( H |` ( f supp .0. ) )
33 31 32 eqtr4di 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) = ( H " ( f supp .0. ) ) )
34 33 supeq1d 
 |-  ( ( ( I e. _V /\ R e. _V ) /\ f e. B ) -> sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) = sup ( ( H " ( f supp .0. ) ) , RR* , < ) )
35 34 mpteq2dva 
 |-  ( ( I e. _V /\ R e. _V ) -> ( f e. B |-> sup ( ran ( h e. ( f supp .0. ) |-> ( CCfld gsum h ) ) , RR* , < ) ) = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) )
36 22 35 eqtrd 
 |-  ( ( I e. _V /\ R e. _V ) -> ( I mDeg R ) = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) )
37 reldmmdeg 
 |-  Rel dom mDeg
38 37 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mDeg R ) = (/) )
39 mpt0 
 |-  ( f e. (/) |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) = (/)
40 38 39 eqtr4di 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mDeg R ) = ( f e. (/) |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) )
41 reldmmpl 
 |-  Rel dom mPoly
42 41 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = (/) )
43 2 42 syl5eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> P = (/) )
44 43 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( Base ` P ) = ( Base ` (/) ) )
45 base0 
 |-  (/) = ( Base ` (/) )
46 44 3 45 3eqtr4g 
 |-  ( -. ( I e. _V /\ R e. _V ) -> B = (/) )
47 46 mpteq1d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) = ( f e. (/) |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) )
48 40 47 eqtr4d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mDeg R ) = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) ) )
49 36 48 pm2.61i 
 |-  ( I mDeg R ) = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) )
50 1 49 eqtri 
 |-  D = ( f e. B |-> sup ( ( H " ( f supp .0. ) ) , RR* , < ) )