evlsgsumadd

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

	Ref	Expression
Hypotheses	evlsgsumadd.q	$⊢ Q = (I evalSub S) (R)$
	evlsgsumadd.w	$⊢ W = I mPoly U$
	evlsgsumadd.0	$⊢ \underset{˙}{0} = 0_{W}$
	evlsgsumadd.u	$⊢ U = S ↾_{𝑠} R$
	evlsgsumadd.p	$⊢ P = S ↑_{𝑠} (K^{I})$
	evlsgsumadd.k	$⊢ K = {Base}_{S}$
	evlsgsumadd.b	$⊢ B = {Base}_{W}$
	evlsgsumadd.i	$⊢ φ \to I \in V$
	evlsgsumadd.s	$⊢ φ \to S \in CRing$
	evlsgsumadd.r	$⊢ φ \to R \in SubRing (S)$
	evlsgsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
	evlsgsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
	evlsgsumadd.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in N ⟼ Y))$
Assertion	evlsgsumadd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Proof

Step	Hyp	Ref	Expression
1		evlsgsumadd.q	$⊢ Q = (I evalSub S) (R)$
2		evlsgsumadd.w	$⊢ W = I mPoly U$
3		evlsgsumadd.0	$⊢ \underset{˙}{0} = 0_{W}$
4		evlsgsumadd.u	$⊢ U = S ↾_{𝑠} R$
5		evlsgsumadd.p	$⊢ P = S ↑_{𝑠} (K^{I})$
6		evlsgsumadd.k	$⊢ K = {Base}_{S}$
7		evlsgsumadd.b	$⊢ B = {Base}_{W}$
8		evlsgsumadd.i	$⊢ φ \to I \in V$
9		evlsgsumadd.s	$⊢ φ \to S \in CRing$
10		evlsgsumadd.r	$⊢ φ \to R \in SubRing (S)$
11		evlsgsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
12		evlsgsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
13		evlsgsumadd.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in N ⟼ Y))$
14	4	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
15	10 14	syl	$⊢ φ \to U \in Ring$
16	2	mplring	$⊢ (I \in V \land U \in Ring) \to W \in Ring$
17	8 15 16	syl2anc	$⊢ φ \to W \in Ring$
18		ringcmn	$⊢ W \in Ring \to W \in CMnd$
19	17 18	syl	$⊢ φ \to W \in CMnd$
20		crngring	$⊢ S \in CRing \to S \in Ring$
21	9 20	syl	$⊢ φ \to S \in Ring$
22		ovex	$⊢ K^{I} \in V$
23	21 22	jctir	$⊢ φ \to (S \in Ring \land K^{I} \in V)$
24	5	pwsring	$⊢ (S \in Ring \land K^{I} \in V) \to P \in Ring$
25		ringmnd	$⊢ P \in Ring \to P \in Mnd$
26	23 24 25	3syl	$⊢ φ \to P \in Mnd$
27		nn0ex	$⊢ ℕ_{0} \in V$
28	27	a1i	$⊢ φ \to ℕ_{0} \in V$
29	28 12	ssexd	$⊢ φ \to N \in V$
30	1 2 4 5 6	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom P)$
31	8 9 10 30	syl3anc	$⊢ φ \to Q \in (W RingHom P)$
32		rhmghm	$⊢ Q \in (W RingHom P) \to Q \in (W GrpHom P)$
33		ghmmhm	$⊢ Q \in (W GrpHom P) \to Q \in (W MndHom P)$
34	31 32 33	3syl	$⊢ φ \to Q \in (W MndHom P)$
35	7 3 19 26 29 34 11 13	gsummptmhm	$⊢ φ \to \underset{x \in N}{\sum_{P}} Q (Y) = Q (\underset{x \in N}{\sum_{W}} Y)$
36	35	eqcomd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Metamath Proof Explorer

Theorem evlsgsumadd

Proof