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 ⊢Ⅎ_kB
sumsnf.2 ⊢k=M→A=B
Assertion sumsnf ⊢M∈V∧B∈ℂ→∑k∈MA=B

Proof

Step Hyp Ref Expression
1 sumsnf.1 ⊢Ⅎ_kB
2 sumsnf.2 ⊢k=M→A=B
3 nfcv ⊢Ⅎ_mA
4 nfcsb1v ⊢Ⅎ_k⦋m/k⦌A
5 csbeq1a ⊢k=m→A=⦋m/k⦌A
6 3 4 5 cbvsumi ⊢∑k∈MA=∑m∈M⦋m/k⦌A
7 csbeq1 ⊢m=1M⁡n→⦋m/k⦌A=⦋1M⁡n/k⦌A
8 1nn ⊢1∈ℕ
9 8 a1i ⊢M∈V∧B∈ℂ→1∈ℕ
10 simpl ⊢M∈V∧B∈ℂ→M∈V
11 f1osng ⊢1∈ℕ∧M∈V→1M:1⟶1-1 ontoM
12 8 10 11 sylancr ⊢M∈V∧B∈ℂ→1M:1⟶1-1 ontoM
13 1z ⊢1∈ℤ
14 fzsn ⊢1∈ℤ→1…1=1
15 f1oeq2 ⊢1…1=1→1M:1…1⟶1-1 ontoM↔1M:1⟶1-1 ontoM
16 13 14 15 mp2b ⊢1M:1…1⟶1-1 ontoM↔1M:1⟶1-1 ontoM
17 12 16 sylibr ⊢M∈V∧B∈ℂ→1M:1…1⟶1-1 ontoM
18 elsni ⊢m∈M→m=M
19 18 adantl ⊢M∈V∧B∈ℂ∧m∈M→m=M
20 19 csbeq1d ⊢M∈V∧B∈ℂ∧m∈M→⦋m/k⦌A=⦋M/k⦌A
21 1 a1i ⊢M∈V→Ⅎ_kB
22 21 2 csbiegf ⊢M∈V→⦋M/k⦌A=B
23 22 ad2antrr ⊢M∈V∧B∈ℂ∧m∈M→⦋M/k⦌A=B
24 simplr ⊢M∈V∧B∈ℂ∧m∈M→B∈ℂ
25 23 24 eqeltrd ⊢M∈V∧B∈ℂ∧m∈M→⦋M/k⦌A∈ℂ
26 20 25 eqeltrd ⊢M∈V∧B∈ℂ∧m∈M→⦋m/k⦌A∈ℂ
27 22 ad2antrr ⊢M∈V∧B∈ℂ∧n∈1…1→⦋M/k⦌A=B
28 elfz1eq ⊢n∈1…1→n=1
29 28 fveq2d ⊢n∈1…1→1M⁡n=1M⁡1
30 fvsng ⊢1∈ℕ∧M∈V→1M⁡1=M
31 8 10 30 sylancr ⊢M∈V∧B∈ℂ→1M⁡1=M
32 29 31 sylan9eqr ⊢M∈V∧B∈ℂ∧n∈1…1→1M⁡n=M
33 32 csbeq1d ⊢M∈V∧B∈ℂ∧n∈1…1→⦋1M⁡n/k⦌A=⦋M/k⦌A
34 28 fveq2d ⊢n∈1…1→1B⁡n=1B⁡1
35 simpr ⊢M∈V∧B∈ℂ→B∈ℂ
36 fvsng ⊢1∈ℕ∧B∈ℂ→1B⁡1=B
37 8 35 36 sylancr ⊢M∈V∧B∈ℂ→1B⁡1=B
38 34 37 sylan9eqr ⊢M∈V∧B∈ℂ∧n∈1…1→1B⁡n=B
39 27 33 38 3eqtr4rd ⊢M∈V∧B∈ℂ∧n∈1…1→1B⁡n=⦋1M⁡n/k⦌A
40 7 9 17 26 39 fsum ⊢M∈V∧B∈ℂ→∑m∈M⦋m/k⦌A=seq1+1B⁡1
41 6 40 eqtrid ⊢M∈V∧B∈ℂ→∑k∈MA=seq1+1B⁡1
42 13 37 seq1i ⊢M∈V∧B∈ℂ→seq1+1B⁡1=B
43 41 42 eqtrd ⊢M∈V∧B∈ℂ→∑k∈MA=B