This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1gsummul

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

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

Proof

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