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

Metamath Proof Explorer

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	$⊢ B = {Base}_{G}$
		gsumreidx.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsumreidx.g	$⊢ φ \to G \in CMnd$
		gsumreidx.f	$⊢ φ \to F : (M \dots N) ⟶ B$
		gsumreidx.h	$⊢ φ \to H : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$
	Assertion	gsumreidx	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$

Proof

Step	Hyp	Ref	Expression
1		gsumreidx.b	$⊢ B = {Base}_{G}$
2		gsumreidx.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumreidx.g	$⊢ φ \to G \in CMnd$
4		gsumreidx.f	$⊢ φ \to F : (M \dots N) ⟶ B$
5		gsumreidx.h	$⊢ φ \to H : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$
6		ovexd	$⊢ φ \to (M \dots N) \in V$
7		fzfid	$⊢ φ \to (M \dots N) \in Fin$
8	2	fvexi	$⊢ \underset{˙}{0} \in V$
9	8	a1i	$⊢ φ \to \underset{˙}{0} \in V$
10	4 7 9	fdmfifsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
11	1 2 3 6 4 10 5	gsumf1o	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$