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 jca 
 |-  ( ph -> ( F : A --> B /\ A e. V ) )
16 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
17 15 16 syl 
 |-  ( ph -> F e. _V )
18 2 fvexi 
 |-  .0. e. _V
19 suppimacnv 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
20 17 18 19 sylancl 
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
21 1 2 3 13 gsumvallem2 
 |-  ( G e. Mnd -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } )
22 5 21 syl 
 |-  ( ph -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } )
23 22 eqcomd 
 |-  ( ph -> { .0. } = { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } )
24 23 difeq2d 
 |-  ( ph -> ( _V \ { .0. } ) = ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) )
25 24 imaeq2d 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) )
26 14 20 25 3eqtrd 
 |-  ( ph -> W = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) )
27 1 2 3 13 26 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 ) ) ) ) ) ) )
28 22 sseq2d 
 |-  ( ph -> ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } <-> ran F C_ { .0. } ) )
29 11 a1i 
 |-  ( ( ph /\ ran F C_ { .0. } ) -> W = ( F supp .0. ) )
30 15 adantr 
 |-  ( ( ph /\ ran F C_ { .0. } ) -> ( F : A --> B /\ A e. V ) )
31 30 16 syl 
 |-  ( ( ph /\ ran F C_ { .0. } ) -> F e. _V )
32 31 18 19 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 29 32 40 3eqtrd 
 |-  ( ( ph /\ ran F C_ { .0. } ) -> W = (/) )
42 41 ex 
 |-  ( ph -> ( ran F C_ { .0. } -> W = (/) ) )
43 28 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 27 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 ) ) ) ) )