Metamath Proof Explorer


Theorem gsumsplit2

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumsplit2.b
|- B = ( Base ` G )
gsumsplit2.z
|- .0. = ( 0g ` G )
gsumsplit2.p
|- .+ = ( +g ` G )
gsumsplit2.g
|- ( ph -> G e. CMnd )
gsumsplit2.a
|- ( ph -> A e. V )
gsumsplit2.f
|- ( ( ph /\ k e. A ) -> X e. B )
gsumsplit2.w
|- ( ph -> ( k e. A |-> X ) finSupp .0. )
gsumsplit2.i
|- ( ph -> ( C i^i D ) = (/) )
gsumsplit2.u
|- ( ph -> A = ( C u. D ) )
Assertion gsumsplit2
|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumsplit2.b
 |-  B = ( Base ` G )
2 gsumsplit2.z
 |-  .0. = ( 0g ` G )
3 gsumsplit2.p
 |-  .+ = ( +g ` G )
4 gsumsplit2.g
 |-  ( ph -> G e. CMnd )
5 gsumsplit2.a
 |-  ( ph -> A e. V )
6 gsumsplit2.f
 |-  ( ( ph /\ k e. A ) -> X e. B )
7 gsumsplit2.w
 |-  ( ph -> ( k e. A |-> X ) finSupp .0. )
8 gsumsplit2.i
 |-  ( ph -> ( C i^i D ) = (/) )
9 gsumsplit2.u
 |-  ( ph -> A = ( C u. D ) )
10 6 fmpttd
 |-  ( ph -> ( k e. A |-> X ) : A --> B )
11 1 2 3 4 5 10 7 8 9 gsumsplit
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( ( k e. A |-> X ) |` C ) ) .+ ( G gsum ( ( k e. A |-> X ) |` D ) ) ) )
12 ssun1
 |-  C C_ ( C u. D )
13 12 9 sseqtrrid
 |-  ( ph -> C C_ A )
14 13 resmptd
 |-  ( ph -> ( ( k e. A |-> X ) |` C ) = ( k e. C |-> X ) )
15 14 oveq2d
 |-  ( ph -> ( G gsum ( ( k e. A |-> X ) |` C ) ) = ( G gsum ( k e. C |-> X ) ) )
16 ssun2
 |-  D C_ ( C u. D )
17 16 9 sseqtrrid
 |-  ( ph -> D C_ A )
18 17 resmptd
 |-  ( ph -> ( ( k e. A |-> X ) |` D ) = ( k e. D |-> X ) )
19 18 oveq2d
 |-  ( ph -> ( G gsum ( ( k e. A |-> X ) |` D ) ) = ( G gsum ( k e. D |-> X ) ) )
20 15 19 oveq12d
 |-  ( ph -> ( ( G gsum ( ( k e. A |-> X ) |` C ) ) .+ ( G gsum ( ( k e. A |-> X ) |` D ) ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )
21 11 20 eqtrd
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )