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