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

Theorem evl1gsummul 18883
 Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019.)
Hypotheses
Ref Expression
evl1gsummul.1
evl1gsummul.g mulGrp
evl1gsummul.h mulGrp
evl1gsummul.f finSupp
Assertion
Ref Expression
evl1gsummul g g
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem evl1gsummul
StepHypRef Expression
1 evl1gsummul.g . . . 4 mulGrp
2 evl1gsumadd.b . . . 4
31, 2mgpbas 17664 . . 3
4 evl1gsummul.1 . . . 4
51, 4ringidval 17672 . . 3
6 evl1gsumadd.r . . . 4
7 evl1gsumadd.w . . . . 5 Poly1
87ply1crng 18726 . . . 4
91crngmgp 17723 . . . 4 CMnd
106, 8, 93syl 18 . . 3 CMnd
11 crngring 17726 . . . . . 6
126, 11syl 17 . . . . 5
13 evl1gsumadd.k . . . . . 6
14 fvex 5891 . . . . . 6
1513, 14eqeltri 2513 . . . . 5
1612, 15jctir 540 . . . 4
17 evl1gsumadd.p . . . . 5 s
1817pwsring 17778 . . . 4
19 evl1gsummul.h . . . . 5 mulGrp
2019ringmgp 17721 . . . 4
2116, 18, 203syl 18 . . 3
22 nn0ex 10875 . . . . 5
2322a1i 11 . . . 4
24 evl1gsumadd.n . . . 4
2523, 24ssexd 4572 . . 3
26 evl1gsumadd.q . . . . 5 eval1
2726, 7, 17, 13evl1rhm 18855 . . . 4 RingHom
281, 19rhmmhm 17885 . . . 4 RingHom MndHom
296, 27, 283syl 18 . . 3 MndHom