This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )