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

Metamath Proof Explorer

Theorem gsummhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

		Ref	Expression
	Hypotheses	gsummhm.b	$⊢ B = {Base}_{G}$
		gsummhm.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsummhm.g	$⊢ φ \to G \in CMnd$
		gsummhm.h	$⊢ φ \to H \in Mnd$
		gsummhm.a	$⊢ φ \to A \in V$
		gsummhm.k	$⊢ φ \to K \in (G MndHom H)$
		gsummhm.f	$⊢ φ \to F : A ⟶ B$
		gsummhm.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	Assertion	gsummhm	$⊢ φ \to \sum_{H} (K \circ F) = K (\sum_{G} F)$

Proof

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