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