# Metamath Proof Explorer

## Theorem gsumunsnd

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 2-Jan-2019) (Proof shortened by AV, 11-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 gsumunsnd.b
` |-  B = ( Base ` G )`
2 gsumunsnd.p
` |-  .+ = ( +g ` G )`
3 gsumunsnd.g
` |-  ( ph -> G e. CMnd )`
4 gsumunsnd.a
` |-  ( ph -> A e. Fin )`
5 gsumunsnd.f
` |-  ( ( ph /\ k e. A ) -> X e. B )`
6 gsumunsnd.m
` |-  ( ph -> M e. V )`
7 gsumunsnd.d
` |-  ( ph -> -. M e. A )`
8 gsumunsnd.y
` |-  ( ph -> Y e. B )`
9 gsumunsnd.s
` |-  ( ( ph /\ k = M ) -> X = Y )`
10 nfcv
` |-  F/_ k Y`
11 1 2 3 4 5 6 7 8 9 10 gsumunsnfd
` |-  ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`