Metamath Proof Explorer

Theorem gsumzres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

Ref Expression
Hypotheses gsumzcl.b 
|- B = ( Base ` G )
gsumzcl.0 
|- .0. = ( 0g ` G )
gsumzcl.z 
|- Z = ( Cntz ` G )
gsumzcl.g 
|- ( ph -> G e. Mnd )
gsumzcl.a 
|- ( ph -> A e. V )
gsumzcl.f 
|- ( ph -> F : A --> B )
gsumzcl.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzres.s 
|- ( ph -> ( F supp .0. ) C_ W )
gsumzres.w 
|- ( ph -> F finSupp .0. )
Assertion gsumzres 
|- ( ph -> ( G gsum ( F |` W ) ) = ( G gsum F ) )

Proof

Step Hyp Ref Expression
1 gsumzcl.b 
 |-  B = ( Base ` G )
2 gsumzcl.0 
 |-  .0. = ( 0g ` G )
3 gsumzcl.z 
 |-  Z = ( Cntz ` G )
4 gsumzcl.g 
 |-  ( ph -> G e. Mnd )
5 gsumzcl.a 
 |-  ( ph -> A e. V )
6 gsumzcl.f 
 |-  ( ph -> F : A --> B )
7 gsumzcl.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
8 gsumzres.s 
 |-  ( ph -> ( F supp .0. ) C_ W )
9 gsumzres.w 
 |-  ( ph -> F finSupp .0. )
10 inex1g 
 |-  ( A e. V -> ( A i^i W ) e. _V )
11 5 10 syl 
 |-  ( ph -> ( A i^i W ) e. _V )
12 2 gsumz 
 |-  ( ( G e. Mnd /\ ( A i^i W ) e. _V ) -> ( G gsum ( k e. ( A i^i W ) |-> .0. ) ) = .0. )
13 4 11 12 syl2anc 
 |-  ( ph -> ( G gsum ( k e. ( A i^i W ) |-> .0. ) ) = .0. )
14 2 gsumz 
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
15 4 5 14 syl2anc 
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
16 13 15 eqtr4d 
 |-  ( ph -> ( G gsum ( k e. ( A i^i W ) |-> .0. ) ) = ( G gsum ( k e. A |-> .0. ) ) )
17 16 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( k e. ( A i^i W ) |-> .0. ) ) = ( G gsum ( k e. A |-> .0. ) ) )
18 resres 
 |-  ( ( F |` A ) |` W ) = ( F |` ( A i^i W ) )
19 ffn 
 |-  ( F : A --> B -> F Fn A )
20 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
21 6 19 20 3syl 
 |-  ( ph -> ( F |` A ) = F )
22 21 reseq1d 
 |-  ( ph -> ( ( F |` A ) |` W ) = ( F |` W ) )
23 18 22 syl5eqr 
 |-  ( ph -> ( F |` ( A i^i W ) ) = ( F |` W ) )
24 23 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F |` ( A i^i W ) ) = ( F |` W ) )
25 2 fvexi 
 |-  .0. e. _V
26 25 a1i 
 |-  ( ph -> .0. e. _V )
27 ssid 
 |-  ( F supp .0. ) C_ ( F supp .0. )
28 27 a1i 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
29 6 5 26 28 gsumcllem 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> F = ( k e. A |-> .0. ) )
30 29 reseq1d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F |` ( A i^i W ) ) = ( ( k e. A |-> .0. ) |` ( A i^i W ) ) )
31 inss1 
 |-  ( A i^i W ) C_ A
32 resmpt 
 |-  ( ( A i^i W ) C_ A -> ( ( k e. A |-> .0. ) |` ( A i^i W ) ) = ( k e. ( A i^i W ) |-> .0. ) )
33 31 32 ax-mp 
 |-  ( ( k e. A |-> .0. ) |` ( A i^i W ) ) = ( k e. ( A i^i W ) |-> .0. )
34 30 33 syl6eq 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F |` ( A i^i W ) ) = ( k e. ( A i^i W ) |-> .0. ) )
35 24 34 eqtr3d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F |` W ) = ( k e. ( A i^i W ) |-> .0. ) )
36 35 oveq2d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( F |` W ) ) = ( G gsum ( k e. ( A i^i W ) |-> .0. ) ) )
37 29 oveq2d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) )
38 17 36 37 3eqtr4d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( F |` W ) ) = ( G gsum F ) )
39 38 ex 
 |-  ( ph -> ( ( F supp .0. ) = (/) -> ( G gsum ( F |` W ) ) = ( G gsum F ) ) )
40 f1ofo 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) )
41 forn 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
42 40 41 syl 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
43 42 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f = ( F supp .0. ) )
44 8 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ W )
45 43 44 eqsstrd 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f C_ W )
46 cores 
 |-  ( ran f C_ W -> ( ( F |` W ) o. f ) = ( F o. f ) )
47 45 46 syl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( F |` W ) o. f ) = ( F o. f ) )
48 47 seqeq3d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> seq 1 ( ( +g ` G ) , ( ( F |` W ) o. f ) ) = seq 1 ( ( +g ` G ) , ( F o. f ) ) )
49 48 fveq1d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( seq 1 ( ( +g ` G ) , ( ( F |` W ) o. f ) ) ` ( # ` ( F supp .0. ) ) ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) )
50 eqid 
 |-  ( +g ` G ) = ( +g ` G )
