This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑘 𝐵
sumsnf.2 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
Assertion sumsnf ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 sumsnf.1 ⊢ Ⅎ 𝑘 𝐵
2 sumsnf.2 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
3 csbeq1a ⊢ ( 𝑘 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑘 ⦌ 𝐴 )
4 nfcv ⊢ Ⅎ 𝑚 𝐴
5 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐴
6 3 4 5 cbvsum ⊢ Σ 𝑘 ∈ { 𝑀 } 𝐴 = Σ 𝑚 ∈ { 𝑀 } ⦋ 𝑚 / 𝑘 ⦌ 𝐴
7 csbeq1 ⊢ ( 𝑚 = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 )
8 1nn ⊢ 1 ∈ ℕ
9 8 a1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → 1 ∈ ℕ )
10 simpl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → 𝑀 ∈ 𝑉 )
11 f1osng ⊢ ( ( 1 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } )
12 8 10 11 sylancr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } )
13 1z ⊢ 1 ∈ ℤ
14 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
15 f1oeq2 ⊢ ( ( 1 ... 1 ) = { 1 } → ( { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } ↔ { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } ) )
16 13 14 15 mp2b ⊢ ( { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } ↔ { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } )
17 12 16 sylibr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } )
18 elsni ⊢ ( 𝑚 ∈ { 𝑀 } → 𝑚 = 𝑀 )
19 18 adantl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → 𝑚 = 𝑀 )
20 19 csbeq1d ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
21 1 a1i ⊢ ( 𝑀 ∈ 𝑉 → Ⅎ 𝑘 𝐵 )
22 21 2 csbiegf ⊢ ( 𝑀 ∈ 𝑉 → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐵 )
23 22 ad2antrr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐵 )
24 simplr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → 𝐵 ∈ ℂ )
25 23 24 eqeltrd ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ )
26 20 25 eqeltrd ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ )
27 22 ad2antrr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐵 )
28 elfz1eq ⊢ ( 𝑛 ∈ ( 1 ... 1 ) → 𝑛 = 1 )
29 28 fveq2d ⊢ ( 𝑛 ∈ ( 1 ... 1 ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) )
30 fvsng ⊢ ( ( 1 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀 )
31 8 10 30 sylancr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀 )
32 29 31 sylan9eqr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) = 𝑀 )
33 32 csbeq1d ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
34 28 fveq2d ⊢ ( 𝑛 ∈ ( 1 ... 1 ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) )
35 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
36 fvsng ⊢ ( ( 1 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
37 8 35 36 sylancr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
38 34 37 sylan9eqr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = 𝐵 )
39 27 33 38 3eqtr4rd ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 )
40 7 9 17 26 39 fsum ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑚 ∈ { 𝑀 } ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ( seq 1 ( + , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
41 6 40 eqtrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = ( seq 1 ( + , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
42 13 37 seq1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( seq 1 ( + , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) = 𝐵 )
43 41 42 eqtrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )