Metamath Proof Explorer


Theorem gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumdifsnd.b
|- B = ( Base ` G )
gsumdifsnd.p
|- .+ = ( +g ` G )
gsumdifsnd.g
|- ( ph -> G e. CMnd )
gsumdifsnd.a
|- ( ph -> A e. W )
gsumdifsnd.f
|- ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )
gsumdifsnd.e
|- ( ( ph /\ k e. A ) -> X e. B )
gsumdifsnd.m
|- ( ph -> M e. A )
gsumdifsnd.y
|- ( ph -> Y e. B )
gsumdifsnd.s
|- ( ( ph /\ k = M ) -> X = Y )
Assertion gsumdifsnd
|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )

Proof

Step Hyp Ref Expression
1 gsumdifsnd.b
 |-  B = ( Base ` G )
2 gsumdifsnd.p
 |-  .+ = ( +g ` G )
3 gsumdifsnd.g
 |-  ( ph -> G e. CMnd )
4 gsumdifsnd.a
 |-  ( ph -> A e. W )
5 gsumdifsnd.f
 |-  ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )
6 gsumdifsnd.e
 |-  ( ( ph /\ k e. A ) -> X e. B )
7 gsumdifsnd.m
 |-  ( ph -> M e. A )
8 gsumdifsnd.y
 |-  ( ph -> Y e. B )
9 gsumdifsnd.s
 |-  ( ( ph /\ k = M ) -> X = Y )
10 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
11 7 snssd
 |-  ( ph -> { M } C_ A )
12 difin2
 |-  ( { M } C_ A -> ( { M } \ { M } ) = ( ( A \ { M } ) i^i { M } ) )
13 11 12 syl
 |-  ( ph -> ( { M } \ { M } ) = ( ( A \ { M } ) i^i { M } ) )
14 difid
 |-  ( { M } \ { M } ) = (/)
15 13 14 eqtr3di
 |-  ( ph -> ( ( A \ { M } ) i^i { M } ) = (/) )
16 difsnid
 |-  ( M e. A -> ( ( A \ { M } ) u. { M } ) = A )
17 7 16 syl
 |-  ( ph -> ( ( A \ { M } ) u. { M } ) = A )
18 17 eqcomd
 |-  ( ph -> A = ( ( A \ { M } ) u. { M } ) )
19 1 10 2 3 4 6 5 15 18 gsumsplit2
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) )
20 cmnmnd
 |-  ( G e. CMnd -> G e. Mnd )
21 3 20 syl
 |-  ( ph -> G e. Mnd )
22 1 21 7 8 9 gsumsnd
 |-  ( ph -> ( G gsum ( k e. { M } |-> X ) ) = Y )
23 22 oveq2d
 |-  ( ph -> ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )
24 19 23 eqtrd
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )