# Metamath Proof Explorer

## Theorem gsumunsnfd

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised 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 )`
gsumunsnfd.0
`|- F/_ k Y`
Assertion gsumunsnfd
`|- ( 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 gsumunsnfd.0
` |-  F/_ k Y`
11 snfi
` |-  { M } e. Fin`
12 unfi
` |-  ( ( A e. Fin /\ { M } e. Fin ) -> ( A u. { M } ) e. Fin )`
13 4 11 12 sylancl
` |-  ( ph -> ( A u. { M } ) e. Fin )`
14 elun
` |-  ( k e. ( A u. { M } ) <-> ( k e. A \/ k e. { M } ) )`
15 elsni
` |-  ( k e. { M } -> k = M )`
16 15 9 sylan2
` |-  ( ( ph /\ k e. { M } ) -> X = Y )`
` |-  ( ( ph /\ k e. { M } ) -> Y e. B )`
18 16 17 eqeltrd
` |-  ( ( ph /\ k e. { M } ) -> X e. B )`
19 5 18 jaodan
` |-  ( ( ph /\ ( k e. A \/ k e. { M } ) ) -> X e. B )`
20 14 19 sylan2b
` |-  ( ( ph /\ k e. ( A u. { M } ) ) -> X e. B )`
21 disjsn
` |-  ( ( A i^i { M } ) = (/) <-> -. M e. A )`
22 7 21 sylibr
` |-  ( ph -> ( A i^i { M } ) = (/) )`
23 eqidd
` |-  ( ph -> ( A u. { M } ) = ( A u. { M } ) )`
24 1 2 3 13 20 22 23 gsummptfidmsplit
` |-  ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) )`
25 cmnmnd
` |-  ( G e. CMnd -> G e. Mnd )`
26 3 25 syl
` |-  ( ph -> G e. Mnd )`
27 nfv
` |-  F/ k ph`
28 1 26 6 8 9 27 10 gsumsnfd
` |-  ( ph -> ( G gsum ( k e. { M } |-> X ) ) = Y )`
29 28 oveq2d
` |-  ( ph -> ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`
30 24 29 eqtrd
` |-  ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`