# Metamath Proof Explorer

## Theorem gsumzunsnd

Description: Append an element to a finite group sum, more general version of gsumunsnd . (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses gsumzunsnd.b
`|- B = ( Base ` G )`
gsumzunsnd.p
`|- .+ = ( +g ` G )`
gsumzunsnd.z
`|- Z = ( Cntz ` G )`
gsumzunsnd.f
`|- F = ( k e. ( A u. { M } ) |-> X )`
gsumzunsnd.g
`|- ( ph -> G e. Mnd )`
gsumzunsnd.a
`|- ( ph -> A e. Fin )`
gsumzunsnd.c
`|- ( ph -> ran F C_ ( Z ` ran F ) )`
gsumzunsnd.x
`|- ( ( ph /\ k e. A ) -> X e. B )`
gsumzunsnd.m
`|- ( ph -> M e. V )`
gsumzunsnd.d
`|- ( ph -> -. M e. A )`
gsumzunsnd.y
`|- ( ph -> Y e. B )`
gsumzunsnd.s
`|- ( ( ph /\ k = M ) -> X = Y )`
Assertion gsumzunsnd
`|- ( ph -> ( G gsum F ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`

### Proof

Step Hyp Ref Expression
1 gsumzunsnd.b
` |-  B = ( Base ` G )`
2 gsumzunsnd.p
` |-  .+ = ( +g ` G )`
3 gsumzunsnd.z
` |-  Z = ( Cntz ` G )`
4 gsumzunsnd.f
` |-  F = ( k e. ( A u. { M } ) |-> X )`
5 gsumzunsnd.g
` |-  ( ph -> G e. Mnd )`
6 gsumzunsnd.a
` |-  ( ph -> A e. Fin )`
7 gsumzunsnd.c
` |-  ( ph -> ran F C_ ( Z ` ran F ) )`
8 gsumzunsnd.x
` |-  ( ( ph /\ k e. A ) -> X e. B )`
9 gsumzunsnd.m
` |-  ( ph -> M e. V )`
10 gsumzunsnd.d
` |-  ( ph -> -. M e. A )`
11 gsumzunsnd.y
` |-  ( ph -> Y e. B )`
12 gsumzunsnd.s
` |-  ( ( ph /\ k = M ) -> X = Y )`
13 eqid
` |-  ( 0g ` G ) = ( 0g ` G )`
14 snfi
` |-  { M } e. Fin`
15 unfi
` |-  ( ( A e. Fin /\ { M } e. Fin ) -> ( A u. { M } ) e. Fin )`
16 6 14 15 sylancl
` |-  ( ph -> ( A u. { M } ) e. Fin )`
17 elun
` |-  ( k e. ( A u. { M } ) <-> ( k e. A \/ k e. { M } ) )`
18 elsni
` |-  ( k e. { M } -> k = M )`
19 18 12 sylan2
` |-  ( ( ph /\ k e. { M } ) -> X = Y )`
` |-  ( ( ph /\ k e. { M } ) -> Y e. B )`
21 19 20 eqeltrd
` |-  ( ( ph /\ k e. { M } ) -> X e. B )`
22 8 21 jaodan
` |-  ( ( ph /\ ( k e. A \/ k e. { M } ) ) -> X e. B )`
23 17 22 sylan2b
` |-  ( ( ph /\ k e. ( A u. { M } ) ) -> X e. B )`
24 23 4 fmptd
` |-  ( ph -> F : ( A u. { M } ) --> B )`
25 8 expcom
` |-  ( k e. A -> ( ph -> X e. B ) )`
` |-  ( ( ph /\ k = M ) -> Y e. B )`
27 12 26 eqeltrd
` |-  ( ( ph /\ k = M ) -> X e. B )`
28 27 expcom
` |-  ( k = M -> ( ph -> X e. B ) )`
29 18 28 syl
` |-  ( k e. { M } -> ( ph -> X e. B ) )`
30 25 29 jaoi
` |-  ( ( k e. A \/ k e. { M } ) -> ( ph -> X e. B ) )`
31 17 30 sylbi
` |-  ( k e. ( A u. { M } ) -> ( ph -> X e. B ) )`
32 31 impcom
` |-  ( ( ph /\ k e. ( A u. { M } ) ) -> X e. B )`
33 fvexd
` |-  ( ph -> ( 0g ` G ) e. _V )`
34 4 16 32 33 fsuppmptdm
` |-  ( ph -> F finSupp ( 0g ` G ) )`
35 disjsn
` |-  ( ( A i^i { M } ) = (/) <-> -. M e. A )`
36 10 35 sylibr
` |-  ( ph -> ( A i^i { M } ) = (/) )`
37 eqidd
` |-  ( ph -> ( A u. { M } ) = ( A u. { M } ) )`
38 1 13 2 3 5 16 24 7 34 36 37 gsumzsplit
` |-  ( ph -> ( G gsum F ) = ( ( G gsum ( F |` A ) ) .+ ( G gsum ( F |` { M } ) ) ) )`
39 4 reseq1i
` |-  ( F |` A ) = ( ( k e. ( A u. { M } ) |-> X ) |` A )`
40 ssun1
` |-  A C_ ( A u. { M } )`
41 resmpt
` |-  ( A C_ ( A u. { M } ) -> ( ( k e. ( A u. { M } ) |-> X ) |` A ) = ( k e. A |-> X ) )`
42 40 41 mp1i
` |-  ( ph -> ( ( k e. ( A u. { M } ) |-> X ) |` A ) = ( k e. A |-> X ) )`
43 39 42 syl5eq
` |-  ( ph -> ( F |` A ) = ( k e. A |-> X ) )`
44 43 oveq2d
` |-  ( ph -> ( G gsum ( F |` A ) ) = ( G gsum ( k e. A |-> X ) ) )`
45 4 reseq1i
` |-  ( F |` { M } ) = ( ( k e. ( A u. { M } ) |-> X ) |` { M } )`
46 ssun2
` |-  { M } C_ ( A u. { M } )`
47 resmpt
` |-  ( { M } C_ ( A u. { M } ) -> ( ( k e. ( A u. { M } ) |-> X ) |` { M } ) = ( k e. { M } |-> X ) )`
48 46 47 mp1i
` |-  ( ph -> ( ( k e. ( A u. { M } ) |-> X ) |` { M } ) = ( k e. { M } |-> X ) )`
49 45 48 syl5eq
` |-  ( ph -> ( F |` { M } ) = ( k e. { M } |-> X ) )`
50 49 oveq2d
` |-  ( ph -> ( G gsum ( F |` { M } ) ) = ( G gsum ( k e. { M } |-> X ) ) )`
51 44 50 oveq12d
` |-  ( ph -> ( ( G gsum ( F |` A ) ) .+ ( G gsum ( F |` { M } ) ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) )`
52 1 5 9 11 12 gsumsnd
` |-  ( ph -> ( G gsum ( k e. { M } |-> X ) ) = Y )`
53 52 oveq2d
` |-  ( ph -> ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`
54 38 51 53 3eqtrd
` |-  ( ph -> ( G gsum F ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )`