Theorem 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	|- .0. = ( 0g ` G )
	gsummptfssub.s	|- .- = ( -g ` G )
	gsummptfssub.g	|- ( ph -> G e. Abel )
	gsummptfssub.a	|- ( ph -> A e. V )
	gsummptfssub.c	|- ( ( ph /\ x e. A ) -> C e. B )
	gsummptfssub.d	|- ( ( ph /\ x e. A ) -> D e. B )
	gsummptfssub.f	|- ( ph -> F = ( x e. A |-> C ) )
	gsummptfssub.h	|- ( ph -> H = ( x e. A |-> D ) )
	gsummptfssub.w	|- ( ph -> F finSupp .0. )
	gsummptfssub.v	|- ( ph -> H finSupp .0. )
Assertion	gsummptfssub	|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfssub.b	|- B = ( Base ` G )
2		gsummptfssub.z	|- .0. = ( 0g ` G )
3		gsummptfssub.s	|- .- = ( -g ` G )
4		gsummptfssub.g	|- ( ph -> G e. Abel )
5		gsummptfssub.a	|- ( ph -> A e. V )
6		gsummptfssub.c	|- ( ( ph /\ x e. A ) -> C e. B )
7		gsummptfssub.d	|- ( ( ph /\ x e. A ) -> D e. B )
8		gsummptfssub.f	|- ( ph -> F = ( x e. A |-> C ) )
9		gsummptfssub.h	|- ( ph -> H = ( x e. A |-> D ) )
10		gsummptfssub.w	|- ( ph -> F finSupp .0. )
11		gsummptfssub.v	|- ( ph -> H finSupp .0. )
12	5 6 7 8 9	offval2	|- ( ph -> ( F oF .- H ) = ( x e. A |-> ( C .- D ) ) )
13	12	eqcomd	|- ( ph -> ( x e. A |-> ( C .- D ) ) = ( F oF .- H ) )
14	13	oveq2d	|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( G gsum ( F oF .- H ) ) )
15	8 6	fmpt3d	|- ( ph -> F : A --> B )
16	9 7	fmpt3d	|- ( ph -> H : A --> B )
17	1 2 3 4 5 15 16 10 11	gsumsub	|- ( ph -> ( G gsum ( F oF .- H ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )
18	14 17	eqtrd	|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )