Theorem evls1gsummul

Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 14-Sep-2019)

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

Proof

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