Metamath Proof Explorer


Theorem fsum

Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses fsum.1 k=FnB=C
fsum.2 φM
fsum.3 φF:1M1-1 ontoA
fsum.4 φkAB
fsum.5 φn1MGn=C
Assertion fsum φkAB=seq1+GM

Proof

Step Hyp Ref Expression
1 fsum.1 k=FnB=C
2 fsum.2 φM
3 fsum.3 φF:1M1-1 ontoA
4 fsum.4 φkAB
5 fsum.5 φn1MGn=C
6 df-sum kAB=ιx|mAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm
7 fvex seq1+GMV
8 eleq1w n=jnAjA
9 csbeq1 n=jn/kB=j/kB
10 8 9 ifbieq1d n=jifnAn/kB0=ifjAj/kB0
11 10 cbvmptv nifnAn/kB0=jifjAj/kB0
12 4 ralrimiva φkAB
13 nfcsb1v _kj/kB
14 13 nfel1 kj/kB
15 csbeq1a k=jB=j/kB
16 15 eleq1d k=jBj/kB
17 14 16 rspc jAkABj/kB
18 12 17 mpan9 φjAj/kB
19 fveq2 n=ifn=fi
20 19 csbeq1d n=ifn/kB=fi/kB
21 csbcow fi/jj/kB=fi/kB
22 20 21 eqtr4di n=ifn/kB=fi/jj/kB
23 22 cbvmptv nfn/kB=ifi/jj/kB
24 11 18 23 summo φ*xmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm
25 f1of F:1M1-1 ontoAF:1MA
26 3 25 syl φF:1MA
27 ovex 1MV
28 fex F:1MA1MVFV
29 26 27 28 sylancl φFV
30 nnuz =1
31 2 30 eleqtrdi φM1
32 elfznn n1Mn
33 fvex GnV
34 5 33 eqeltrrdi φn1MCV
35 eqid nC=nC
36 35 fvmpt2 nCVnCn=C
37 32 34 36 syl2an2 φn1MnCn=C
38 5 37 eqtr4d φn1MGn=nCn
39 38 ralrimiva φn1MGn=nCn
40 nffvmpt1 _nnCk
41 40 nfeq2 nGk=nCk
42 fveq2 n=kGn=Gk
43 fveq2 n=knCn=nCk
44 42 43 eqeq12d n=kGn=nCnGk=nCk
45 41 44 rspc k1Mn1MGn=nCnGk=nCk
46 39 45 mpan9 φk1MGk=nCk
47 31 46 seqfveq φseq1+GM=seq1+nCM
48 3 47 jca φF:1M1-1 ontoAseq1+GM=seq1+nCM
49 f1oeq1 f=Ff:1M1-1 ontoAF:1M1-1 ontoA
50 fveq1 f=Ffn=Fn
51 50 csbeq1d f=Ffn/kB=Fn/kB
52 fvex FnV
53 52 1 csbie Fn/kB=C
54 51 53 eqtrdi f=Ffn/kB=C
55 54 mpteq2dv f=Fnfn/kB=nC
56 55 seqeq3d f=Fseq1+nfn/kB=seq1+nC
57 56 fveq1d f=Fseq1+nfn/kBM=seq1+nCM
58 57 eqeq2d f=Fseq1+GM=seq1+nfn/kBMseq1+GM=seq1+nCM
59 49 58 anbi12d f=Ff:1M1-1 ontoAseq1+GM=seq1+nfn/kBMF:1M1-1 ontoAseq1+GM=seq1+nCM
60 29 48 59 spcedv φff:1M1-1 ontoAseq1+GM=seq1+nfn/kBM
61 oveq2 m=M1m=1M
62 61 f1oeq2d m=Mf:1m1-1 ontoAf:1M1-1 ontoA
63 fveq2 m=Mseq1+nfn/kBm=seq1+nfn/kBM
64 63 eqeq2d m=Mseq1+GM=seq1+nfn/kBmseq1+GM=seq1+nfn/kBM
65 62 64 anbi12d m=Mf:1m1-1 ontoAseq1+GM=seq1+nfn/kBmf:1M1-1 ontoAseq1+GM=seq1+nfn/kBM
66 65 exbidv m=Mff:1m1-1 ontoAseq1+GM=seq1+nfn/kBmff:1M1-1 ontoAseq1+GM=seq1+nfn/kBM
67 66 rspcev Mff:1M1-1 ontoAseq1+GM=seq1+nfn/kBMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
68 2 60 67 syl2anc φmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
69 68 olcd φmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
70 breq2 x=seq1+GMseqm+nifnAn/kB0xseqm+nifnAn/kB0seq1+GM
71 70 anbi2d x=seq1+GMAmseqm+nifnAn/kB0xAmseqm+nifnAn/kB0seq1+GM
72 71 rexbidv x=seq1+GMmAmseqm+nifnAn/kB0xmAmseqm+nifnAn/kB0seq1+GM
73 eqeq1 x=seq1+GMx=seq1+nfn/kBmseq1+GM=seq1+nfn/kBm
74 73 anbi2d x=seq1+GMf:1m1-1 ontoAx=seq1+nfn/kBmf:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
75 74 exbidv x=seq1+GMff:1m1-1 ontoAx=seq1+nfn/kBmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
76 75 rexbidv x=seq1+GMmff:1m1-1 ontoAx=seq1+nfn/kBmmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
77 72 76 orbi12d x=seq1+GMmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBm
78 77 moi2 seq1+GMV*xmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBmx=seq1+GM
79 7 78 mpanl1 *xmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBmx=seq1+GM
80 79 ancom2s *xmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBmmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmx=seq1+GM
81 80 expr *xmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kB0seq1+GMmff:1m1-1 ontoAseq1+GM=seq1+nfn/kBmmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmx=seq1+GM
82 24 69 81 syl2anc φmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmx=seq1+GM
83 69 77 syl5ibrcom φx=seq1+GMmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm
84 82 83 impbid φmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmx=seq1+GM
85 84 adantr φseq1+GMVmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmx=seq1+GM
86 85 iota5 φseq1+GMVιx|mAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm=seq1+GM
87 7 86 mpan2 φιx|mAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm=seq1+GM
88 6 87 eqtrid φkAB=seq1+GM