Theorem gsummptfidmadd

Description: The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmadd.b	|- B = ( Base ` G )
2		gsummptfidmadd.p	|- .+ = ( +g ` G )
3		gsummptfidmadd.g	|- ( ph -> G e. CMnd )
4		gsummptfidmadd.a	|- ( ph -> A e. Fin )
5		gsummptfidmadd.c	|- ( ( ph /\ x e. A ) -> C e. B )
6		gsummptfidmadd.d	|- ( ( ph /\ x e. A ) -> D e. B )
7		gsummptfidmadd.f	|- F = ( x e. A |-> C )
8		gsummptfidmadd.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	gsummptfsadd	|- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )