gsummptfsadd

Description: The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019) (Revised by AV, 9-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfsadd.b	$⊢ B = {Base}_{G}$
	gsummptfsadd.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptfsadd.p	$⊢ \underset{˙}{+} = +_{G}$
	gsummptfsadd.g	$⊢ φ \to G \in CMnd$
	gsummptfsadd.a	$⊢ φ \to A \in V$
	gsummptfsadd.c	$⊢ (φ \land x \in A) \to C \in B$
	gsummptfsadd.d	$⊢ (φ \land x \in A) \to D \in B$
	gsummptfsadd.f	$⊢ φ \to F = (x \in A ⟼ C)$
	gsummptfsadd.h	$⊢ φ \to H = (x \in A ⟼ D)$
	gsummptfsadd.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsummptfsadd.v	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
Assertion	gsummptfsadd	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Step	Hyp	Ref	Expression
1		gsummptfsadd.b	$⊢ B = {Base}_{G}$
2		gsummptfsadd.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptfsadd.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsummptfsadd.g	$⊢ φ \to G \in CMnd$
5		gsummptfsadd.a	$⊢ φ \to A \in V$
6		gsummptfsadd.c	$⊢ (φ \land x \in A) \to C \in B$
7		gsummptfsadd.d	$⊢ (φ \land x \in A) \to D \in B$
8		gsummptfsadd.f	$⊢ φ \to F = (x \in A ⟼ C)$
9		gsummptfsadd.h	$⊢ φ \to H = (x \in A ⟼ D)$
10		gsummptfsadd.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
11		gsummptfsadd.v	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
12	5 6 7 8 9	offval2	$⊢ φ \to F {\underset{˙}{+}}_{f} H = (x \in A ⟼ C \underset{˙}{+} D)$
13	12	eqcomd	$⊢ φ \to (x \in A ⟼ C \underset{˙}{+} D) = F {\underset{˙}{+}}_{f} H$
14	13	oveq2d	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D) = \sum_{G} (F {\underset{˙}{+}}_{f} H)$
15	8 6	fmpt3d	$⊢ φ \to F : A ⟶ B$
16	9 7	fmpt3d	$⊢ φ \to H : A ⟶ B$
17	1 2 3 4 5 15 16 10 11	gsumadd	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
18	14 17	eqtrd	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer