evlsgsummul

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

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

Proof

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

Metamath Proof Explorer

Theorem evlsgsummul

Proof