Metamath Proof Explorer


Theorem sumsnd

Description: A sum of a singleton is the term. The deduction version of sumsn . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses sumsnd.1 φ_kB
sumsnd.2 kφ
sumsnd.3 φk=MA=B
sumsnd.4 φMV
sumsnd.5 φB
Assertion sumsnd φkMA=B

Proof

Step Hyp Ref Expression
1 sumsnd.1 φ_kB
2 sumsnd.2 kφ
3 sumsnd.3 φk=MA=B
4 sumsnd.4 φMV
5 sumsnd.5 φB
6 nfcv _mA
7 nfcsb1v _km/kA
8 csbeq1a k=mA=m/kA
9 6 7 8 cbvsumi kMA=mMm/kA
10 csbeq1 m=1Mnm/kA=1Mn/kA
11 1nn 1
12 11 a1i φ1
13 f1osng 1MV1M:11-1 ontoM
14 11 4 13 sylancr φ1M:11-1 ontoM
15 1z 1
16 fzsn 111=1
17 f1oeq2 11=11M:111-1 ontoM1M:11-1 ontoM
18 15 16 17 mp2b 1M:111-1 ontoM1M:11-1 ontoM
19 14 18 sylibr φ1M:111-1 ontoM
20 elsni mMm=M
21 20 adantl φmMm=M
22 21 csbeq1d φmMm/kA=M/kA
23 2 1 4 3 csbiedf φM/kA=B
24 23 adantr φmMM/kA=B
25 5 adantr φmMB
26 24 25 eqeltrd φmMM/kA
27 22 26 eqeltrd φmMm/kA
28 23 adantr φn11M/kA=B
29 elfz1eq n11n=1
30 29 fveq2d n111Mn=1M1
31 fvsng 1MV1M1=M
32 11 4 31 sylancr φ1M1=M
33 30 32 sylan9eqr φn111Mn=M
34 33 csbeq1d φn111Mn/kA=M/kA
35 29 fveq2d n111Bn=1B1
36 fvsng 1B1B1=B
37 11 5 36 sylancr φ1B1=B
38 35 37 sylan9eqr φn111Bn=B
39 28 34 38 3eqtr4rd φn111Bn=1Mn/kA
40 10 12 19 27 39 fsum φmMm/kA=seq1+1B1
41 9 40 eqtrid φkMA=seq1+1B1
42 15 37 seq1i φseq1+1B1=B
43 41 42 eqtrd φkMA=B