This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
20 11 adantr 
 |-  ( ( 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 ) )
26 11 adantr 
 |-  ( ( 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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 ) )