Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evls1gsumadd Structured version   Visualization version   Unicode version

 Description: Univariate polynomial evaluation maps (additive) group sums to group sums. (Contributed by AV, 14-Sep-2019.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()

StepHypRef Expression
3 evls1gsumadd.r . . . . 5 SubRing
4 evls1gsumadd.u . . . . . 6 s
54subrgring 18011 . . . . 5 SubRing
63, 5syl 17 . . . 4
7 evls1gsumadd.w . . . . 5 Poly1
87ply1ring 18841 . . . 4
9 ringcmn 17811 . . . 4 CMnd
106, 8, 93syl 18 . . 3 CMnd
11 evls1gsumadd.s . . . . . 6
12 crngring 17791 . . . . . 6
1311, 12syl 17 . . . . 5
14 evls1gsumadd.k . . . . . 6
15 fvex 5875 . . . . . 6
1614, 15eqeltri 2525 . . . . 5
1713, 16jctir 541 . . . 4
18 evls1gsumadd.p . . . . 5 s
1918pwsring 17843 . . . 4
20 ringmnd 17789 . . . 4
2117, 19, 203syl 18 . . 3
22 nn0ex 10875 . . . . 5
2322a1i 11 . . . 4
24 evls1gsumadd.n . . . 4
2523, 24ssexd 4550 . . 3
26 evls1gsumadd.q . . . . . 6 evalSub1
2726, 14, 18, 4, 7evls1rhm 18911 . . . . 5 SubRing RingHom
2811, 3, 27syl2anc 667 . . . 4 RingHom
29 rhmghm 17953 . . . 4 RingHom
30 ghmmhm 16893 . . . 4 MndHom
3128, 29, 303syl 18 . . 3 MndHom