| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlsmhpvvval.q |
|- Q = ( ( I evalSub S ) ` R ) |
| 2 |
|
evlsmhpvvval.p |
|- H = ( I mHomP U ) |
| 3 |
|
evlsmhpvvval.u |
|- U = ( S |`s R ) |
| 4 |
|
evlsmhpvvval.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
| 5 |
|
evlsmhpvvval.g |
|- G = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } |
| 6 |
|
evlsmhpvvval.k |
|- K = ( Base ` S ) |
| 7 |
|
evlsmhpvvval.m |
|- M = ( mulGrp ` S ) |
| 8 |
|
evlsmhpvvval.w |
|- .^ = ( .g ` M ) |
| 9 |
|
evlsmhpvvval.x |
|- .x. = ( .r ` S ) |
| 10 |
|
evlsmhpvvval.s |
|- ( ph -> S e. CRing ) |
| 11 |
|
evlsmhpvvval.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 12 |
|
evlsmhpvvval.f |
|- ( ph -> F e. ( H ` N ) ) |
| 13 |
|
evlsmhpvvval.a |
|- ( ph -> A e. ( K ^m I ) ) |
| 14 |
|
eqid |
|- ( I mPoly U ) = ( I mPoly U ) |
| 15 |
|
eqid |
|- ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) ) |
| 16 |
|
reldmmhp |
|- Rel dom mHomP |
| 17 |
16 2 12
|
elfvov1 |
|- ( ph -> I e. _V ) |
| 18 |
2 14 15 12
|
mhpmpl |
|- ( ph -> F e. ( Base ` ( I mPoly U ) ) ) |
| 19 |
1 14 15 3 4 6 7 8 9 17 10 11 18 13
|
evlsvvval |
|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |
| 20 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
| 21 |
10
|
crngringd |
|- ( ph -> S e. Ring ) |
| 22 |
21
|
ringcmnd |
|- ( ph -> S e. CMnd ) |
| 23 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
| 24 |
4 23
|
rabex2 |
|- D e. _V |
| 25 |
24
|
a1i |
|- ( ph -> D e. _V ) |
| 26 |
21
|
adantr |
|- ( ( ph /\ b e. D ) -> S e. Ring ) |
| 27 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
| 28 |
14 27 15 4 18
|
mplelf |
|- ( ph -> F : D --> ( Base ` U ) ) |
| 29 |
3
|
subrgbas |
|- ( R e. ( SubRing ` S ) -> R = ( Base ` U ) ) |
| 30 |
6
|
subrgss |
|- ( R e. ( SubRing ` S ) -> R C_ K ) |
| 31 |
29 30
|
eqsstrrd |
|- ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K ) |
| 32 |
11 31
|
syl |
|- ( ph -> ( Base ` U ) C_ K ) |
| 33 |
28 32
|
fssd |
|- ( ph -> F : D --> K ) |
| 34 |
33
|
ffvelcdmda |
|- ( ( ph /\ b e. D ) -> ( F ` b ) e. K ) |
| 35 |
17
|
adantr |
|- ( ( ph /\ b e. D ) -> I e. _V ) |
| 36 |
10
|
adantr |
|- ( ( ph /\ b e. D ) -> S e. CRing ) |
| 37 |
13
|
adantr |
|- ( ( ph /\ b e. D ) -> A e. ( K ^m I ) ) |
| 38 |
|
simpr |
|- ( ( ph /\ b e. D ) -> b e. D ) |
| 39 |
4 6 7 8 35 36 37 38
|
evlsvvvallem |
|- ( ( ph /\ b e. D ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K ) |
| 40 |
6 9 26 34 39
|
ringcld |
|- ( ( ph /\ b e. D ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) e. K ) |
| 41 |
40
|
fmpttd |
|- ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) : D --> K ) |
| 42 |
3 20
|
subrg0 |
|- ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) ) |
| 43 |
11 42
|
syl |
|- ( ph -> ( 0g ` S ) = ( 0g ` U ) ) |
| 44 |
43
|
oveq2d |
|- ( ph -> ( F supp ( 0g ` S ) ) = ( F supp ( 0g ` U ) ) ) |
| 45 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
| 46 |
2 45 4 12
|
mhpdeg |
|- ( ph -> ( F supp ( 0g ` U ) ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) |
| 47 |
46 5
|
sseqtrrdi |
|- ( ph -> ( F supp ( 0g ` U ) ) C_ G ) |
| 48 |
44 47
|
eqsstrd |
|- ( ph -> ( F supp ( 0g ` S ) ) C_ G ) |
| 49 |
|
fvexd |
|- ( ph -> ( 0g ` S ) e. _V ) |
| 50 |
33 48 25 49
|
suppssr |
|- ( ( ph /\ b e. ( D \ G ) ) -> ( F ` b ) = ( 0g ` S ) ) |
| 51 |
50
|
oveq1d |
|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |
| 52 |
21
|
adantr |
|- ( ( ph /\ b e. ( D \ G ) ) -> S e. Ring ) |
| 53 |
|
eldifi |
|- ( b e. ( D \ G ) -> b e. D ) |
| 54 |
53 39
|
sylan2 |
|- ( ( ph /\ b e. ( D \ G ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K ) |
| 55 |
6 9 20 52 54
|
ringlzd |
|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) ) |
| 56 |
51 55
|
eqtrd |
|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) ) |
| 57 |
56 25
|
suppss2 |
|- ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) supp ( 0g ` S ) ) C_ G ) |
| 58 |
4 14 3 15 6 7 8 9 17 10 11 18 13
|
evlsvvvallem2 |
|- ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) finSupp ( 0g ` S ) ) |
| 59 |
6 20 22 25 41 57 58
|
gsumres |
|- ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |
| 60 |
5
|
ssrab3 |
|- G C_ D |
| 61 |
60
|
a1i |
|- ( ph -> G C_ D ) |
| 62 |
61
|
resmptd |
|- ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) = ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 63 |
62
|
oveq2d |
|- ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) ) = ( S gsum ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |
| 64 |
19 59 63
|
3eqtr2d |
|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |