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

Metamath Proof Explorer

Theorem gsuminv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 4-May-2015) (Revised by AV, 6-Jun-2019)

		Ref	Expression
	Hypotheses	gsuminv.b	$⊢ B = {Base}_{G}$
		gsuminv.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsuminv.p	$⊢ I = {inv}_{g} (G)$
		gsuminv.g	$⊢ φ \to G \in Abel$
		gsuminv.a	$⊢ φ \to A \in V$
		gsuminv.f	$⊢ φ \to F : A ⟶ B$
		gsuminv.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	Assertion	gsuminv	$⊢ φ \to \sum_{G} (I \circ F) = I (\sum_{G} F)$

Proof

Step	Hyp	Ref	Expression
1		gsuminv.b	$⊢ B = {Base}_{G}$
2		gsuminv.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsuminv.p	$⊢ I = {inv}_{g} (G)$
4		gsuminv.g	$⊢ φ \to G \in Abel$
5		gsuminv.a	$⊢ φ \to A \in V$
6		gsuminv.f	$⊢ φ \to F : A ⟶ B$
7		gsuminv.n	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		ablcmn	$⊢ G \in Abel \to G \in CMnd$
9	4 8	syl	$⊢ φ \to G \in CMnd$
10		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
11	9 10	syl	$⊢ φ \to G \in Mnd$
12	1 3	invghm	$⊢ G \in Abel \leftrightarrow I \in (G GrpHom G)$
13	4 12	sylib	$⊢ φ \to I \in (G GrpHom G)$
14		ghmmhm	$⊢ I \in (G GrpHom G) \to I \in (G MndHom G)$
15	13 14	syl	$⊢ φ \to I \in (G MndHom G)$
16	1 2 9 11 5 15 6 7	gsummhm	$⊢ φ \to \sum_{G} (I \circ F) = I (\sum_{G} F)$