Theorem evls1gsummul

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

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