Step |
Hyp |
Ref |
Expression |
1 |
|
evl1gsumadd.q |
|- Q = ( eval1 ` R ) |
2 |
|
evl1gsumadd.k |
|- K = ( Base ` R ) |
3 |
|
evl1gsumadd.w |
|- W = ( Poly1 ` R ) |
4 |
|
evl1gsumadd.p |
|- P = ( R ^s K ) |
5 |
|
evl1gsumadd.b |
|- B = ( Base ` W ) |
6 |
|
evl1gsumadd.r |
|- ( ph -> R e. CRing ) |
7 |
|
evl1gsumadd.y |
|- ( ( ph /\ x e. N ) -> Y e. B ) |
8 |
|
evl1gsumadd.n |
|- ( ph -> N C_ NN0 ) |
9 |
|
evl1gsummul.1 |
|- .1. = ( 1r ` W ) |
10 |
|
evl1gsummul.g |
|- G = ( mulGrp ` W ) |
11 |
|
evl1gsummul.h |
|- H = ( mulGrp ` P ) |
12 |
|
evl1gsummul.f |
|- ( ph -> ( x e. N |-> Y ) finSupp .1. ) |
13 |
10 5
|
mgpbas |
|- B = ( Base ` G ) |
14 |
10 9
|
ringidval |
|- .1. = ( 0g ` G ) |
15 |
3
|
ply1crng |
|- ( R e. CRing -> W e. CRing ) |
16 |
10
|
crngmgp |
|- ( W e. CRing -> G e. CMnd ) |
17 |
6 15 16
|
3syl |
|- ( ph -> G e. CMnd ) |
18 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
19 |
6 18
|
syl |
|- ( ph -> R e. Ring ) |
20 |
2
|
fvexi |
|- K e. _V |
21 |
19 20
|
jctir |
|- ( ph -> ( R e. Ring /\ K e. _V ) ) |
22 |
4
|
pwsring |
|- ( ( R e. Ring /\ K e. _V ) -> P e. Ring ) |
23 |
11
|
ringmgp |
|- ( P e. Ring -> H e. Mnd ) |
24 |
21 22 23
|
3syl |
|- ( ph -> H e. Mnd ) |
25 |
|
nn0ex |
|- NN0 e. _V |
26 |
25
|
a1i |
|- ( ph -> NN0 e. _V ) |
27 |
26 8
|
ssexd |
|- ( ph -> N e. _V ) |
28 |
1 3 4 2
|
evl1rhm |
|- ( R e. CRing -> Q e. ( W RingHom P ) ) |
29 |
10 11
|
rhmmhm |
|- ( Q e. ( W RingHom P ) -> Q e. ( G MndHom H ) ) |
30 |
6 28 29
|
3syl |
|- ( ph -> Q e. ( G MndHom H ) ) |
31 |
13 14 17 24 27 30 7 12
|
gsummptmhm |
|- ( ph -> ( H gsum ( x e. N |-> ( Q ` Y ) ) ) = ( Q ` ( G gsum ( x e. N |-> Y ) ) ) ) |
32 |
31
|
eqcomd |
|- ( ph -> ( Q ` ( G gsum ( x e. N |-> Y ) ) ) = ( H gsum ( x e. N |-> ( Q ` Y ) ) ) ) |