gsummptfidmadd

Description: The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019)

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

Step	Hyp	Ref	Expression
1		gsummptfidmadd.b	$⊢ B = {Base}_{G}$
2		gsummptfidmadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsummptfidmadd.g	$⊢ φ \to G \in CMnd$
4		gsummptfidmadd.a	$⊢ φ \to A \in Fin$
5		gsummptfidmadd.c	$⊢ (φ \land x \in A) \to C \in B$
6		gsummptfidmadd.d	$⊢ (φ \land x \in A) \to D \in B$
7		gsummptfidmadd.f	$⊢ F = (x \in A ⟼ C)$
8		gsummptfidmadd.h	$⊢ H = (x \in A ⟼ D)$
9		eqid	$⊢ 0_{G} = 0_{G}$
10	7	a1i	$⊢ φ \to F = (x \in A ⟼ C)$
11	8	a1i	$⊢ φ \to H = (x \in A ⟼ D)$
12		fvexd	$⊢ φ \to 0_{G} \in V$
13	7 4 5 12	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} (F)$
14	8 4 6 12	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} (H)$
15	1 9 2 3 4 5 6 10 11 13 14	gsummptfsadd	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer