Metamath Proof Explorer

Theorem gsumsplit2f

Description: Split a group sum into two parts. (Contributed by AV, 4-Sep-2019)

Ref Expression
Hypotheses gsumsplit2f.n 
|- F/ k ph
gsumsplit2f.b 
|- B = ( Base ` G )
gsumsplit2f.z 
|- .0. = ( 0g ` G )
gsumsplit2f.p 
|- .+ = ( +g ` G )
gsumsplit2f.g 
|- ( ph -> G e. CMnd )
gsumsplit2f.a 
|- ( ph -> A e. V )
gsumsplit2f.f 
|- ( ( ph /\ k e. A ) -> X e. B )
gsumsplit2f.w 
|- ( ph -> ( k e. A |-> X ) finSupp .0. )
gsumsplit2f.i 
|- ( ph -> ( C i^i D ) = (/) )
gsumsplit2f.u 
|- ( ph -> A = ( C u. D ) )
Assertion gsumsplit2f 
|- ( 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 gsumsplit2f.n 
 |-  F/ k ph
2 gsumsplit2f.b 
 |-  B = ( Base ` G )
3 gsumsplit2f.z 
 |-  .0. = ( 0g ` G )
4 gsumsplit2f.p 
 |-  .+ = ( +g ` G )
5 gsumsplit2f.g 
 |-  ( ph -> G e. CMnd )
6 gsumsplit2f.a 
 |-  ( ph -> A e. V )
7 gsumsplit2f.f 
 |-  ( ( ph /\ k e. A ) -> X e. B )
8 gsumsplit2f.w 
 |-  ( ph -> ( k e. A |-> X ) finSupp .0. )
9 gsumsplit2f.i 
 |-  ( ph -> ( C i^i D ) = (/) )
10 gsumsplit2f.u 
 |-  ( ph -> A = ( C u. D ) )
11 eqid 
 |-  ( k e. A |-> X ) = ( k e. A |-> X )
12 1 7 11 fmptdf 
 |-  ( ph -> ( k e. A |-> X ) : A --> B )
13 2 3 4 5 6 12 8 9 10 gsumsplit 
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( ( k e. A |-> X ) |` C ) ) .+ ( G gsum ( ( k e. A |-> X ) |` D ) ) ) )
14 ssun1 
 |-  C C_ ( C u. D )
15 14 10 sseqtrrid 
 |-  ( ph -> C C_ A )
16 15 resmptd 
 |-  ( ph -> ( ( k e. A |-> X ) |` C ) = ( k e. C |-> X ) )
17 16 oveq2d 
 |-  ( ph -> ( G gsum ( ( k e. A |-> X ) |` C ) ) = ( G gsum ( k e. C |-> X ) ) )
18 ssun2 
 |-  D C_ ( C u. D )
19 18 10 sseqtrrid 
 |-  ( ph -> D C_ A )
20 19 resmptd 
 |-  ( ph -> ( ( k e. A |-> X ) |` D ) = ( k e. D |-> X ) )
21 20 oveq2d 
 |-  ( ph -> ( G gsum ( ( k e. A |-> X ) |` D ) ) = ( G gsum ( k e. D |-> X ) ) )
22 17 21 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 ) ) ) )
23 13 22 eqtrd 
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )