Metamath Proof Explorer


Theorem gsumzcl

Description: Closure of a finite group sum. (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 ) )
gsumzcl.w
|- ( ph -> F finSupp .0. )
Assertion gsumzcl
|- ( 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 gsumzcl.w
 |-  ( ph -> F finSupp .0. )
9 8 fsuppimpd
 |-  ( ph -> ( F supp .0. ) e. Fin )
10 1 2 3 4 5 6 7 9 gsumzcl2
 |-  ( ph -> ( G gsum F ) e. B )