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		nfcv	⊢ Ⅎ 𝑚 𝐴
4		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐴
5		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑘 ⦌ 𝐴 )
6	3 4 5	cbvsumi	⊢ Σ 𝑘 ∈ { 𝑀 } 𝐴 = Σ 𝑚 ∈ { 𝑀 } ⦋ 𝑚 / 𝑘 ⦌ 𝐴
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	syl5eq	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = ( seq 1 ( + , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
42	13 37	seq1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( seq 1 ( + , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) = 𝐵 )
43	41 42	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )