Metamath Proof Explorer


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