Metamath Proof Explorer


Theorem gsumval3a

Description: Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014) (Revised by AV, 29-May-2019)

Ref Expression
Hypotheses gsumval3.b
|- B = ( Base ` G )
gsumval3.0
|- .0. = ( 0g ` G )
gsumval3.p
|- .+ = ( +g ` G )
gsumval3.z
|- Z = ( Cntz ` G )
gsumval3.g
|- ( ph -> G e. Mnd )
gsumval3.a
|- ( ph -> A e. V )
gsumval3.f
|- ( ph -> F : A --> B )
gsumval3.c
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumval3a.t
|- ( ph -> W e. Fin )
gsumval3a.n
|- ( ph -> W =/= (/) )
gsumval3a.w
|- W = ( F supp .0. )
gsumval3a.i
|- ( ph -> -. A e. ran ... )
Assertion gsumval3a
|- ( ph -> ( G gsum F ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b
 |-  B = ( Base ` G )
2 gsumval3.0
 |-  .0. = ( 0g ` G )
3 gsumval3.p
 |-  .+ = ( +g ` G )
4 gsumval3.z
 |-  Z = ( Cntz ` G )
5 gsumval3.g
 |-  ( ph -> G e. Mnd )
6 gsumval3.a
 |-  ( ph -> A e. V )
7 gsumval3.f
 |-  ( ph -> F : A --> B )
8 gsumval3.c
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
9 gsumval3a.t
 |-  ( ph -> W e. Fin )
10 gsumval3a.n
 |-  ( ph -> W =/= (/) )
11 gsumval3a.w
 |-  W = ( F supp .0. )
12 gsumval3a.i
 |-  ( ph -> -. A e. ran ... )
13 eqid
 |-  { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) }
14 11 a1i
 |-  ( ph -> W = ( F supp .0. ) )
15 7 6 fexd
 |-  ( ph -> F e. _V )
16 2 fvexi
 |-  .0. e. _V
17 suppimacnv
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
18 15 16 17 sylancl
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
19 1 2 3 13 gsumvallem2
 |-  ( G e. Mnd -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } )
20 5 19 syl
 |-  ( ph -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } )
21 20 eqcomd
 |-  ( ph -> { .0. } = { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } )
22 21 difeq2d
 |-  ( ph -> ( _V \ { .0. } ) = ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) )
23 22 imaeq2d
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) )
24 14 18 23 3eqtrd
 |-  ( ph -> W = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) )
25 1 2 3 13 24 5 6 7 gsumval
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
26 20 sseq2d
 |-  ( ph -> ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } <-> ran F C_ { .0. } ) )
27 11 a1i
 |-  ( ( ph /\ ran F C_ { .0. } ) -> W = ( F supp .0. ) )
28 7 6 jca
 |-  ( ph -> ( F : A --> B /\ A e. V ) )
29 28 adantr
 |-  ( ( ph /\ ran F C_ { .0. } ) -> ( F : A --> B /\ A e. V ) )
30 fex
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
31 29 30 syl
 |-  ( ( ph /\ ran F C_ { .0. } ) -> F e. _V )
32 31 16 17 sylancl
 |-  ( ( ph /\ ran F C_ { .0. } ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
33 7 ffnd
 |-  ( ph -> F Fn A )
34 33 adantr
 |-  ( ( ph /\ ran F C_ { .0. } ) -> F Fn A )
35 simpr
 |-  ( ( ph /\ ran F C_ { .0. } ) -> ran F C_ { .0. } )
36 df-f
 |-  ( F : A --> { .0. } <-> ( F Fn A /\ ran F C_ { .0. } ) )
37 34 35 36 sylanbrc
 |-  ( ( ph /\ ran F C_ { .0. } ) -> F : A --> { .0. } )
38 disjdif
 |-  ( { .0. } i^i ( _V \ { .0. } ) ) = (/)
39 fimacnvdisj
 |-  ( ( F : A --> { .0. } /\ ( { .0. } i^i ( _V \ { .0. } ) ) = (/) ) -> ( `' F " ( _V \ { .0. } ) ) = (/) )
40 37 38 39 sylancl
 |-  ( ( ph /\ ran F C_ { .0. } ) -> ( `' F " ( _V \ { .0. } ) ) = (/) )
41 27 32 40 3eqtrd
 |-  ( ( ph /\ ran F C_ { .0. } ) -> W = (/) )
42 41 ex
 |-  ( ph -> ( ran F C_ { .0. } -> W = (/) ) )
43 26 42 sylbid
 |-  ( ph -> ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } -> W = (/) ) )
44 43 necon3ad
 |-  ( ph -> ( W =/= (/) -> -. ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) )
45 10 44 mpd
 |-  ( ph -> -. ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } )
46 45 iffalsed
 |-  ( ph -> if ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) = if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) )
47 12 iffalsed
 |-  ( ph -> if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
48 25 46 47 3eqtrd
 |-  ( ph -> ( G gsum F ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )