Theorem coe1fzgsumd

Description: Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019)

	Ref	Expression
Hypotheses	coe1fzgsumd.p	|- P = ( Poly1 ` R )
	coe1fzgsumd.b	|- B = ( Base ` P )
	coe1fzgsumd.r	|- ( ph -> R e. Ring )
	coe1fzgsumd.k	|- ( ph -> K e. NN0 )
	coe1fzgsumd.m	|- ( ph -> A. x e. N M e. B )
	coe1fzgsumd.n	|- ( ph -> N e. Fin )
Assertion	coe1fzgsumd	|- ( ph -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fzgsumd.p	|- P = ( Poly1 ` R )
2		coe1fzgsumd.b	|- B = ( Base ` P )
3		coe1fzgsumd.r	|- ( ph -> R e. Ring )
4		coe1fzgsumd.k	|- ( ph -> K e. NN0 )
5		coe1fzgsumd.m	|- ( ph -> A. x e. N M e. B )
6		coe1fzgsumd.n	|- ( ph -> N e. Fin )
7		raleq	|- ( n = (/) -> ( A. x e. n M e. B <-> A. x e. (/) M e. B ) )
8	7	anbi2d	|- ( n = (/) -> ( ( ph /\ A. x e. n M e. B ) <-> ( ph /\ A. x e. (/) M e. B ) ) )
9		mpteq1	|- ( n = (/) -> ( x e. n |-> M ) = ( x e. (/) |-> M ) )
10	9	oveq2d	|- ( n = (/) -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. (/) |-> M ) ) )
11	10	fveq2d	|- ( n = (/) -> ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) = ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) )
12	11	fveq1d	|- ( n = (/) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) )
13		mpteq1	|- ( n = (/) -> ( x e. n |-> ( ( coe1 ` M ) ` K ) ) = ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) )
14	13	oveq2d	|- ( n = (/) -> ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) )
15	12 14	eqeq12d	|- ( n = (/) -> ( ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) <-> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) ) )
16	8 15	imbi12d	|- ( n = (/) -> ( ( ( ph /\ A. x e. n M e. B ) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ( ph /\ A. x e. (/) M e. B ) -> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
17		raleq	|- ( n = m -> ( A. x e. n M e. B <-> A. x e. m M e. B ) )
18	17	anbi2d	|- ( n = m -> ( ( ph /\ A. x e. n M e. B ) <-> ( ph /\ A. x e. m M e. B ) ) )
19		mpteq1	|- ( n = m -> ( x e. n |-> M ) = ( x e. m |-> M ) )
20	19	oveq2d	|- ( n = m -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. m |-> M ) ) )
21	20	fveq2d	|- ( n = m -> ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) = ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) )
22	21	fveq1d	|- ( n = m -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) )
23		mpteq1	|- ( n = m -> ( x e. n |-> ( ( coe1 ` M ) ` K ) ) = ( x e. m |-> ( ( coe1 ` M ) ` K ) ) )
24	23	oveq2d	|- ( n = m -> ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) )
25	22 24	eqeq12d	|- ( n = m -> ( ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) <-> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) )
26	18 25	imbi12d	|- ( n = m -> ( ( ( ph /\ A. x e. n M e. B ) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ( ph /\ A. x e. m M e. B ) -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
27		raleq	|- ( n = ( m u. { a } ) -> ( A. x e. n M e. B <-> A. x e. ( m u. { a } ) M e. B ) )
28	27	anbi2d	|- ( n = ( m u. { a } ) -> ( ( ph /\ A. x e. n M e. B ) <-> ( ph /\ A. x e. ( m u. { a } ) M e. B ) ) )
29		mpteq1	|- ( n = ( m u. { a } ) -> ( x e. n |-> M ) = ( x e. ( m u. { a } ) |-> M ) )
30	29	oveq2d	|- ( n = ( m u. { a } ) -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. ( m u. { a } ) |-> M ) ) )
31	30	fveq2d	|- ( n = ( m u. { a } ) -> ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) = ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) )
32	31	fveq1d	|- ( n = ( m u. { a } ) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) )
33		mpteq1	|- ( n = ( m u. { a } ) -> ( x e. n |-> ( ( coe1 ` M ) ` K ) ) = ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) )
34	33	oveq2d	|- ( n = ( m u. { a } ) -> ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) )
35	32 34	eqeq12d	|- ( n = ( m u. { a } ) -> ( ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) <-> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) )
36	28 35	imbi12d	|- ( n = ( m u. { a } ) -> ( ( ( ph /\ A. x e. n M e. B ) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ( ph /\ A. x e. ( m u. { a } ) M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
37		raleq	|- ( n = N -> ( A. x e. n M e. B <-> A. x e. N M e. B ) )
38	37	anbi2d	|- ( n = N -> ( ( ph /\ A. x e. n M e. B ) <-> ( ph /\ A. x e. N M e. B ) ) )
39		mpteq1	|- ( n = N -> ( x e. n |-> M ) = ( x e. N |-> M ) )
40	39	oveq2d	|- ( n = N -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. N |-> M ) ) )
41	40	fveq2d	|- ( n = N -> ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) = ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) )
42	41	fveq1d	|- ( n = N -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) )
43		mpteq1	|- ( n = N -> ( x e. n |-> ( ( coe1 ` M ) ` K ) ) = ( x e. N |-> ( ( coe1 ` M ) ` K ) ) )
44	43	oveq2d	|- ( n = N -> ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) )
45	42 44	eqeq12d	|- ( n = N -> ( ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) <-> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) ) )
46	38 45	imbi12d	|- ( n = N -> ( ( ( ph /\ A. x e. n M e. B ) -> ( ( coe1 ` ( P gsum ( x e. n |-> M ) ) ) ` K ) = ( R gsum ( x e. n |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ( ph /\ A. x e. N M e. B ) -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
47		mpt0	|- ( x e. (/) |-> M ) = (/)
48	47	oveq2i	|- ( P gsum ( x e. (/) |-> M ) ) = ( P gsum (/) )
49		eqid	|- ( 0g ` P ) = ( 0g ` P )
50	49	gsum0	|- ( P gsum (/) ) = ( 0g ` P )
51	48 50	eqtri	|- ( P gsum ( x e. (/) |-> M ) ) = ( 0g ` P )
52	51	fveq2i	|- ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) = ( coe1 ` ( 0g ` P ) )
53	52	a1i	|- ( ph -> ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) = ( coe1 ` ( 0g ` P ) ) )
54	53	fveq1d	|- ( ph -> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( ( coe1 ` ( 0g ` P ) ) ` K ) )
55		eqid	|- ( 0g ` R ) = ( 0g ` R )
56	1 49 55	coe1z	|- ( R e. Ring -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
57	3 56	syl	|- ( ph -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
58	57	fveq1d	|- ( ph -> ( ( coe1 ` ( 0g ` P ) ) ` K ) = ( ( NN0 X. { ( 0g ` R ) } ) ` K ) )
59		fvex	|- ( 0g ` R ) e. _V
60		fvconst2g	|- ( ( ( 0g ` R ) e. _V /\ K e. NN0 ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` K ) = ( 0g ` R ) )
61	59 4 60	sylancr	|- ( ph -> ( ( NN0 X. { ( 0g ` R ) } ) ` K ) = ( 0g ` R ) )
62	54 58 61	3eqtrd	|- ( ph -> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( 0g ` R ) )
63		mpt0	|- ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) = (/)
64	63	oveq2i	|- ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum (/) )
65	55	gsum0	|- ( R gsum (/) ) = ( 0g ` R )
66	64 65	eqtri	|- ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) = ( 0g ` R )
67	62 66	eqtr4di	|- ( ph -> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) )
68	67	adantr	|- ( ( ph /\ A. x e. (/) M e. B ) -> ( ( coe1 ` ( P gsum ( x e. (/) |-> M ) ) ) ` K ) = ( R gsum ( x e. (/) |-> ( ( coe1 ` M ) ` K ) ) ) )
69	1 2 3 4	coe1fzgsumdlem	|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
70	69	3expia	|- ( ( m e. Fin /\ -. a e. m ) -> ( ph -> ( ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) )
71	70	a2d	|- ( ( m e. Fin /\ -. a e. m ) -> ( ( ph -> ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) ) -> ( ph -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) )
72		impexp	|- ( ( ( ph /\ A. x e. m M e. B ) -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ph -> ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
73		impexp	|- ( ( ( ph /\ A. x e. ( m u. { a } ) M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) <-> ( ph -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
74	71 72 73	3imtr4g	|- ( ( m e. Fin /\ -. a e. m ) -> ( ( ( ph /\ A. x e. m M e. B ) -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( ( ph /\ A. x e. ( m u. { a } ) M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
75	16 26 36 46 68 74	findcard2s	|- ( N e. Fin -> ( ( ph /\ A. x e. N M e. B ) -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) ) )
76	75	expd	|- ( N e. Fin -> ( ph -> ( A. x e. N M e. B -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) ) ) )
77	6 76	mpcom	|- ( ph -> ( A. x e. N M e. B -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) ) )
78	5 77	mpd	|- ( ph -> ( ( coe1 ` ( P gsum ( x e. N |-> M ) ) ) ` K ) = ( R gsum ( x e. N |-> ( ( coe1 ` M ) ` K ) ) ) )