This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )