Theorem gsumreidx

Description: Re-index a finite group sum using a bijection. Corresponds to the first equation in Lang p. 5 with M = 1 . (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumreidx.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumreidx.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumreidx.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumreidx.f	⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
	gsumreidx.h	⊢ ( 𝜑 → 𝐻 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
Assertion	gsumreidx	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumreidx.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumreidx.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumreidx.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsumreidx.f	⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
5		gsumreidx.h	⊢ ( 𝜑 → 𝐻 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
6		ovexd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
7		fzfid	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
8	2	fvexi	⊢ 0 ∈ V
9	8	a1i	⊢ ( 𝜑 → 0 ∈ V )
10	4 7 9	fdmfifsupp	⊢ ( 𝜑 → 𝐹 finSupp 0 )
11	1 2 3 6 4 10 5	gsumf1o	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )