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

Metamath Proof Explorer

Theorem gsumf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

		Ref	Expression
	Hypotheses	gsumcl.b	$⊢ B = {Base}_{G}$
		gsumcl.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsumcl.g	$⊢ φ \to G \in CMnd$
		gsumcl.a	$⊢ φ \to A \in V$
		gsumcl.f	$⊢ φ \to F : A ⟶ B$
		gsumcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
		gsumf1o.h	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
	Assertion	gsumf1o	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	$⊢ B = {Base}_{G}$
2		gsumcl.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumcl.g	$⊢ φ \to G \in CMnd$
4		gsumcl.a	$⊢ φ \to A \in V$
5		gsumcl.f	$⊢ φ \to F : A ⟶ B$
6		gsumcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
7		gsumf1o.h	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
8		eqid	$⊢ Cntz (G) = Cntz (G)$
9		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
10	3 9	syl	$⊢ φ \to G \in Mnd$
11	1 8 3 5	cntzcmnf	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
12	1 2 8 10 4 5 11 6 7	gsumzf1o	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$