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

Metamath Proof Explorer

Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

		Ref	Expression
	Hypotheses	gsumadd.b	$⊢ B = {Base}_{G}$
		gsumadd.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsumadd.p	$⊢ \underset{˙}{+} = +_{G}$
		gsumadd.g	$⊢ φ \to G \in CMnd$
		gsumadd.a	$⊢ φ \to A \in V$
		gsumadd.f	$⊢ φ \to F : A ⟶ B$
		gsumadd.h	$⊢ φ \to H : A ⟶ B$
		gsumadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
		gsumadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
	Assertion	gsumadd	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Proof

Step	Hyp	Ref	Expression
1		gsumadd.b	$⊢ B = {Base}_{G}$
2		gsumadd.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumadd.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumadd.g	$⊢ φ \to G \in CMnd$
5		gsumadd.a	$⊢ φ \to A \in V$
6		gsumadd.f	$⊢ φ \to F : A ⟶ B$
7		gsumadd.h	$⊢ φ \to H : A ⟶ B$
8		gsumadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
9		gsumadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
10		eqid	$⊢ Cntz (G) = Cntz (G)$
11		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
12	4 11	syl	$⊢ φ \to G \in Mnd$
13	1	submid	$⊢ G \in Mnd \to B \in SubMnd (G)$
14	12 13	syl	$⊢ φ \to B \in SubMnd (G)$
15		ssid	$⊢ B \subseteq B$
16	1 10	cntzcmn	$⊢ (G \in CMnd \land B \subseteq B) \to Cntz (G) (B) = B$
17	4 15 16	sylancl	$⊢ φ \to Cntz (G) (B) = B$
18	15 17	sseqtrrid	$⊢ φ \to B \subseteq Cntz (G) (B)$
19	1 2 3 10 12 5 8 9 14 18 6 7	gsumzadd	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$