Metamath Proof Explorer

Theorem gsumval2

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 )
Assertion gsumval2 
|- ( 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 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 eqid 
 |-  { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
8 3 adantr 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> G e. V )
9 ovexd 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( M ... N ) e. _V )
10 5 ffnd 
 |-  ( ph -> F Fn ( M ... N ) )
11 10 adantr 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> F Fn ( M ... N ) )
12 simpr 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
13 df-f 
 |-  ( F : ( M ... N ) --> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } <-> ( F Fn ( M ... N ) /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) )
14 11 12 13 sylanbrc 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> F : ( M ... N ) --> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
15 1 6 2 7 8 9 14 gsumval1 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( G gsum F ) = ( 0g ` G ) )
16 simpl 
 |-  ( ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> ( x .+ y ) = y )
17 16 ralimi 
 |-  ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> A. y e. B ( x .+ y ) = y )
18 17 a1i 
 |-  ( x e. B -> ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> A. y e. B ( x .+ y ) = y ) )
19 18 ss2rabi 
 |-  { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { x e. B | A. y e. B ( x .+ y ) = y }
20 fvex 
 |-  ( 0g ` G ) e. _V
21 20 snid 
 |-  ( 0g ` G ) e. { ( 0g ` G ) }
22 5 fdmd 
 |-  ( ph -> dom F = ( M ... N ) )
23 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
24 ne0i 
 |-  ( M e. ( M ... N ) -> ( M ... N ) =/= (/) )
25 4 23 24 3syl 
 |-  ( ph -> ( M ... N ) =/= (/) )
26 22 25 eqnetrd 
 |-  ( ph -> dom F =/= (/) )
27 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
28 27 necon3bii 
 |-  ( dom F =/= (/) <-> ran F =/= (/) )
29 26 28 sylib 
 |-  ( ph -> ran F =/= (/) )
30 29 adantr 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ran F =/= (/) )
31 ssn0 
 |-  ( ( ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } /\ ran F =/= (/) ) -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } =/= (/) )
32 12 30 31 syl2anc 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } =/= (/) )
33 32 neneqd 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> -. { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = (/) )
34 1 6 2 7 mgmidsssn0 
 |-  ( G e. V -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { ( 0g ` G ) } )
35 3 34 syl 
 |-  ( ph -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { ( 0g ` G ) } )
36 sssn 
 |-  ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { ( 0g ` G ) } <-> ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = (/) \/ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = { ( 0g ` G ) } ) )
37 35 36 sylib 
 |-  ( ph -> ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = (/) \/ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = { ( 0g ` G ) } ) )
38 37 orcanai 
 |-  ( ( ph /\ -. { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = (/) ) -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = { ( 0g ` G ) } )
39 33 38 syldan 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } = { ( 0g ` G ) } )
40 21 39 eleqtrrid 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( 0g ` G ) e. { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
41 19 40 sselid 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( 0g ` G ) e. { x e. B | A. y e. B ( x .+ y ) = y } )
42 oveq1 
 |-  ( x = ( 0g ` G ) -> ( x .+ y ) = ( ( 0g ` G ) .+ y ) )
43 42 eqeq1d 
 |-  ( x = ( 0g ` G ) -> ( ( x .+ y ) = y <-> ( ( 0g ` G ) .+ y ) = y ) )
44 43 ralbidv 
 |-  ( x = ( 0g ` G ) -> ( A. y e. B ( x .+ y ) = y <-> A. y e. B ( ( 0g ` G ) .+ y ) = y ) )
45 44 elrab 
 |-  ( ( 0g ` G ) e. { x e. B | A. y e. B ( x .+ y ) = y } <-> ( ( 0g ` G ) e. B /\ A. y e. B ( ( 0g ` G ) .+ y ) = y ) )
46 oveq2 
 |-  ( y = ( 0g ` G ) -> ( ( 0g ` G ) .+ y ) = ( ( 0g ` G ) .+ ( 0g ` G ) ) )
47 id 
 |-  ( y = ( 0g ` G ) -> y = ( 0g ` G ) )
48 46 47 eqeq12d 
 |-  ( y = ( 0g ` G ) -> ( ( ( 0g ` G ) .+ y ) = y <-> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) ) )
49 48 rspcva 
 |-  ( ( ( 0g ` G ) e. B /\ A. y e. B ( ( 0g ` G ) .+ y ) = y ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
50 45 49 sylbi 
 |-  ( ( 0g ` G ) e. { x e. B | A. y e. B ( x .+ y ) = y } -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
51 41 50 syl 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
52 4 adantr 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> N e. ( ZZ>= ` M ) )
53 35 ad2antrr 
 |-  ( ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) /\ z e. ( M ... N ) ) -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { ( 0g ` G ) } )
54 14 ffvelrnda 
 |-  ( ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) /\ z e. ( M ... N ) ) -> ( F ` z ) e. { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
55 53 54 sseldd 
 |-  ( ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) /\ z e. ( M ... N ) ) -> ( F ` z ) e. { ( 0g ` G ) } )
56 elsni 
 |-  ( ( F ` z ) e. { ( 0g ` G ) } -> ( F ` z ) = ( 0g ` G ) )
57 55 56 syl 
 |-  ( ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) /\ z e. ( M ... N ) ) -> ( F ` z ) = ( 0g ` G ) )
58 51 52 57 seqid3 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( seq M ( .+ , F ) ` N ) = ( 0g ` G ) )
59 15 58 eqtr4d 
 |-  ( ( ph /\ ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( G gsum F ) = ( seq M ( .+ , F ) ` N ) )
60 3 adantr 
 |-  ( ( ph /\ -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> G e. V )
61 4 adantr 
 |-  ( ( ph /\ -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> N e. ( ZZ>= ` M ) )
62 5 adantr 
 |-  ( ( ph /\ -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> F : ( M ... N ) --> B )
63 simpr 
 |-  ( ( ph /\ -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
64 1 2 60 61 62 7 63 gsumval2a 
 |-  ( ( ph /\ -. ran F C_ { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) -> ( G gsum F ) = ( seq M ( .+ , F ) ` N ) )
65 59 64 pm2.61dan 
 |-  ( ph -> ( G gsum F ) = ( seq M ( .+ , F ) ` N ) )