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 = ( eval1 ` R )
	evl1gsummon.k	|- K = ( Base ` R )
	evl1gsummon.w	|- W = ( Poly1 ` R )
	evl1gsummon.b	|- B = ( Base ` W )
	evl1gsummon.x	|- X = ( var1 ` R )
	evl1gsummon.h	|- H = ( mulGrp ` R )
	evl1gsummon.e	|- E = ( .g ` H )
	evl1gsummon.g	|- G = ( mulGrp ` W )
	evl1gsummon.p	|- .^ = ( .g ` G )
	evl1gsummon.t1	|- .X. = ( .s ` W )
	evl1gsummon.t2	|- .x. = ( .r ` R )
	evl1gsummon.r	|- ( ph -> R e. CRing )
	evl1gsummon.a	|- ( ph -> A. x e. M A e. K )
	evl1gsummon.m	|- ( ph -> M C_ NN0 )
	evl1gsummon.f	|- ( ph -> M e. Fin )
	evl1gsummon.n	|- ( ph -> A. x e. M N e. NN0 )
	evl1gsummon.c	|- ( ph -> C e. K )
Assertion	evl1gsummon	|- ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1gsummon.q	|- Q = ( eval1 ` R )
2		evl1gsummon.k	|- K = ( Base ` R )
3		evl1gsummon.w	|- W = ( Poly1 ` R )
4		evl1gsummon.b	|- B = ( Base ` W )
5		evl1gsummon.x	|- X = ( var1 ` R )
6		evl1gsummon.h	|- H = ( mulGrp ` R )
7		evl1gsummon.e	|- E = ( .g ` H )
8		evl1gsummon.g	|- G = ( mulGrp ` W )
9		evl1gsummon.p	|- .^ = ( .g ` G )
10		evl1gsummon.t1	|- .X. = ( .s ` W )
11		evl1gsummon.t2	|- .x. = ( .r ` R )
12		evl1gsummon.r	|- ( ph -> R e. CRing )
13		evl1gsummon.a	|- ( ph -> A. x e. M A e. K )
14		evl1gsummon.m	|- ( ph -> M C_ NN0 )
15		evl1gsummon.f	|- ( ph -> M e. Fin )
16		evl1gsummon.n	|- ( ph -> A. x e. M N e. NN0 )
17		evl1gsummon.c	|- ( ph -> C e. K )
18		eqid	|- ( R ^s K ) = ( R ^s K )
19		crngring	|- ( R e. CRing -> R e. Ring )
20	12 19	syl	|- ( ph -> R e. Ring )
21	3	ply1lmod	|- ( R e. Ring -> W e. LMod )
22	20 21	syl	|- ( ph -> W e. LMod )
23	22	adantr	|- ( ( ph /\ x e. M ) -> W e. LMod )
24	13	r19.21bi	|- ( ( ph /\ x e. M ) -> A e. K )
25	3	ply1sca	|- ( R e. CRing -> R = ( Scalar ` W ) )
26	12 25	syl	|- ( ph -> R = ( Scalar ` W ) )
27	26	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` W ) ) )
28	2 27	eqtrid	|- ( ph -> K = ( Base ` ( Scalar ` W ) ) )
29	28	adantr	|- ( ( ph /\ x e. M ) -> K = ( Base ` ( Scalar ` W ) ) )
30	24 29	eleqtrd	|- ( ( ph /\ x e. M ) -> A e. ( Base ` ( Scalar ` W ) ) )
31	8 4	mgpbas	|- B = ( Base ` G )
32	3	ply1ring	|- ( R e. Ring -> W e. Ring )
33	20 32	syl	|- ( ph -> W e. Ring )
34	8	ringmgp	|- ( W e. Ring -> G e. Mnd )
35	33 34	syl	|- ( ph -> G e. Mnd )
36	35	adantr	|- ( ( ph /\ x e. M ) -> G e. Mnd )
37	16	r19.21bi	|- ( ( ph /\ x e. M ) -> N e. NN0 )
38	20	adantr	|- ( ( ph /\ x e. M ) -> R e. Ring )
39	5 3 4	vr1cl	|- ( R e. Ring -> X e. B )
40	38 39	syl	|- ( ( ph /\ x e. M ) -> X e. B )
41	31 9 36 37 40	mulgnn0cld	|- ( ( ph /\ x e. M ) -> ( N .^ X ) e. B )
42		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
43		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
44	4 42 10 43	lmodvscl	|- ( ( W e. LMod /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( N .^ X ) e. B ) -> ( A .X. ( N .^ X ) ) e. B )
45	23 30 41 44	syl3anc	|- ( ( ph /\ x e. M ) -> ( A .X. ( N .^ X ) ) e. B )
46	1 2 3 18 4 12 45 14 15 17	evl1gsumaddval	|- ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) ) )
47	12	adantr	|- ( ( ph /\ x e. M ) -> R e. CRing )
48	17	adantr	|- ( ( ph /\ x e. M ) -> C e. K )
49	1 3 8 5 2 9 47 37 10 24 48 6 7 11	evl1scvarpwval	|- ( ( ph /\ x e. M ) -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) )
50	49	mpteq2dva	|- ( ph -> ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) = ( x e. M |-> ( A .x. ( N E C ) ) ) )
51	50	oveq2d	|- ( ph -> ( R gsum ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )
52	46 51	eqtrd	|- ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )