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

Metamath Proof Explorer

Theorem evlsgsumadd

Description: Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024)

Ref Expression
Hypotheses evlsgsumadd.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsgsumadd.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsgsumadd.0 ⊢ 0 = ( 0g ‘ 𝑊 )
evlsgsumadd.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsgsumadd.p ⊢ 𝑃 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
evlsgsumadd.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsgsumadd.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evlsgsumadd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsgsumadd.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsgsumadd.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsgsumadd.y ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
evlsgsumadd.n ⊢ ( 𝜑 → 𝑁 ⊆ ℕ0 )
evlsgsumadd.f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp 0 )
Assertion evlsgsumadd ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )

Proof

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