51 4 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> G e. Mnd )
52 11 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( A i^i W ) e. _V )
53 6 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> F : A --> B )
54 fssres 
 |-  ( ( F : A --> B /\ ( A i^i W ) C_ A ) -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
55 53 31 54 sylancl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
56 23 feq1d 
 |-  ( ph -> ( ( F |` ( A i^i W ) ) : ( A i^i W ) --> B <-> ( F |` W ) : ( A i^i W ) --> B ) )
57 56 biimpa 
 |-  ( ( ph /\ ( F |` ( A i^i W ) ) : ( A i^i W ) --> B ) -> ( F |` W ) : ( A i^i W ) --> B )
58 55 57 syldan 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F |` W ) : ( A i^i W ) --> B )
59 resss 
 |-  ( F |` W ) C_ F
60 59 rnssi 
 |-  ran ( F |` W ) C_ ran F
61 3 cntzidss 
 |-  ( ( ran F C_ ( Z ` ran F ) /\ ran ( F |` W ) C_ ran F ) -> ran ( F |` W ) C_ ( Z ` ran ( F |` W ) ) )
62 7 60 61 sylancl 
 |-  ( ph -> ran ( F |` W ) C_ ( Z ` ran ( F |` W ) ) )
63 62 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran ( F |` W ) C_ ( Z ` ran ( F |` W ) ) )
64 simprl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. NN )
65 f1of1 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
66 65 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
67 suppssdm 
 |-  ( F supp .0. ) C_ dom F
68 67 6 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
69 68 8 ssind 
 |-  ( ph -> ( F supp .0. ) C_ ( A i^i W ) )
70 69 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ( A i^i W ) )
71 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ ( A i^i W ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( A i^i W ) )
72 66 70 71 syl2anc 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( A i^i W ) )
73 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
74 6 5 73 syl2anc 
 |-  ( ph -> F e. _V )
75 ressuppss 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` W ) supp .0. ) C_ ( F supp .0. ) )
76 74 25 75 sylancl 
 |-  ( ph -> ( ( F |` W ) supp .0. ) C_ ( F supp .0. ) )
77 sseq2 
 |-  ( ran f = ( F supp .0. ) -> ( ( ( F |` W ) supp .0. ) C_ ran f <-> ( ( F |` W ) supp .0. ) C_ ( F supp .0. ) ) )
78 76 77 syl5ibr 
 |-  ( ran f = ( F supp .0. ) -> ( ph -> ( ( F |` W ) supp .0. ) C_ ran f ) )
79 40 41 78 3syl 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( ph -> ( ( F |` W ) supp .0. ) C_ ran f ) )
80 79 adantl 
 |-  ( ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( ph -> ( ( F |` W ) supp .0. ) C_ ran f ) )
81 80 impcom 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( F |` W ) supp .0. ) C_ ran f )
82 eqid 
 |-  ( ( ( F |` W ) o. f ) supp .0. ) = ( ( ( F |` W ) o. f ) supp .0. )
83 1 2 50 3 51 52 58 63 64 72 81 82 gsumval3 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum ( F |` W ) ) = ( seq 1 ( ( +g ` G ) , ( ( F |` W ) o. f ) ) ` ( # ` ( F supp .0. ) ) ) )
84 5 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> A e. V )
85 7 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran F C_ ( Z ` ran F ) )
86 68 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A )
87 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
88 66 86 87 syl2anc 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
89 27 43 sseqtrrid 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ran f )
90 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
91 1 2 50 3 51 84 53 85 64 88 89 90 gsumval3 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) )
92 49 83 91 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum ( F |` W ) ) = ( G gsum F ) )
93 92 expr 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum ( F |` W ) ) = ( G gsum F ) ) )
94 93 exlimdv 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum ( F |` W ) ) = ( G gsum F ) ) )
95 94 expimpd 
 |-  ( ph -> ( ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( G gsum ( F |` W ) ) = ( G gsum F ) ) )
96 fsuppimp 
 |-  ( F finSupp .0. -> ( Fun F /\ ( F supp .0. ) e. Fin ) )
97 96 simprd 
 |-  ( F finSupp .0. -> ( F supp .0. ) e. Fin )
98 fz1f1o 
 |-  ( ( F supp .0. ) e. Fin -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
99 9 97 98 3syl 
 |-  ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
100 39 95 99 mpjaod 
 |-  ( ph -> ( G gsum ( F |` W ) ) = ( G gsum F ) )