Metamath Proof Explorer

Theorem gsumzcl2

Description: Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl , because it is not required that F is a function (actually, the hypothesis always holds for any proper class F ). (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-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 ) )
gsumzcl2.w 
|- ( ph -> ( F supp .0. ) e. Fin )
Assertion gsumzcl2 
|- ( ph -> ( G gsum F ) e. B )

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 gsumzcl2.w 
 |-  ( ph -> ( F supp .0. ) e. Fin )
9 2 fvexi 
 |-  .0. e. _V
10 9 a1i 
 |-  ( ph -> .0. e. _V )
11 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
12 6 5 10 11 gsumcllem 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> F = ( k e. A |-> .0. ) )
13 12 oveq2d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .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 15 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
17 13 16 eqtrd 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = .0. )
18 1 2 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
19 4 18 syl 
 |-  ( ph -> .0. e. B )
20 19 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> .0. e. B )
21 17 20 eqeltrd 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) e. B )
22 21 ex 
 |-  ( ph -> ( ( F supp .0. ) = (/) -> ( G gsum F ) e. B ) )
23 eqid 
 |-  ( +g ` G ) = ( +g ` G )
24 4 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> G e. Mnd )
25 5 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> A e. V )
26 6 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> F : A --> B )
27 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 ) )
28 simprl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. NN )
29 f1of1 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
30 29 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. ) )
31 suppssdm 
 |-  ( F supp .0. ) C_ dom F
32 31 6 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
33 32 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A )
34 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
35 30 33 34 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 )
36 ssid 
 |-  ( F supp .0. ) C_ ( F supp .0. )
37 f1ofo 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) )
38 forn 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
39 37 38 syl 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
40 39 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f = ( F supp .0. ) )
41 36 40 sseqtrrid 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ran f )
42 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
43 1 2 23 3 24 25 26 27 28 35 41 42 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. ) ) ) )
44 nnuz 
 |-  NN = ( ZZ>= ` 1 )
45 28 44 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. ( ZZ>= ` 1 ) )
46 f1f 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A )
47 35 46 syl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A )
48 fco 
 |-  ( ( F : A --> B /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) --> B )
49 26 47 48 syl2anc 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) --> B )
50 49 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) /\ k e. ( 1 ... ( # ` ( F supp .0. ) ) ) ) -> ( ( F o. f ) ` k ) e. B )
51 1 23 mndcl 
 |-  ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k ( +g ` G ) x ) e. B )
52 51 3expb 
 |-  ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k ( +g ` G ) x ) e. B )
53 24 52 sylan 
 |-  ( ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) /\ ( k e. B /\ x e. B ) ) -> ( k ( +g ` G ) x ) e. B )
54 45 50 53 seqcl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) e. B )
55 43 54 eqeltrd 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) e. B )
56 55 expr 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) e. B ) )
57 56 exlimdv 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) e. B ) )
58 57 expimpd 
 |-  ( ph -> ( ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( G gsum F ) e. B ) )
59 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. ) ) ) )
60 8 59 syl 
 |-  ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
61 22 58 60 mpjaod 
 |-  ( ph -> ( G gsum F ) e. B )