Theorem evl1gsummul

Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsumadd.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
	evl1gsumadd.k	$$⊢K={\mathrm{Base}}_R$$
	evl1gsumadd.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	evl1gsumadd.p	$$⊢P=R{\uparrow }_{𝑠}K$$
	evl1gsumadd.b	$$⊢B={\mathrm{Base}}_W$$
	evl1gsumadd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1gsumadd.y	$$⊢\left(\phi \wedge x\in N\right)\to Y\in B$$
	evl1gsumadd.n	$$⊢\phi \to N\subseteq {\mathbb{N}}_0$$
	evl1gsummul.1	$$⊢\underset{\dot{}}{1}=1_W$$
	evl1gsummul.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evl1gsummul.h	$$⊢H={\mathrm{mulGrp}}_P$$
	evl1gsummul.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(\left(x\in N⟼Y\right)\right)$$
Assertion	evl1gsummul	$$⊢\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		evl1gsumadd.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
2		evl1gsumadd.k	$$⊢K={\mathrm{Base}}_R$$
3		evl1gsumadd.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
4		evl1gsumadd.p	$$⊢P=R{\uparrow }_{𝑠}K$$
5		evl1gsumadd.b	$$⊢B={\mathrm{Base}}_W$$
6		evl1gsumadd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		evl1gsumadd.y	$$⊢\left(\phi \wedge x\in N\right)\to Y\in B$$
8		evl1gsumadd.n	$$⊢\phi \to N\subseteq {\mathbb{N}}_0$$
9		evl1gsummul.1	$$⊢\underset{\dot{}}{1}=1_W$$
10		evl1gsummul.g	$$⊢G={\mathrm{mulGrp}}_W$$
11		evl1gsummul.h	$$⊢H={\mathrm{mulGrp}}_P$$
12		evl1gsummul.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(\left(x\in N⟼Y\right)\right)$$
13	10 5	mgpbas	$$⊢B={\mathrm{Base}}_G$$
14	10 9	ringidval	$$⊢\underset{\dot{}}{1}=0_G$$
15	3	ply1crng	$$⊢R\in \mathrm{CRing}\to W\in \mathrm{CRing}$$
16	10	crngmgp	$$⊢W\in \mathrm{CRing}\to G\in \mathrm{CMnd}$$
17	6 15 16	3syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
18		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
19	6 18	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
20	2	fvexi	$$⊢K\in \mathrm{V}$$
21	19 20	jctir	$$⊢\phi \to \left(R\in \mathrm{Ring}\wedge K\in \mathrm{V}\right)$$
22	4	pwsring	$$⊢\left(R\in \mathrm{Ring}\wedge K\in \mathrm{V}\right)\to P\in \mathrm{Ring}$$
23	11	ringmgp	$$⊢P\in \mathrm{Ring}\to H\in \mathrm{Mnd}$$
24	21 22 23	3syl	$$⊢\phi \to H\in \mathrm{Mnd}$$
25		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
26	25	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
27	26 8	ssexd	$$⊢\phi \to N\in \mathrm{V}$$
28	1 3 4 2	evl1rhm	$$⊢R\in \mathrm{CRing}\to Q\in \left(W\mathrm{RingHom}P\right)$$
29	10 11	rhmmhm	$$⊢Q\in \left(W\mathrm{RingHom}P\right)\to Q\in \left(G\mathrm{MndHom}H\right)$$
30	6 28 29	3syl	$$⊢\phi \to Q\in \left(G\mathrm{MndHom}H\right)$$
31	13 14 17 24 27 30 7 12	gsummptmhm	$$⊢\phi \to \underset{x\in N}{{\sum }_H}Q\left(Y\right)=Q\left(\underset{x\in N}{{\sum }_G}Y\right)$$
32	31	eqcomd	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_G}Y\right)=\underset{x\in N}{{\sum }_H}Q\left(Y\right)$$