Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evls1gsumadd Structured 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
54subrgrng 17212 . . . . 5 SubRing
63, 5syl 16 . . . 4
7 evls1gsumadd.w . . . . 5 Poly1
87ply1rng 18057 . . . 4
9 rngcmn 17013 . . . 4 CMnd
106, 8, 93syl 20 . . 3 CMnd
11 evls1gsumadd.s . . . . . 6
12 crngrng 16993 . . . . . 6
1311, 12syl 16 . . . . 5
14 evls1gsumadd.k . . . . . . 7
15 fvex 5874 . . . . . . 7
1614, 15eqeltri 2551 . . . . . 6
1716a1i 11 . . . . 5
1813, 17jca 532 . . . 4
19 evls1gsumadd.p . . . . 5 s
2019pwsrng 17045 . . . 4
21 rngmnd 16992 . . . 4
2218, 20, 213syl 20 . . 3
23 nn0ex 10797 . . . . 5
2423a1i 11 . . . 4
25 evls1gsumadd.n . . . 4
2624, 25ssexd 4594 . . 3
27 evls1gsumadd.q . . . . . 6 evalSub1
2827, 14, 19, 4, 7evls1rhm 18127 . . . . 5 SubRing RingHom
2911, 3, 28syl2anc 661 . . . 4 RingHom
30 rhmghm 17155 . . . 4 RingHom
31 ghmmhm 16069 . . . 4 MndHom
3229, 30, 313syl 20 . . 3 MndHom