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

Proof

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