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 ˙ = 0 W
evlsgsumadd.u U = S 𝑠 R
evlsgsumadd.p P = S 𝑠 K I
evlsgsumadd.k K = Base S
evlsgsumadd.b B = Base W
evlsgsumadd.i φ I V
evlsgsumadd.s φ S CRing
evlsgsumadd.r φ R SubRing S
evlsgsumadd.y φ x N Y B
evlsgsumadd.n φ N 0
evlsgsumadd.f φ finSupp 0 ˙ x N Y
Assertion evlsgsumadd φ Q W x N Y = P x 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 ˙ = 0 W
4 evlsgsumadd.u U = S 𝑠 R
5 evlsgsumadd.p P = S 𝑠 K I
6 evlsgsumadd.k K = Base S
7 evlsgsumadd.b B = Base W
8 evlsgsumadd.i φ I V
9 evlsgsumadd.s φ S CRing
10 evlsgsumadd.r φ R SubRing S
11 evlsgsumadd.y φ x N Y B
12 evlsgsumadd.n φ N 0
13 evlsgsumadd.f φ finSupp 0 ˙ x N Y
14 4 subrgring R SubRing S U Ring
15 10 14 syl φ U Ring
16 2 8 15 mplringd φ W Ring
17 ringcmn W Ring W CMnd
18 16 17 syl φ W CMnd
19 crngring S CRing S Ring
20 9 19 syl φ S Ring
21 ovex K I V
22 20 21 jctir φ S Ring K I V
23 5 pwsring S Ring K I V P Ring
24 ringmnd P Ring P Mnd
25 22 23 24 3syl φ P Mnd
26 nn0ex 0 V
27 26 a1i φ 0 V
28 27 12 ssexd φ N V
29 1 2 4 5 6 evlsrhm I V S CRing R SubRing S Q W RingHom P
30 8 9 10 29 syl3anc φ Q W RingHom P
31 rhmghm Q W RingHom P Q W GrpHom P
32 ghmmhm Q W GrpHom P Q W MndHom P
33 30 31 32 3syl φ Q W MndHom P
34 7 3 18 25 28 33 11 13 gsummptmhm φ P x N Q Y = Q W x N Y
35 34 eqcomd φ Q W x N Y = P x N Q Y