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 = ( eval1 ` R )
	evl1gsumadd.k	|- K = ( Base ` R )
	evl1gsumadd.w	|- W = ( Poly1 ` R )
	evl1gsumadd.p	|- P = ( R ^s K )
	evl1gsumadd.b	|- B = ( Base ` W )
	evl1gsumadd.r	|- ( ph -> R e. CRing )
	evl1gsumadd.y	|- ( ( ph /\ x e. N ) -> Y e. B )
	evl1gsumadd.n	|- ( ph -> N C_ NN0 )
	evl1gsumaddval.f	|- ( ph -> N e. Fin )
	evl1gsumaddval.c	|- ( ph -> C e. K )
Assertion	evl1gsumaddval	|- ( ph -> ( ( Q ` ( W gsum ( x e. N |-> Y ) ) ) ` C ) = ( R gsum ( x e. N |-> ( ( Q ` Y ) ` C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1gsumadd.q	|- Q = ( eval1 ` R )
2		evl1gsumadd.k	|- K = ( Base ` R )
3		evl1gsumadd.w	|- W = ( Poly1 ` R )
4		evl1gsumadd.p	|- P = ( R ^s K )
5		evl1gsumadd.b	|- B = ( Base ` W )
6		evl1gsumadd.r	|- ( ph -> R e. CRing )
7		evl1gsumadd.y	|- ( ( ph /\ x e. N ) -> Y e. B )
8		evl1gsumadd.n	|- ( ph -> N C_ NN0 )
9		evl1gsumaddval.f	|- ( ph -> N e. Fin )
10		evl1gsumaddval.c	|- ( ph -> C e. K )
11	7	ralrimiva	|- ( ph -> A. x e. N Y e. B )
12	1 3 2 5 6 10 11 9	evl1gsumd	|- ( ph -> ( ( Q ` ( W gsum ( x e. N |-> Y ) ) ) ` C ) = ( R gsum ( x e. N |-> ( ( Q ` Y ) ` C ) ) ) )