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

Metamath Proof Explorer

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