Theorem evlsgsummul

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

	Ref	Expression
Hypotheses	evlsgsummul.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsgsummul.w	$$⊢W=I\mathrm{mPoly}U$$
	evlsgsummul.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evlsgsummul.1	$$⊢\underset{\dot{}}{1}=1_W$$
	evlsgsummul.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsgsummul.p	$$⊢P=S{\uparrow }_{𝑠}\left(K^I\right)$$
	evlsgsummul.h	$$⊢H={\mathrm{mulGrp}}_P$$
	evlsgsummul.k	$$⊢K={\mathrm{Base}}_S$$
	evlsgsummul.b	$$⊢B={\mathrm{Base}}_W$$
	evlsgsummul.i	$$⊢\phi \to I\in V$$
	evlsgsummul.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsgsummul.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsgsummul.y	$$⊢\left(\phi \wedge x\in N\right)\to Y\in B$$
	evlsgsummul.n	$$⊢\phi \to N\subseteq {\mathbb{N}}_0$$
	evlsgsummul.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(\left(x\in N⟼Y\right)\right)$$
Assertion	evlsgsummul	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_G}Y\right)=\underset{x\in N}{{\sum }_H}Q\left(Y\right)$$

Proof

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