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

Metamath Proof Explorer

Theorem gsummptfif1o

Description: Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019)

Ref Expression
Hypotheses gsummptcl.b ⊢ B = Base G
gsummptcl.g ⊢ φ → G ∈ CMnd
gsummptcl.n ⊢ φ → N ∈ Fin
gsummptcl.e ⊢ φ → ∀ i ∈ N X ∈ B
gsummptfif1o.f ⊢ F = i ∈ N ⟼ X
gsummptfif1o.h ⊢ φ → H : C ⟶ 1-1 onto N
Assertion gsummptfif1o ⊢ φ → ∑ G F = ∑ G F ∘ H

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 gsummptfif1o.f ⊢ F = i ∈ N ⟼ X
6 gsummptfif1o.h ⊢ φ → H : C ⟶ 1-1 onto N
7 eqid ⊢ 0 G = 0 G
8 5 fmpt ⊢ ∀ i ∈ N X ∈ B ↔ F : N ⟶ B
9 4 8 sylib ⊢ φ → F : N ⟶ B
10 fvexd ⊢ φ → 0 G ∈ V
11 9 3 10 fdmfifsupp ⊢ φ → finSupp 0 G⁡ F
12 1 7 2 3 9 11 6 gsumf1o ⊢ φ → ∑ G F = ∑ G F ∘ H