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 ( 𝐹 ∘ 𝐻 ) ) )