Theorem evl1gsumaddval

Description: Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-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$$
	evl1gsumaddval.f	$$⊢\phi \to N\in \mathrm{Fin}$$
	evl1gsumaddval.c	$$⊢\phi \to C\in K$$
Assertion	evl1gsumaddval	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_W}Y\right)\left(C\right)=\underset{x\in N}{{\sum }_R}Q\left(Y\right)\left(C\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		evl1gsumaddval.f	$$⊢\phi \to N\in \mathrm{Fin}$$
10		evl1gsumaddval.c	$$⊢\phi \to C\in K$$
11	7	ralrimiva	$$⊢\phi \to \forall x\in NY\in B$$
12	1 3 2 5 6 10 11 9	evl1gsumd	$$⊢\phi \to Q\left(\underset{x\in N}{{\sum }_W}Y\right)\left(C\right)=\underset{x\in N}{{\sum }_R}Q\left(Y\right)\left(C\right)$$