Theorem gsummptfidmadd2

Description: The sum of two group sums expressed as mappings with finite domain, using a function operation. (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	gsummptfidmadd2	|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( 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	7	a1i	|- ( ph -> F = ( x e. A |-> C ) )
10	8	a1i	|- ( ph -> H = ( x e. A |-> D ) )
11	4 5 6 9 10	offval2	|- ( ph -> ( F oF .+ H ) = ( x e. A |-> ( C .+ D ) ) )
12	11	oveq2d	|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( G gsum ( x e. A |-> ( C .+ D ) ) ) )
13	1 2 3 4 5 6 7 8	gsummptfidmadd	|- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )
14	12 13	eqtrd	|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )