Theorem evl1gsummon

Description: Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsummon.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
	evl1gsummon.k	$$⊢K={\mathrm{Base}}_R$$
	evl1gsummon.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	evl1gsummon.b	$$⊢B={\mathrm{Base}}_W$$
	evl1gsummon.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	evl1gsummon.h	$$⊢H={\mathrm{mulGrp}}_R$$
	evl1gsummon.e	$$⊢E={\cdot }_H$$
	evl1gsummon.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evl1gsummon.p	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	evl1gsummon.t1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
	evl1gsummon.t2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	evl1gsummon.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1gsummon.a	$$⊢\phi \to \forall x\in MA\in K$$
	evl1gsummon.m	$$⊢\phi \to M\subseteq {\mathbb{N}}_0$$
	evl1gsummon.f	$$⊢\phi \to M\in \mathrm{Fin}$$
	evl1gsummon.n	$$⊢\phi \to \forall x\in MN\in {\mathbb{N}}_0$$
	evl1gsummon.c	$$⊢\phi \to C\in K$$
Assertion	evl1gsummon	$$⊢\phi \to Q\left(\underset{x\in M}{{\sum }_W}\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\right)\left(C\right)=\underset{x\in M}{{\sum }_R}\left(A\underset{\dot{}}{·}\left(NEC\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1gsummon.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
2		evl1gsummon.k	$$⊢K={\mathrm{Base}}_R$$
3		evl1gsummon.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
4		evl1gsummon.b	$$⊢B={\mathrm{Base}}_W$$
5		evl1gsummon.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
6		evl1gsummon.h	$$⊢H={\mathrm{mulGrp}}_R$$
7		evl1gsummon.e	$$⊢E={\cdot }_H$$
8		evl1gsummon.g	$$⊢G={\mathrm{mulGrp}}_W$$
9		evl1gsummon.p	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
10		evl1gsummon.t1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
11		evl1gsummon.t2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
12		evl1gsummon.r	$$⊢\phi \to R\in \mathrm{CRing}$$
13		evl1gsummon.a	$$⊢\phi \to \forall x\in MA\in K$$
14		evl1gsummon.m	$$⊢\phi \to M\subseteq {\mathbb{N}}_0$$
15		evl1gsummon.f	$$⊢\phi \to M\in \mathrm{Fin}$$
16		evl1gsummon.n	$$⊢\phi \to \forall x\in MN\in {\mathbb{N}}_0$$
17		evl1gsummon.c	$$⊢\phi \to C\in K$$
18		eqid	$$⊢R{\uparrow }_{𝑠}K=R{\uparrow }_{𝑠}K$$
19		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
20	12 19	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
21	3	ply1lmod	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
22	20 21	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
23	22	adantr	$$⊢\left(\phi \wedge x\in M\right)\to W\in \mathrm{LMod}$$
24	13	r19.21bi	$$⊢\left(\phi \wedge x\in M\right)\to A\in K$$
25	3	ply1sca	$$⊢R\in \mathrm{CRing}\to R=\mathrm{Scalar}\left(W\right)$$
26	12 25	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(W\right)$$
27	26	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
28	2 27	syl5eq	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
29	28	adantr	$$⊢\left(\phi \wedge x\in M\right)\to K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
30	24 29	eleqtrd	$$⊢\left(\phi \wedge x\in M\right)\to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
31	3	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
32	20 31	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
33	8	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
34	32 33	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
35	34	adantr	$$⊢\left(\phi \wedge x\in M\right)\to G\in \mathrm{Mnd}$$
36	16	r19.21bi	$$⊢\left(\phi \wedge x\in M\right)\to N\in {\mathbb{N}}_0$$
37	20	adantr	$$⊢\left(\phi \wedge x\in M\right)\to R\in \mathrm{Ring}$$
38	5 3 4	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
39	37 38	syl	$$⊢\left(\phi \wedge x\in M\right)\to X\in B$$
40	8 4	mgpbas	$$⊢B={\mathrm{Base}}_G$$
41	40 9	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{\times }X\in B$$
42	35 36 39 41	syl3anc	$$⊢\left(\phi \wedge x\in M\right)\to N\underset{\dot{}}{\times }X\in B$$
43		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
44		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
45	4 43 10 44	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge N\underset{\dot{}}{\times }X\in B\right)\to A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\in B$$
46	23 30 42 45	syl3anc	$$⊢\left(\phi \wedge x\in M\right)\to A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\in B$$
47	1 2 3 18 4 12 46 14 15 17	evl1gsumaddval	$$⊢\phi \to Q\left(\underset{x\in M}{{\sum }_W}\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\right)\left(C\right)=\underset{x\in M}{{\sum }_R}Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)$$
48	12	adantr	$$⊢\left(\phi \wedge x\in M\right)\to R\in \mathrm{CRing}$$
49	17	adantr	$$⊢\left(\phi \wedge x\in M\right)\to C\in K$$
50	1 3 8 5 2 9 48 36 10 24 49 6 7 11	evl1scvarpwval	$$⊢\left(\phi \wedge x\in M\right)\to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)=A\underset{\dot{}}{·}\left(NEC\right)$$
51	50	mpteq2dva	$$⊢\phi \to \left(x\in M⟼Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)\right)=\left(x\in M⟼A\underset{\dot{}}{·}\left(NEC\right)\right)$$
52	51	oveq2d	$$⊢\phi \to \underset{x\in M}{{\sum }_R}Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)=\underset{x\in M}{{\sum }_R}\left(A\underset{\dot{}}{·}\left(NEC\right)\right)$$
53	47 52	eqtrd	$$⊢\phi \to Q\left(\underset{x\in M}{{\sum }_W}\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\right)\left(C\right)=\underset{x\in M}{{\sum }_R}\left(A\underset{\dot{}}{·}\left(NEC\right)\right)$$