Metamath Proof Explorer


Theorem evls1gsumadd

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 3 ply1ring ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
15 ringcmn ( 𝑊 ∈ Ring → 𝑊 ∈ CMnd )
16 9 13 14 15 4syl ( 𝜑𝑊 ∈ CMnd )
17 crngring ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
18 8 17 syl ( 𝜑𝑆 ∈ Ring )
19 2 fvexi 𝐾 ∈ V
20 18 19 jctir ( 𝜑 → ( 𝑆 ∈ Ring ∧ 𝐾 ∈ V ) )
21 6 pwsring ( ( 𝑆 ∈ Ring ∧ 𝐾 ∈ V ) → 𝑃 ∈ Ring )
22 ringmnd ( 𝑃 ∈ Ring → 𝑃 ∈ Mnd )
23 20 21 22 3syl ( 𝜑𝑃 ∈ Mnd )
24 nn0ex 0 ∈ V
25 24 a1i ( 𝜑 → ℕ0 ∈ V )
26 25 11 ssexd ( 𝜑𝑁 ∈ V )
27 1 2 6 5 3 evls1rhm ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
28 8 9 27 syl2anc ( 𝜑𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
29 rhmghm ( 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) → 𝑄 ∈ ( 𝑊 GrpHom 𝑃 ) )
30 ghmmhm ( 𝑄 ∈ ( 𝑊 GrpHom 𝑃 ) → 𝑄 ∈ ( 𝑊 MndHom 𝑃 ) )
31 28 29 30 3syl ( 𝜑𝑄 ∈ ( 𝑊 MndHom 𝑃 ) )
32 7 4 16 23 26 31 10 12 gsummptmhm ( 𝜑 → ( 𝑃 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) = ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) )
33 32 eqcomd ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )