Theorem evl1gsumadd

Description: Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd . (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$$
	evl1gsumadd.0	$$⊢\underset{\dot{}}{0}=0_W$$
	evl1gsumadd.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in N⟼Y\right)\right)$$
Assertion	evl1gsumadd	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_W}Y\right)=\underset{x\in N}{{\sum }_P}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		evl1gsumadd.0	$$⊢\underset{\dot{}}{0}=0_W$$
10		evl1gsumadd.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in N⟼Y\right)\right)$$
11	1 2	evl1fval1	$$⊢Q=R{\mathrm{evalSub}}_{1}K$$
12	11	a1i	$$⊢\phi \to Q=R{\mathrm{evalSub}}_{1}K$$
13	12	fveq1d	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_W}Y\right)=\left(R{\mathrm{evalSub}}_{1}K\right)\left(\underset{x\in N}{{\sum }_W}Y\right)$$
14	2	ressid	$$⊢R\in \mathrm{CRing}\to R{\upharpoonright }_{𝑠}K=R$$
15	6 14	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}K=R$$
16	15	eqcomd	$$⊢\phi \to R=R{\upharpoonright }_{𝑠}K$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)$$
18	3 17	syl5eq	$$⊢\phi \to W={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)$$
19	18	fvoveq1d	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}K\right)\left(\underset{x\in N}{{\sum }_W}Y\right)=\left(R{\mathrm{evalSub}}_{1}K\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}}Y\right)$$
20		eqid	$$⊢R{\mathrm{evalSub}}_{1}K=R{\mathrm{evalSub}}_{1}K$$
21		eqid	$$⊢{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)$$
22		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}=0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}$$
23		eqid	$$⊢R{\upharpoonright }_{𝑠}K=R{\upharpoonright }_{𝑠}K$$
24		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}$$
25		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
26	2	subrgid	$$⊢R\in \mathrm{Ring}\to K\in \mathrm{SubRing}\left(R\right)$$
27	6 25 26	3syl	$$⊢\phi \to K\in \mathrm{SubRing}\left(R\right)$$
28	18	adantr	$$⊢\left(\phi \wedge x\in N\right)\to W={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)$$
29	28	fveq2d	$$⊢\left(\phi \wedge x\in N\right)\to {\mathrm{Base}}_W={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}$$
30	5 29	syl5eq	$$⊢\left(\phi \wedge x\in N\right)\to B={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}$$
31	7 30	eleqtrd	$$⊢\left(\phi \wedge x\in N\right)\to Y\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}$$
32	18	eqcomd	$$⊢\phi \to {\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)=W$$
33	32	fveq2d	$$⊢\phi \to 0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}=0_W$$
34	33 9	eqtr4di	$$⊢\phi \to 0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}=\underset{\dot{}}{0}$$
35	10 34	breqtrrd	$$⊢\phi \to {finSupp}_{0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}}\left(\left(x\in N⟼Y\right)\right)$$
36	20 2 21 22 23 4 24 6 27 31 8 35	evls1gsumadd	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}K\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}K\right)}}Y\right)=\underset{x\in N}{{\sum }_P}\left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)$$
37	19 36	eqtrd	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}K\right)\left(\underset{x\in N}{{\sum }_W}Y\right)=\underset{x\in N}{{\sum }_P}\left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)$$
38	12	fveq1d	$$⊢\phi \to Q\left(Y\right)=\left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)$$
39	38	eqcomd	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)=Q\left(Y\right)$$
40	39	mpteq2dv	$$⊢\phi \to \left(x\in N⟼\left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)\right)=\left(x\in N⟼Q\left(Y\right)\right)$$
41	40	oveq2d	$$⊢\phi \to \underset{x\in N}{{\sum }_P}\left(R{\mathrm{evalSub}}_{1}K\right)\left(Y\right)=\underset{x\in N}{{\sum }_P}Q\left(Y\right)$$
42	13 37 41	3eqtrd	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_W}Y\right)=\underset{x\in N}{{\sum }_P}Q\left(Y\right)$$