This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )