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 8 15	mplringd	$⊢ φ \to W \in Ring$
17		ringcmn	$⊢ W \in Ring \to W \in CMnd$
18	16 17	syl	$⊢ φ \to W \in CMnd$
19		crngring	$⊢ S \in CRing \to S \in Ring$
20	9 19	syl	$⊢ φ \to S \in Ring$
21		ovex	$⊢ K^{I} \in V$
22	20 21	jctir	$⊢ φ \to (S \in Ring \land K^{I} \in V)$
23	5	pwsring	$⊢ (S \in Ring \land K^{I} \in V) \to P \in Ring$
24		ringmnd	$⊢ P \in Ring \to P \in Mnd$
25	22 23 24	3syl	$⊢ φ \to P \in Mnd$
26		nn0ex	$⊢ ℕ_{0} \in V$
27	26	a1i	$⊢ φ \to ℕ_{0} \in V$
28	27 12	ssexd	$⊢ φ \to N \in V$
29	1 2 4 5 6	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom P)$
30	8 9 10 29	syl3anc	$⊢ φ \to Q \in (W RingHom P)$
31		rhmghm	$⊢ Q \in (W RingHom P) \to Q \in (W GrpHom P)$
32		ghmmhm	$⊢ Q \in (W GrpHom P) \to Q \in (W MndHom P)$
33	30 31 32	3syl	$⊢ φ \to Q \in (W MndHom P)$
34	7 3 18 25 28 33 11 13	gsummptmhm	$⊢ φ \to \underset{x \in N}{\sum_{P}} Q (Y) = Q (\underset{x \in N}{\sum_{W}} Y)$
35	34	eqcomd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Metamath Proof Explorer

Theorem evlsgsumadd

Proof