Theorem gsummptfsadd

Description: The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019) (Revised by AV, 9-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfsadd.b	|- B = ( Base ` G )
	gsummptfsadd.z	|- .0. = ( 0g ` G )
	gsummptfsadd.p	|- .+ = ( +g ` G )
	gsummptfsadd.g	|- ( ph -> G e. CMnd )
	gsummptfsadd.a	|- ( ph -> A e. V )
	gsummptfsadd.c	|- ( ( ph /\ x e. A ) -> C e. B )
	gsummptfsadd.d	|- ( ( ph /\ x e. A ) -> D e. B )
	gsummptfsadd.f	|- ( ph -> F = ( x e. A |-> C ) )
	gsummptfsadd.h	|- ( ph -> H = ( x e. A |-> D ) )
	gsummptfsadd.w	|- ( ph -> F finSupp .0. )
	gsummptfsadd.v	|- ( ph -> H finSupp .0. )
Assertion	gsummptfsadd	|- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfsadd.b	|- B = ( Base ` G )
2		gsummptfsadd.z	|- .0. = ( 0g ` G )
3		gsummptfsadd.p	|- .+ = ( +g ` G )
4		gsummptfsadd.g	|- ( ph -> G e. CMnd )
5		gsummptfsadd.a	|- ( ph -> A e. V )
6		gsummptfsadd.c	|- ( ( ph /\ x e. A ) -> C e. B )
7		gsummptfsadd.d	|- ( ( ph /\ x e. A ) -> D e. B )
8		gsummptfsadd.f	|- ( ph -> F = ( x e. A |-> C ) )
9		gsummptfsadd.h	|- ( ph -> H = ( x e. A |-> D ) )
10		gsummptfsadd.w	|- ( ph -> F finSupp .0. )
11		gsummptfsadd.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	gsumadd	|- ( 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 ) ) )