Step |
Hyp |
Ref |
Expression |
1 |
|
mdegaddle.y |
|- Y = ( I mPoly R ) |
2 |
|
mdegaddle.d |
|- D = ( I mDeg R ) |
3 |
|
mdegaddle.i |
|- ( ph -> I e. V ) |
4 |
|
mdegaddle.r |
|- ( ph -> R e. Ring ) |
5 |
|
mdegvsca.b |
|- B = ( Base ` Y ) |
6 |
|
mdegvsca.e |
|- E = ( RLReg ` R ) |
7 |
|
mdegvsca.p |
|- .x. = ( .s ` Y ) |
8 |
|
mdegvsca.f |
|- ( ph -> F e. E ) |
9 |
|
mdegvsca.g |
|- ( ph -> G e. B ) |
10 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
11 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
12 |
|
eqid |
|- { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |
13 |
6 10
|
rrgss |
|- E C_ ( Base ` R ) |
14 |
13 8
|
sselid |
|- ( ph -> F e. ( Base ` R ) ) |
15 |
1 7 10 5 11 12 14 9
|
mplvsca |
|- ( ph -> ( F .x. G ) = ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) ) |
16 |
15
|
oveq1d |
|- ( ph -> ( ( F .x. G ) supp ( 0g ` R ) ) = ( ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) supp ( 0g ` R ) ) ) |
17 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
18 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
19 |
18
|
rabex |
|- { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V |
20 |
19
|
a1i |
|- ( ph -> { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V ) |
21 |
1 10 5 12 9
|
mplelf |
|- ( ph -> G : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> ( Base ` R ) ) |
22 |
6 10 11 17 20 4 8 21
|
rrgsupp |
|- ( ph -> ( ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) supp ( 0g ` R ) ) = ( G supp ( 0g ` R ) ) ) |
23 |
16 22
|
eqtrd |
|- ( ph -> ( ( F .x. G ) supp ( 0g ` R ) ) = ( G supp ( 0g ` R ) ) ) |
24 |
23
|
imaeq2d |
|- ( ph -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) = ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) ) |
25 |
24
|
supeq1d |
|- ( ph -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) ) |
26 |
1 3 4
|
mpllmodd |
|- ( ph -> Y e. LMod ) |
27 |
1 3 4
|
mplsca |
|- ( ph -> R = ( Scalar ` Y ) ) |
28 |
27
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) ) |
29 |
14 28
|
eleqtrd |
|- ( ph -> F e. ( Base ` ( Scalar ` Y ) ) ) |
30 |
|
eqid |
|- ( Scalar ` Y ) = ( Scalar ` Y ) |
31 |
|
eqid |
|- ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) ) |
32 |
5 30 7 31
|
lmodvscl |
|- ( ( Y e. LMod /\ F e. ( Base ` ( Scalar ` Y ) ) /\ G e. B ) -> ( F .x. G ) e. B ) |
33 |
26 29 9 32
|
syl3anc |
|- ( ph -> ( F .x. G ) e. B ) |
34 |
|
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 ) ) |
35 |
2 1 5 17 12 34
|
mdegval |
|- ( ( F .x. G ) e. B -> ( D ` ( F .x. G ) ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) ) |
36 |
33 35
|
syl |
|- ( ph -> ( D ` ( F .x. G ) ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) ) |
37 |
2 1 5 17 12 34
|
mdegval |
|- ( G e. B -> ( D ` G ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) ) |
38 |
9 37
|
syl |
|- ( ph -> ( D ` G ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) ) |
39 |
25 36 38
|
3eqtr4d |
|- ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) ) |