Metamath Proof Explorer


Theorem gsummptcl

Description: Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018)

Ref Expression
Hypotheses gsummptcl.b
|- B = ( Base ` G )
gsummptcl.g
|- ( ph -> G e. CMnd )
gsummptcl.n
|- ( ph -> N e. Fin )
gsummptcl.e
|- ( ph -> A. i e. N X e. B )
Assertion gsummptcl
|- ( ph -> ( G gsum ( i e. N |-> X ) ) e. B )

Proof

Step Hyp Ref Expression
1 gsummptcl.b
 |-  B = ( Base ` G )
2 gsummptcl.g
 |-  ( ph -> G e. CMnd )
3 gsummptcl.n
 |-  ( ph -> N e. Fin )
4 gsummptcl.e
 |-  ( ph -> A. i e. N X e. B )
5 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
6 eqid
 |-  ( i e. N |-> X ) = ( i e. N |-> X )
7 6 fmpt
 |-  ( A. i e. N X e. B <-> ( i e. N |-> X ) : N --> B )
8 4 7 sylib
 |-  ( ph -> ( i e. N |-> X ) : N --> B )
9 6 fnmpt
 |-  ( A. i e. N X e. B -> ( i e. N |-> X ) Fn N )
10 4 9 syl
 |-  ( ph -> ( i e. N |-> X ) Fn N )
11 fvexd
 |-  ( ph -> ( 0g ` G ) e. _V )
12 10 3 11 fndmfifsupp
 |-  ( ph -> ( i e. N |-> X ) finSupp ( 0g ` G ) )
13 1 5 2 3 8 12 gsumcl
 |-  ( ph -> ( G gsum ( i e. N |-> X ) ) e. B )