gsummptfidmadd2

Description: The sum of two group sums expressed as mappings with finite domain, using a function operation. (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	gsummptfidmadd2	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\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	7	a1i	$⊢ φ \to F = (x \in A ⟼ C)$
10	8	a1i	$⊢ φ \to H = (x \in A ⟼ D)$
11	4 5 6 9 10	offval2	$⊢ φ \to F {\underset{˙}{+}}_{f} H = (x \in A ⟼ C \underset{˙}{+} D)$
12	11	oveq2d	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D)$
13	1 2 3 4 5 6 7 8	gsummptfidmadd	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{+} D) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
14	12 13	eqtrd	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer