Metamath Proof Explorer


Theorem evl1gsummul

Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019)

Ref Expression
Hypotheses evl1gsumadd.q
|- Q = ( eval1 ` R )
evl1gsumadd.k
|- K = ( Base ` R )
evl1gsumadd.w
|- W = ( Poly1 ` R )
evl1gsumadd.p
|- P = ( R ^s K )
evl1gsumadd.b
|- B = ( Base ` W )
evl1gsumadd.r
|- ( ph -> R e. CRing )
evl1gsumadd.y
|- ( ( ph /\ x e. N ) -> Y e. B )
evl1gsumadd.n
|- ( ph -> N C_ NN0 )
evl1gsummul.1
|- .1. = ( 1r ` W )
evl1gsummul.g
|- G = ( mulGrp ` W )
evl1gsummul.h
|- H = ( mulGrp ` P )
evl1gsummul.f
|- ( ph -> ( x e. N |-> Y ) finSupp .1. )
Assertion evl1gsummul
|- ( ph -> ( Q ` ( G gsum ( x e. N |-> Y ) ) ) = ( H gsum ( x e. N |-> ( Q ` Y ) ) ) )

Proof

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