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

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 )