# Metamath Proof Explorer

## Theorem sumsnf

Description: A sum of a singleton is the term. A version of sumsn using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses sumsnf.1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
sumsnf.2 ${⊢}{k}={M}\to {A}={B}$
Assertion sumsnf ${⊢}\left({M}\in {V}\wedge {B}\in ℂ\right)\to \sum _{{k}\in \left\{{M}\right\}}{A}={B}$

### Proof

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