# 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 ${⊢}{\phi }\to \underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
sumsnd.2 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
sumsnd.3 ${⊢}\left({\phi }\wedge {k}={M}\right)\to {A}={B}$
sumsnd.4 ${⊢}{\phi }\to {M}\in {V}$
sumsnd.5 ${⊢}{\phi }\to {B}\in ℂ$
Assertion sumsnd ${⊢}{\phi }\to \sum _{{k}\in \left\{{M}\right\}}{A}={B}$

### Proof

Step Hyp Ref Expression
1 sumsnd.1 ${⊢}{\phi }\to \underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
2 sumsnd.2 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
3 sumsnd.3 ${⊢}\left({\phi }\wedge {k}={M}\right)\to {A}={B}$
4 sumsnd.4 ${⊢}{\phi }\to {M}\in {V}$
5 sumsnd.5 ${⊢}{\phi }\to {B}\in ℂ$
6 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{A}$
7 nfcsb1v
8 csbeq1a
9 6 7 8 cbvsumi
10 csbeq1
11 1nn ${⊢}1\in ℕ$
12 11 a1i ${⊢}{\phi }\to 1\in ℕ$
13 f1osng ${⊢}\left(1\in ℕ\wedge {M}\in {V}\right)\to \left\{⟨1,{M}⟩\right\}:\left\{1\right\}\underset{1-1 onto}{⟶}\left\{{M}\right\}$
14 11 4 13 sylancr ${⊢}{\phi }\to \left\{⟨1,{M}⟩\right\}:\left\{1\right\}\underset{1-1 onto}{⟶}\left\{{M}\right\}$
15 1z ${⊢}1\in ℤ$
16 fzsn ${⊢}1\in ℤ\to \left(1\dots 1\right)=\left\{1\right\}$
17 f1oeq2 ${⊢}\left(1\dots 1\right)=\left\{1\right\}\to \left(\left\{⟨1,{M}⟩\right\}:\left(1\dots 1\right)\underset{1-1 onto}{⟶}\left\{{M}\right\}↔\left\{⟨1,{M}⟩\right\}:\left\{1\right\}\underset{1-1 onto}{⟶}\left\{{M}\right\}\right)$
18 15 16 17 mp2b ${⊢}\left\{⟨1,{M}⟩\right\}:\left(1\dots 1\right)\underset{1-1 onto}{⟶}\left\{{M}\right\}↔\left\{⟨1,{M}⟩\right\}:\left\{1\right\}\underset{1-1 onto}{⟶}\left\{{M}\right\}$
19 14 18 sylibr ${⊢}{\phi }\to \left\{⟨1,{M}⟩\right\}:\left(1\dots 1\right)\underset{1-1 onto}{⟶}\left\{{M}\right\}$
20 elsni ${⊢}{m}\in \left\{{M}\right\}\to {m}={M}$
21 20 adantl ${⊢}\left({\phi }\wedge {m}\in \left\{{M}\right\}\right)\to {m}={M}$
22 21 csbeq1d
23 2 1 4 3 csbiedf
25 5 adantr ${⊢}\left({\phi }\wedge {m}\in \left\{{M}\right\}\right)\to {B}\in ℂ$
26 24 25 eqeltrd
27 22 26 eqeltrd
29 elfz1eq ${⊢}{n}\in \left(1\dots 1\right)\to {n}=1$
30 29 fveq2d ${⊢}{n}\in \left(1\dots 1\right)\to \left\{⟨1,{M}⟩\right\}\left({n}\right)=\left\{⟨1,{M}⟩\right\}\left(1\right)$
31 fvsng ${⊢}\left(1\in ℕ\wedge {M}\in {V}\right)\to \left\{⟨1,{M}⟩\right\}\left(1\right)={M}$
32 11 4 31 sylancr ${⊢}{\phi }\to \left\{⟨1,{M}⟩\right\}\left(1\right)={M}$
33 30 32 sylan9eqr ${⊢}\left({\phi }\wedge {n}\in \left(1\dots 1\right)\right)\to \left\{⟨1,{M}⟩\right\}\left({n}\right)={M}$
34 33 csbeq1d
35 29 fveq2d ${⊢}{n}\in \left(1\dots 1\right)\to \left\{⟨1,{B}⟩\right\}\left({n}\right)=\left\{⟨1,{B}⟩\right\}\left(1\right)$
36 fvsng ${⊢}\left(1\in ℕ\wedge {B}\in ℂ\right)\to \left\{⟨1,{B}⟩\right\}\left(1\right)={B}$
37 11 5 36 sylancr ${⊢}{\phi }\to \left\{⟨1,{B}⟩\right\}\left(1\right)={B}$
38 35 37 sylan9eqr ${⊢}\left({\phi }\wedge {n}\in \left(1\dots 1\right)\right)\to \left\{⟨1,{B}⟩\right\}\left({n}\right)={B}$
39 28 34 38 3eqtr4rd
40 10 12 19 27 39 fsum
41 9 40 syl5eq ${⊢}{\phi }\to \sum _{{k}\in \left\{{M}\right\}}{A}=seq1\left(+,\left\{⟨1,{B}⟩\right\}\right)\left(1\right)$
42 15 37 seq1i ${⊢}{\phi }\to seq1\left(+,\left\{⟨1,{B}⟩\right\}\right)\left(1\right)={B}$
43 41 42 eqtrd ${⊢}{\phi }\to \sum _{{k}\in \left\{{M}\right\}}{A}={B}$