gsummptfidmsub

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

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

Step	Hyp	Ref	Expression
1		gsummptfidmsub.b	$⊢ B = {Base}_{G}$
2		gsummptfidmsub.s	$⊢ \underset{˙}{-} = -_{G}$
3		gsummptfidmsub.g	$⊢ φ \to G \in Abel$
4		gsummptfidmsub.a	$⊢ φ \to A \in Fin$
5		gsummptfidmsub.c	$⊢ (φ \land x \in A) \to C \in B$
6		gsummptfidmsub.d	$⊢ (φ \land x \in A) \to D \in B$
7		gsummptfidmsub.f	$⊢ F = (x \in A ⟼ C)$
8		gsummptfidmsub.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	gsummptfssub	$⊢ φ \to \underset{x \in A}{\sum_{G}} (C \underset{˙}{-} D) = (\sum_{G}, F) \underset{˙}{-} (\sum_{G}, H)$

Metamath Proof Explorer