# Metamath Proof Explorer

## Theorem evls1gsummul

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

Ref Expression
Hypotheses evls1gsummul.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1gsummul.k 𝐾 = ( Base ‘ 𝑆 )
evls1gsummul.w 𝑊 = ( Poly1𝑈 )
evls1gsummul.g 𝐺 = ( mulGrp ‘ 𝑊 )
evls1gsummul.1 1 = ( 1r𝑊 )
evls1gsummul.u 𝑈 = ( 𝑆s 𝑅 )
evls1gsummul.p 𝑃 = ( 𝑆s 𝐾 )
evls1gsummul.h 𝐻 = ( mulGrp ‘ 𝑃 )
evls1gsummul.b 𝐵 = ( Base ‘ 𝑊 )
evls1gsummul.s ( 𝜑𝑆 ∈ CRing )
evls1gsummul.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1gsummul.y ( ( 𝜑𝑥𝑁 ) → 𝑌𝐵 )
evls1gsummul.n ( 𝜑𝑁 ⊆ ℕ0 )
evls1gsummul.f ( 𝜑 → ( 𝑥𝑁𝑌 ) finSupp 1 )
Assertion evls1gsummul ( 𝜑 → ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝐻 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )

### Proof

Step Hyp Ref Expression
1 evls1gsummul.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1gsummul.k 𝐾 = ( Base ‘ 𝑆 )
3 evls1gsummul.w 𝑊 = ( Poly1𝑈 )
4 evls1gsummul.g 𝐺 = ( mulGrp ‘ 𝑊 )
5 evls1gsummul.1 1 = ( 1r𝑊 )
6 evls1gsummul.u 𝑈 = ( 𝑆s 𝑅 )
7 evls1gsummul.p 𝑃 = ( 𝑆s 𝐾 )
8 evls1gsummul.h 𝐻 = ( mulGrp ‘ 𝑃 )
9 evls1gsummul.b 𝐵 = ( Base ‘ 𝑊 )
10 evls1gsummul.s ( 𝜑𝑆 ∈ CRing )
11 evls1gsummul.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12 evls1gsummul.y ( ( 𝜑𝑥𝑁 ) → 𝑌𝐵 )
13 evls1gsummul.n ( 𝜑𝑁 ⊆ ℕ0 )
14 evls1gsummul.f ( 𝜑 → ( 𝑥𝑁𝑌 ) finSupp 1 )
15 4 9 mgpbas 𝐵 = ( Base ‘ 𝐺 )
16 4 5 ringidval 1 = ( 0g𝐺 )
17 6 subrgcrng ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
18 10 11 17 syl2anc ( 𝜑𝑈 ∈ CRing )
19 3 ply1crng ( 𝑈 ∈ CRing → 𝑊 ∈ CRing )
20 4 crngmgp ( 𝑊 ∈ CRing → 𝐺 ∈ CMnd )
21 18 19 20 3syl ( 𝜑𝐺 ∈ CMnd )
22 crngring ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
23 10 22 syl ( 𝜑𝑆 ∈ Ring )
24 2 fvexi 𝐾 ∈ V
25 23 24 jctir ( 𝜑 → ( 𝑆 ∈ Ring ∧ 𝐾 ∈ V ) )
26 7 pwsring ( ( 𝑆 ∈ Ring ∧ 𝐾 ∈ V ) → 𝑃 ∈ Ring )
27 8 ringmgp ( 𝑃 ∈ Ring → 𝐻 ∈ Mnd )
28 25 26 27 3syl ( 𝜑𝐻 ∈ Mnd )
29 nn0ex 0 ∈ V
30 29 a1i ( 𝜑 → ℕ0 ∈ V )
31 30 13 ssexd ( 𝜑𝑁 ∈ V )
32 1 2 7 6 3 evls1rhm ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
33 10 11 32 syl2anc ( 𝜑𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
34 4 8 rhmmhm ( 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
35 33 34 syl ( 𝜑𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
36 15 16 21 28 31 35 12 14 gsummptmhm ( 𝜑 → ( 𝐻 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) = ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥𝑁𝑌 ) ) ) )
37 36 eqcomd ( 𝜑 → ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝐻 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )