Metamath Proof Explorer

Theorem evlsgsummul

Description: Polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by SN, 13-Feb-2024)

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

Proof

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