# Metamath Proof Explorer

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

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

### Proof

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