gsummptfssub

Description: The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019)

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

Step	Hyp	Ref	Expression
1		gsummptfssub.b	$⊢ B = {Base}_{G}$
2		gsummptfssub.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptfssub.s	$⊢ \underset{˙}{-} = -_{G}$
4		gsummptfssub.g	$⊢ φ \to G \in Abel$
5		gsummptfssub.a	$⊢ φ \to A \in V$
6		gsummptfssub.c	$⊢ (φ \land x \in A) \to C \in B$
7		gsummptfssub.d	$⊢ (φ \land x \in A) \to D \in B$
8		gsummptfssub.f	$⊢ φ \to F = (x \in A ⟼ C)$
9		gsummptfssub.h	$⊢ φ \to H = (x \in A ⟼ D)$
10		gsummptfssub.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
11		gsummptfssub.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	gsumsub	$⊢ φ \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