Theorem evlsgsummul

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

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

Proof

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