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