Step |
Hyp |
Ref |
Expression |
1 |
|
mdegxrcl.d |
|- D = ( I mDeg R ) |
2 |
|
mdegxrcl.p |
|- P = ( I mPoly R ) |
3 |
|
mdegxrcl.b |
|- B = ( Base ` P ) |
4 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
5 |
|
eqid |
|- { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |
6 |
|
eqid |
|- ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) = ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) |
7 |
1 2 3 4 5 6
|
mdegval |
|- ( F e. B -> ( D ` F ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) ) |
8 |
|
imassrn |
|- ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) |
9 |
5 6
|
tdeglem1 |
|- ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> NN0 |
10 |
|
frn |
|- ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> NN0 -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ NN0 ) |
11 |
9 10
|
mp1i |
|- ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ NN0 ) |
12 |
|
nn0ssre |
|- NN0 C_ RR |
13 |
|
ressxr |
|- RR C_ RR* |
14 |
12 13
|
sstri |
|- NN0 C_ RR* |
15 |
11 14
|
sstrdi |
|- ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ RR* ) |
16 |
8 15
|
sstrid |
|- ( F e. B -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* ) |
17 |
|
supxrcl |
|- ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. RR* ) |
18 |
16 17
|
syl |
|- ( F e. B -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. RR* ) |
19 |
7 18
|
eqeltrd |
|- ( F e. B -> ( D ` F ) e. RR* ) |