Theorem 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	|- .- = ( -g ` G )
	gsummptfidmsub.g	|- ( ph -> G e. Abel )
	gsummptfidmsub.a	|- ( ph -> A e. Fin )
	gsummptfidmsub.c	|- ( ( ph /\ x e. A ) -> C e. B )
	gsummptfidmsub.d	|- ( ( ph /\ x e. A ) -> D e. B )
	gsummptfidmsub.f	|- F = ( x e. A |-> C )
	gsummptfidmsub.h	|- H = ( x e. A |-> D )
Assertion	gsummptfidmsub	|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsub.b	|- B = ( Base ` G )
2		gsummptfidmsub.s	|- .- = ( -g ` G )
3		gsummptfidmsub.g	|- ( ph -> G e. Abel )
4		gsummptfidmsub.a	|- ( ph -> A e. Fin )
5		gsummptfidmsub.c	|- ( ( ph /\ x e. A ) -> C e. B )
6		gsummptfidmsub.d	|- ( ( ph /\ x e. A ) -> D e. B )
7		gsummptfidmsub.f	|- F = ( x e. A |-> C )
8		gsummptfidmsub.h	|- H = ( x e. A |-> D )
9		eqid	|- ( 0g ` G ) = ( 0g ` G )
10	7	a1i	|- ( ph -> F = ( x e. A |-> C ) )
11	8	a1i	|- ( ph -> H = ( x e. A |-> D ) )
12		fvexd	|- ( ph -> ( 0g ` G ) e. _V )
13	7 4 5 12	fsuppmptdm	|- ( ph -> F finSupp ( 0g ` G ) )
14	8 4 6 12	fsuppmptdm	|- ( ph -> H finSupp ( 0g ` G ) )
15	1 9 2 3 4 5 6 10 11 13 14	gsummptfssub	|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )