| 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 ) ) ) ) |