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	eqtrid	$$⊢\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	8 4	mgpbas	$$⊢B={\mathrm{Base}}_G$$
32	3	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
33	20 32	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
34	8	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
35	33 34	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
36	35	adantr	$$⊢\left(\phi \wedge x\in M\right)\to G\in \mathrm{Mnd}$$
37	16	r19.21bi	$$⊢\left(\phi \wedge x\in M\right)\to N\in {\mathbb{N}}_0$$
38	20	adantr	$$⊢\left(\phi \wedge x\in M\right)\to R\in \mathrm{Ring}$$
39	5 3 4	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
40	38 39	syl	$$⊢\left(\phi \wedge x\in M\right)\to X\in B$$
41	31 9 36 37 40	mulgnn0cld	$$⊢\left(\phi \wedge x\in M\right)\to N\underset{\dot{}}{\times }X\in B$$
42		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
43		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
44	4 42 10 43	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$$
45	23 30 41 44	syl3anc	$$⊢\left(\phi \wedge x\in M\right)\to A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\in B$$
46	1 2 3 18 4 12 45 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)$$
47	12	adantr	$$⊢\left(\phi \wedge x\in M\right)\to R\in \mathrm{CRing}$$
48	17	adantr	$$⊢\left(\phi \wedge x\in M\right)\to C\in K$$
49	1 3 8 5 2 9 47 37 10 24 48 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)$$
50	49	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)$$
51	50	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)$$
52	46 51	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)$$