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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptcl.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
gsummptcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 )
gsummptfif1o.f ⊢ 𝐹 = ( 𝑖 ∈ 𝑁 ↦ 𝑋 )
gsummptfif1o.h ⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝑁 )
Assertion gsummptfif1o ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptcl.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 gsummptcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
4 gsummptcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 )
5 gsummptfif1o.f ⊢ 𝐹 = ( 𝑖 ∈ 𝑁 ↦ 𝑋 )
6 gsummptfif1o.h ⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝑁 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 5 fmpt ⊢ ( ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 ↔ 𝐹 : 𝑁 ⟶ 𝐵 )
9 4 8 sylib ⊢ ( 𝜑 → 𝐹 : 𝑁 ⟶ 𝐵 )
10 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
11 9 3 10 fdmfifsupp ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
12 1 7 2 3 9 11 6 gsumf1o ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )