Metamath Proof Explorer

Theorem gsumval2a

Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval2.b 
|- B = ( Base ` G )
gsumval2.p 
|- .+ = ( +g ` G )
gsumval2.g 
|- ( ph -> G e. V )
gsumval2.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
gsumval2.f 
|- ( ph -> F : ( M ... N ) --> B )
gsumval2a.o 
|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
gsumval2a.f 
|- ( ph -> -. ran F C_ O )
Assertion gsumval2a 
|- ( ph -> ( G gsum F ) = ( seq M ( .+ , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 gsumval2.b 
 |-  B = ( Base ` G )
2 gsumval2.p 
 |-  .+ = ( +g ` G )
3 gsumval2.g 
 |-  ( ph -> G e. V )
4 gsumval2.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 gsumval2.f 
 |-  ( ph -> F : ( M ... N ) --> B )
6 gsumval2a.o 
 |-  O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
7 gsumval2a.f 
 |-  ( ph -> -. ran F C_ O )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 eqidd 
 |-  ( ph -> ( `' F " ( _V \ O ) ) = ( `' F " ( _V \ O ) ) )
10 ovexd 
 |-  ( ph -> ( M ... N ) e. _V )
11 1 8 2 6 9 3 10 5 gsumval 
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ O , ( 0g ` G ) , if ( ( M ... N ) e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) )
12 7 iffalsed 
 |-  ( ph -> if ( ran F C_ O , ( 0g ` G ) , if ( ( M ... N ) e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) = if ( ( M ... N ) e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) )
13 fzf 
 |-  ... : ( ZZ X. ZZ ) --> ~P ZZ
14 ffn 
 |-  ( ... : ( ZZ X. ZZ ) --> ~P ZZ -> ... Fn ( ZZ X. ZZ ) )
15 13 14 ax-mp 
 |-  ... Fn ( ZZ X. ZZ )
16 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
17 4 16 syl 
 |-  ( ph -> M e. ZZ )
18 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
19 4 18 syl 
 |-  ( ph -> N e. ZZ )
20 fnovrn 
 |-  ( ( ... Fn ( ZZ X. ZZ ) /\ M e. ZZ /\ N e. ZZ ) -> ( M ... N ) e. ran ... )
21 15 17 19 20 mp3an2i 
 |-  ( ph -> ( M ... N ) e. ran ... )
22 21 iftrued 
 |-  ( ph -> if ( ( M ... N ) e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) = ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) )
23 12 22 eqtrd 
 |-  ( ph -> if ( ran F C_ O , ( 0g ` G ) , if ( ( M ... N ) e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) = ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) )
24 11 23 eqtrd 
 |-  ( ph -> ( G gsum F ) = ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) )
25 fvex 
 |-  ( seq M ( .+ , F ) ` N ) e. _V
26 fzopth 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) = ( m ... n ) <-> ( M = m /\ N = n ) ) )
27 4 26 syl 
 |-  ( ph -> ( ( M ... N ) = ( m ... n ) <-> ( M = m /\ N = n ) ) )
28 simpl 
 |-  ( ( M = m /\ N = n ) -> M = m )
29 28 seqeq1d 
 |-  ( ( M = m /\ N = n ) -> seq M ( .+ , F ) = seq m ( .+ , F ) )
30 simpr 
 |-  ( ( M = m /\ N = n ) -> N = n )
31 29 30 fveq12d 
 |-  ( ( M = m /\ N = n ) -> ( seq M ( .+ , F ) ` N ) = ( seq m ( .+ , F ) ` n ) )
32 31 eqcomd 
 |-  ( ( M = m /\ N = n ) -> ( seq m ( .+ , F ) ` n ) = ( seq M ( .+ , F ) ` N ) )
33 eqeq1 
 |-  ( z = ( seq m ( .+ , F ) ` n ) -> ( z = ( seq M ( .+ , F ) ` N ) <-> ( seq m ( .+ , F ) ` n ) = ( seq M ( .+ , F ) ` N ) ) )
34 32 33 syl5ibrcom 
 |-  ( ( M = m /\ N = n ) -> ( z = ( seq m ( .+ , F ) ` n ) -> z = ( seq M ( .+ , F ) ` N ) ) )
35 27 34 syl6bi 
 |-  ( ph -> ( ( M ... N ) = ( m ... n ) -> ( z = ( seq m ( .+ , F ) ` n ) -> z = ( seq M ( .+ , F ) ` N ) ) ) )
36 35 impd 
 |-  ( ph -> ( ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) -> z = ( seq M ( .+ , F ) ` N ) ) )
37 36 rexlimdvw 
 |-  ( ph -> ( E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) -> z = ( seq M ( .+ , F ) ` N ) ) )
38 37 exlimdv 
 |-  ( ph -> ( E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) -> z = ( seq M ( .+ , F ) ` N ) ) )
39 17 adantr 
 |-  ( ( ph /\ z = ( seq M ( .+ , F ) ` N ) ) -> M e. ZZ )
40 oveq2 
 |-  ( n = N -> ( M ... n ) = ( M ... N ) )
41 40 eqcomd 
 |-  ( n = N -> ( M ... N ) = ( M ... n ) )
42 41 biantrurd 
 |-  ( n = N -> ( z = ( seq M ( .+ , F ) ` n ) <-> ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) ) )
43 fveq2 
 |-  ( n = N -> ( seq M ( .+ , F ) ` n ) = ( seq M ( .+ , F ) ` N ) )
44 43 eqeq2d 
 |-  ( n = N -> ( z = ( seq M ( .+ , F ) ` n ) <-> z = ( seq M ( .+ , F ) ` N ) ) )
45 42 44 bitr3d 
 |-  ( n = N -> ( ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) <-> z = ( seq M ( .+ , F ) ` N ) ) )
46 45 rspcev 
 |-  ( ( N e. ( ZZ>= ` M ) /\ z = ( seq M ( .+ , F ) ` N ) ) -> E. n e. ( ZZ>= ` M ) ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) )
47 4 46 sylan 
 |-  ( ( ph /\ z = ( seq M ( .+ , F ) ` N ) ) -> E. n e. ( ZZ>= ` M ) ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) )
48 fveq2 
 |-  ( m = M -> ( ZZ>= ` m ) = ( ZZ>= ` M ) )
49 oveq1 
 |-  ( m = M -> ( m ... n ) = ( M ... n ) )
50 49 eqeq2d 
 |-  ( m = M -> ( ( M ... N ) = ( m ... n ) <-> ( M ... N ) = ( M ... n ) ) )
51 seqeq1 
 |-  ( m = M -> seq m ( .+ , F ) = seq M ( .+ , F ) )
52 51 fveq1d 
 |-  ( m = M -> ( seq m ( .+ , F ) ` n ) = ( seq M ( .+ , F ) ` n ) )
53 52 eqeq2d 
 |-  ( m = M -> ( z = ( seq m ( .+ , F ) ` n ) <-> z = ( seq M ( .+ , F ) ` n ) ) )
54 50 53 anbi12d 
 |-  ( m = M -> ( ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) ) )
55 48 54 rexeqbidv 
 |-  ( m = M -> ( E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> E. n e. ( ZZ>= ` M ) ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) ) )
56 55 spcegv 
 |-  ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ( ( M ... N ) = ( M ... n ) /\ z = ( seq M ( .+ , F ) ` n ) ) -> E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) )
57 39 47 56 sylc 
 |-  ( ( ph /\ z = ( seq M ( .+ , F ) ` N ) ) -> E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) )
58 57 ex 
 |-  ( ph -> ( z = ( seq M ( .+ , F ) ` N ) -> E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) )
59 38 58 impbid 
 |-  ( ph -> ( E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> z = ( seq M ( .+ , F ) ` N ) ) )
60 59 adantr 
 |-  ( ( ph /\ ( seq M ( .+ , F ) ` N ) e. _V ) -> ( E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> z = ( seq M ( .+ , F ) ` N ) ) )
61 60 iota5 
 |-  ( ( ph /\ ( seq M ( .+ , F ) ` N ) e. _V ) -> ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) = ( seq M ( .+ , F ) ` N ) )
62 25 61 mpan2 
 |-  ( ph -> ( iota z E. m E. n e. ( ZZ>= ` m ) ( ( M ... N ) = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) = ( seq M ( .+ , F ) ` N ) )
63 24 62 eqtrd 
 |-  ( ph -> ( G gsum F ) = ( seq M ( .+ , F ) ` N ) )