| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlsvvvallem2.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
| 2 |
|
evlsvvvallem2.p |
|- P = ( I mPoly U ) |
| 3 |
|
evlsvvvallem2.u |
|- U = ( S |`s R ) |
| 4 |
|
evlsvvvallem2.b |
|- B = ( Base ` P ) |
| 5 |
|
evlsvvvallem2.k |
|- K = ( Base ` S ) |
| 6 |
|
evlsvvvallem2.m |
|- M = ( mulGrp ` S ) |
| 7 |
|
evlsvvvallem2.w |
|- .^ = ( .g ` M ) |
| 8 |
|
evlsvvvallem2.x |
|- .x. = ( .r ` S ) |
| 9 |
|
evlsvvvallem2.i |
|- ( ph -> I e. V ) |
| 10 |
|
evlsvvvallem2.s |
|- ( ph -> S e. CRing ) |
| 11 |
|
evlsvvvallem2.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 12 |
|
evlsvvvallem2.f |
|- ( ph -> F e. B ) |
| 13 |
|
evlsvvvallem2.a |
|- ( ph -> A e. ( K ^m I ) ) |
| 14 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
| 15 |
1 14
|
rabex2 |
|- D e. _V |
| 16 |
15
|
mptex |
|- ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) e. _V |
| 17 |
16
|
a1i |
|- ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) e. _V ) |
| 18 |
|
fvexd |
|- ( ph -> ( 0g ` S ) e. _V ) |
| 19 |
|
funmpt |
|- Fun ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |
| 20 |
19
|
a1i |
|- ( ph -> Fun ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) |
| 21 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
| 22 |
2 4 21 12
|
mplelsfi |
|- ( ph -> F finSupp ( 0g ` U ) ) |
| 23 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
| 24 |
2 23 4 1 12
|
mplelf |
|- ( ph -> F : D --> ( Base ` U ) ) |
| 25 |
|
ssidd |
|- ( ph -> ( F supp ( 0g ` U ) ) C_ ( F supp ( 0g ` U ) ) ) |
| 26 |
|
fvexd |
|- ( ph -> ( 0g ` U ) e. _V ) |
| 27 |
24 25 12 26
|
suppssrg |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` U ) ) |
| 28 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
| 29 |
3 28
|
subrg0 |
|- ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) ) |
| 30 |
11 29
|
syl |
|- ( ph -> ( 0g ` S ) = ( 0g ` U ) ) |
| 31 |
30
|
eqcomd |
|- ( ph -> ( 0g ` U ) = ( 0g ` S ) ) |
| 32 |
31
|
adantr |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( 0g ` U ) = ( 0g ` S ) ) |
| 33 |
27 32
|
eqtrd |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` S ) ) |
| 34 |
33
|
oveq1d |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |
| 35 |
10
|
crngringd |
|- ( ph -> S e. Ring ) |
| 36 |
35
|
adantr |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> S e. Ring ) |
| 37 |
|
eldifi |
|- ( b e. ( D \ ( F supp ( 0g ` U ) ) ) -> b e. D ) |
| 38 |
9
|
adantr |
|- ( ( ph /\ b e. D ) -> I e. V ) |
| 39 |
10
|
adantr |
|- ( ( ph /\ b e. D ) -> S e. CRing ) |
| 40 |
13
|
adantr |
|- ( ( ph /\ b e. D ) -> A e. ( K ^m I ) ) |
| 41 |
|
simpr |
|- ( ( ph /\ b e. D ) -> b e. D ) |
| 42 |
1 5 6 7 38 39 40 41
|
evlsvvvallem |
|- ( ( ph /\ b e. D ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K ) |
| 43 |
37 42
|
sylan2 |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K ) |
| 44 |
5 8 28 36 43
|
ringlzd |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( 0g ` S ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) ) |
| 45 |
34 44
|
eqtrd |
|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) ) |
| 46 |
15
|
a1i |
|- ( ph -> D e. _V ) |
| 47 |
45 46
|
suppss2 |
|- ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) supp ( 0g ` S ) ) C_ ( F supp ( 0g ` U ) ) ) |
| 48 |
17 18 20 22 47
|
fsuppsssuppgd |
|- ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` S ) ) |