Metamath Proof Explorer


Theorem evls1gsumadd

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

Ref Expression
Hypotheses evls1gsumadd.q Q = S evalSub 1 R
evls1gsumadd.k K = Base S
evls1gsumadd.w W = Poly 1 U
evls1gsumadd.0 0 ˙ = 0 W
evls1gsumadd.u U = S 𝑠 R
evls1gsumadd.p P = S 𝑠 K
evls1gsumadd.b B = Base W
evls1gsumadd.s φ S CRing
evls1gsumadd.r φ R SubRing S
evls1gsumadd.y φ x N Y B
evls1gsumadd.n φ N 0
evls1gsumadd.f φ finSupp 0 ˙ x N Y
Assertion evls1gsumadd φ Q W x N Y = P x N Q Y

Proof

Step Hyp Ref Expression
1 evls1gsumadd.q Q = S evalSub 1 R
2 evls1gsumadd.k K = Base S
3 evls1gsumadd.w W = Poly 1 U
4 evls1gsumadd.0 0 ˙ = 0 W
5 evls1gsumadd.u U = S 𝑠 R
6 evls1gsumadd.p P = S 𝑠 K
7 evls1gsumadd.b B = Base W
8 evls1gsumadd.s φ S CRing
9 evls1gsumadd.r φ R SubRing S
10 evls1gsumadd.y φ x N Y B
11 evls1gsumadd.n φ N 0
12 evls1gsumadd.f φ finSupp 0 ˙ x N Y
13 5 subrgring R SubRing S U Ring
14 3 ply1ring U Ring W Ring
15 ringcmn W Ring W CMnd
16 9 13 14 15 4syl φ W CMnd
17 crngring S CRing S Ring
18 8 17 syl φ S Ring
19 2 fvexi K V
20 18 19 jctir φ S Ring K V
21 6 pwsring S Ring K V P Ring
22 ringmnd P Ring P Mnd
23 20 21 22 3syl φ P Mnd
24 nn0ex 0 V
25 24 a1i φ 0 V
26 25 11 ssexd φ N V
27 1 2 6 5 3 evls1rhm S CRing R SubRing S Q W RingHom P
28 8 9 27 syl2anc φ Q W RingHom P
29 rhmghm Q W RingHom P Q W GrpHom P
30 ghmmhm Q W GrpHom P Q W MndHom P
31 28 29 30 3syl φ Q W MndHom P
32 7 4 16 23 26 31 10 12 gsummptmhm φ P x N Q Y = Q W x N Y
33 32 eqcomd φ Q W x N Y = P x N Q Y