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

Metamath Proof Explorer

Theorem evlsgsumadd

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

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

Proof

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