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 ⊢ φ → G ∈ CMnd
gsummptcl.n ⊢ φ → N ∈ Fin
gsummptcl.e ⊢ φ → ∀ i ∈ N X ∈ B
Assertion gsummptcl ⊢ φ → ∑ G i ∈ N X ∈ B

Proof

Step Hyp Ref Expression
1 gsummptcl.b ⊢ B = Base G
2 gsummptcl.g ⊢ φ → G ∈ CMnd
3 gsummptcl.n ⊢ φ → N ∈ Fin
4 gsummptcl.e ⊢ φ → ∀ i ∈ N X ∈ B
5 eqid ⊢ 0 G = 0 G
6 eqid ⊢ i ∈ N ⟼ X = i ∈ N ⟼ X
7 6 fmpt ⊢ ∀ i ∈ N X ∈ B ↔ i ∈ N ⟼ X : N ⟶ B
8 4 7 sylib ⊢ φ → i ∈ N ⟼ X : N ⟶ B
9 6 fnmpt ⊢ ∀ i ∈ N X ∈ B → i ∈ N ⟼ X Fn N
10 4 9 syl ⊢ φ → i ∈ N ⟼ X Fn N
11 fvexd ⊢ φ → 0 G ∈ V
12 10 3 11 fndmfifsupp ⊢ φ → finSupp 0 G⁡ i ∈ N ⟼ X
13 1 5 2 3 8 12 gsumcl ⊢ φ → ∑ G i ∈ N X ∈ B