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