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=BaseG
gsumval2.p +˙=+G
gsumval2.g φGV
gsumval2.n φNM
gsumval2.f φF:MNB
gsumval2a.o O=xB|yBx+˙y=yy+˙x=y
gsumval2a.f φ¬ranFO
Assertion gsumval2a φGF=seqM+˙FN

Proof

Step Hyp Ref Expression
1 gsumval2.b B=BaseG
2 gsumval2.p +˙=+G
3 gsumval2.g φGV
4 gsumval2.n φNM
5 gsumval2.f φF:MNB
6 gsumval2a.o O=xB|yBx+˙y=yy+˙x=y
7 gsumval2a.f φ¬ranFO
8 eqid 0G=0G
9 eqidd φF-1VO=F-1VO
10 ovexd φMNV
11 1 8 2 6 9 3 10 5 gsumval φGF=ifranFO0GifMNranιz|mnmMN=mnz=seqm+˙Fnιz|ff:1F-1VO1-1 ontoF-1VOz=seq1+˙FfF-1VO
12 7 iffalsed φifranFO0GifMNranιz|mnmMN=mnz=seqm+˙Fnιz|ff:1F-1VO1-1 ontoF-1VOz=seq1+˙FfF-1VO=ifMNranιz|mnmMN=mnz=seqm+˙Fnιz|ff:1F-1VO1-1 ontoF-1VOz=seq1+˙FfF-1VO
13 fzf :×𝒫
14 ffn :×𝒫Fn×
15 13 14 ax-mp Fn×
16 eluzel2 NMM
17 4 16 syl φM
18 eluzelz NMN
19 4 18 syl φN
20 fnovrn Fn×MNMNran
21 15 17 19 20 mp3an2i φMNran
22 21 iftrued φifMNranιz|mnmMN=mnz=seqm+˙Fnιz|ff:1F-1VO1-1 ontoF-1VOz=seq1+˙FfF-1VO=ιz|mnmMN=mnz=seqm+˙Fn
23 12 22 eqtrd φifranFO0GifMNranιz|mnmMN=mnz=seqm+˙Fnιz|ff:1F-1VO1-1 ontoF-1VOz=seq1+˙FfF-1VO=ιz|mnmMN=mnz=seqm+˙Fn
24 11 23 eqtrd φGF=ιz|mnmMN=mnz=seqm+˙Fn
25 fvex seqM+˙FNV
26 fzopth NMMN=mnM=mN=n
27 4 26 syl φMN=mnM=mN=n
28 simpl M=mN=nM=m
29 28 seqeq1d M=mN=nseqM+˙F=seqm+˙F
30 simpr M=mN=nN=n
31 29 30 fveq12d M=mN=nseqM+˙FN=seqm+˙Fn
32 31 eqcomd M=mN=nseqm+˙Fn=seqM+˙FN
33 eqeq1 z=seqm+˙Fnz=seqM+˙FNseqm+˙Fn=seqM+˙FN
34 32 33 syl5ibrcom M=mN=nz=seqm+˙Fnz=seqM+˙FN
35 27 34 syl6bi φMN=mnz=seqm+˙Fnz=seqM+˙FN
36 35 impd φMN=mnz=seqm+˙Fnz=seqM+˙FN
37 36 rexlimdvw φnmMN=mnz=seqm+˙Fnz=seqM+˙FN
38 37 exlimdv φmnmMN=mnz=seqm+˙Fnz=seqM+˙FN
39 17 adantr φz=seqM+˙FNM
40 oveq2 n=NMn=MN
41 40 eqcomd n=NMN=Mn
42 41 biantrurd n=Nz=seqM+˙FnMN=Mnz=seqM+˙Fn
43 fveq2 n=NseqM+˙Fn=seqM+˙FN
44 43 eqeq2d n=Nz=seqM+˙Fnz=seqM+˙FN
45 42 44 bitr3d n=NMN=Mnz=seqM+˙Fnz=seqM+˙FN
46 45 rspcev NMz=seqM+˙FNnMMN=Mnz=seqM+˙Fn
47 4 46 sylan φz=seqM+˙FNnMMN=Mnz=seqM+˙Fn
48 fveq2 m=Mm=M
49 oveq1 m=Mmn=Mn
50 49 eqeq2d m=MMN=mnMN=Mn
51 seqeq1 m=Mseqm+˙F=seqM+˙F
52 51 fveq1d m=Mseqm+˙Fn=seqM+˙Fn
53 52 eqeq2d m=Mz=seqm+˙Fnz=seqM+˙Fn
54 50 53 anbi12d m=MMN=mnz=seqm+˙FnMN=Mnz=seqM+˙Fn
55 48 54 rexeqbidv m=MnmMN=mnz=seqm+˙FnnMMN=Mnz=seqM+˙Fn
56 55 spcegv MnMMN=Mnz=seqM+˙FnmnmMN=mnz=seqm+˙Fn
57 39 47 56 sylc φz=seqM+˙FNmnmMN=mnz=seqm+˙Fn
58 57 ex φz=seqM+˙FNmnmMN=mnz=seqm+˙Fn
59 38 58 impbid φmnmMN=mnz=seqm+˙Fnz=seqM+˙FN
60 59 adantr φseqM+˙FNVmnmMN=mnz=seqm+˙Fnz=seqM+˙FN
61 60 iota5 φseqM+˙FNVιz|mnmMN=mnz=seqm+˙Fn=seqM+˙FN
62 25 61 mpan2 φιz|mnmMN=mnz=seqm+˙Fn=seqM+˙FN
63 24 62 eqtrd φGF=seqM+˙FN