Step |
Hyp |
Ref |
Expression |
1 |
|
evlsgsumadd.q |
|- Q = ( ( I evalSub S ) ` R ) |
2 |
|
evlsgsumadd.w |
|- W = ( I mPoly U ) |
3 |
|
evlsgsumadd.0 |
|- .0. = ( 0g ` W ) |
4 |
|
evlsgsumadd.u |
|- U = ( S |`s R ) |
5 |
|
evlsgsumadd.p |
|- P = ( S ^s ( K ^m I ) ) |
6 |
|
evlsgsumadd.k |
|- K = ( Base ` S ) |
7 |
|
evlsgsumadd.b |
|- B = ( Base ` W ) |
8 |
|
evlsgsumadd.i |
|- ( ph -> I e. V ) |
9 |
|
evlsgsumadd.s |
|- ( ph -> S e. CRing ) |
10 |
|
evlsgsumadd.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
11 |
|
evlsgsumadd.y |
|- ( ( ph /\ x e. N ) -> Y e. B ) |
12 |
|
evlsgsumadd.n |
|- ( ph -> N C_ NN0 ) |
13 |
|
evlsgsumadd.f |
|- ( ph -> ( x e. N |-> Y ) finSupp .0. ) |
14 |
4
|
subrgring |
|- ( R e. ( SubRing ` S ) -> U e. Ring ) |
15 |
10 14
|
syl |
|- ( ph -> U e. Ring ) |
16 |
2 8 15
|
mplringd |
|- ( ph -> W e. Ring ) |
17 |
|
ringcmn |
|- ( W e. Ring -> W e. CMnd ) |
18 |
16 17
|
syl |
|- ( ph -> W e. CMnd ) |
19 |
|
crngring |
|- ( S e. CRing -> S e. Ring ) |
20 |
9 19
|
syl |
|- ( ph -> S e. Ring ) |
21 |
|
ovex |
|- ( K ^m I ) e. _V |
22 |
20 21
|
jctir |
|- ( ph -> ( S e. Ring /\ ( K ^m I ) e. _V ) ) |
23 |
5
|
pwsring |
|- ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> P e. Ring ) |
24 |
|
ringmnd |
|- ( P e. Ring -> P e. Mnd ) |
25 |
22 23 24
|
3syl |
|- ( ph -> P e. Mnd ) |
26 |
|
nn0ex |
|- NN0 e. _V |
27 |
26
|
a1i |
|- ( ph -> NN0 e. _V ) |
28 |
27 12
|
ssexd |
|- ( ph -> N e. _V ) |
29 |
1 2 4 5 6
|
evlsrhm |
|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom P ) ) |
30 |
8 9 10 29
|
syl3anc |
|- ( ph -> Q e. ( W RingHom P ) ) |
31 |
|
rhmghm |
|- ( Q e. ( W RingHom P ) -> Q e. ( W GrpHom P ) ) |
32 |
|
ghmmhm |
|- ( Q e. ( W GrpHom P ) -> Q e. ( W MndHom P ) ) |
33 |
30 31 32
|
3syl |
|- ( ph -> Q e. ( W MndHom P ) ) |
34 |
7 3 18 25 28 33 11 13
|
gsummptmhm |
|- ( ph -> ( P gsum ( x e. N |-> ( Q ` Y ) ) ) = ( Q ` ( W gsum ( x e. N |-> Y ) ) ) ) |
35 |
34
|
eqcomd |
|- ( ph -> ( Q ` ( W gsum ( x e. N |-> Y ) ) ) = ( P gsum ( x e. N |-> ( Q ` Y ) ) ) ) |