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	$⊢ \underline{Ⅎ} k B$
	sumsnf.2	$⊢ k = M \to A = B$
Assertion	sumsnf	$⊢ (M \in V \land B \in ℂ) \to \sum_{k \in \{M\}} A = B$

Proof

Step	Hyp	Ref	Expression
1		sumsnf.1	$⊢ \underline{Ⅎ} k B$
2		sumsnf.2	$⊢ k = M \to A = B$
3		nfcv	$⊢ \underline{Ⅎ} m A$
4		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ A$
5		csbeq1a	$⊢ k = m \to A = ⦋ m / k ⦌ A$
6	3 4 5	cbvsumi	$⊢ \sum_{k \in \{M\}} A = \sum_{m \in \{M\}} ⦋ m / k ⦌ A$
7		csbeq1	$⊢ m = \{⟨1, M⟩\} (n) \to ⦋ m / k ⦌ A = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A$
8		1nn	$⊢ 1 \in ℕ$
9	8	a1i	$⊢ (M \in V \land B \in ℂ) \to 1 \in ℕ$
10		simpl	$⊢ (M \in V \land B \in ℂ) \to M \in V$
11		f1osng	$⊢ (1 \in ℕ \land M \in V) \to \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\}$
12	8 10 11	sylancr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\}$
13		1z	$⊢ 1 \in ℤ$
14		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
15		f1oeq2	$⊢ (1 \dots 1) = \{1\} \to (\{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\} \leftrightarrow \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\})$
16	13 14 15	mp2b	$⊢ \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\} \leftrightarrow \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\}$
17	12 16	sylibr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\}$
18		elsni	$⊢ m \in \{M\} \to m = M$
19	18	adantl	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to m = M$
20	19	csbeq1d	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ m / k ⦌ A = ⦋ M / k ⦌ A$
21	1	a1i	$⊢ M \in V \to \underline{Ⅎ} k B$
22	21 2	csbiegf	$⊢ M \in V \to ⦋ M / k ⦌ A = B$
23	22	ad2antrr	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ M / k ⦌ A = B$
24		simplr	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to B \in ℂ$
25	23 24	eqeltrd	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ M / k ⦌ A \in ℂ$
26	20 25	eqeltrd	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ m / k ⦌ A \in ℂ$
27	22	ad2antrr	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to ⦋ M / k ⦌ A = B$
28		elfz1eq	$⊢ n \in (1 \dots 1) \to n = 1$
29	28	fveq2d	$⊢ n \in (1 \dots 1) \to \{⟨1, M⟩\} (n) = \{⟨1, M⟩\} (1)$
30		fvsng	$⊢ (1 \in ℕ \land M \in V) \to \{⟨1, M⟩\} (1) = M$
31	8 10 30	sylancr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, M⟩\} (1) = M$
32	29 31	sylan9eqr	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to \{⟨1, M⟩\} (n) = M$
33	32	csbeq1d	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to ⦋ \{⟨1, M⟩\} (n) / k ⦌ A = ⦋ M / k ⦌ A$
34	28	fveq2d	$⊢ n \in (1 \dots 1) \to \{⟨1, B⟩\} (n) = \{⟨1, B⟩\} (1)$
35		simpr	$⊢ (M \in V \land B \in ℂ) \to B \in ℂ$
36		fvsng	$⊢ (1 \in ℕ \land B \in ℂ) \to \{⟨1, B⟩\} (1) = B$
37	8 35 36	sylancr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, B⟩\} (1) = B$
38	34 37	sylan9eqr	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to \{⟨1, B⟩\} (n) = B$
39	27 33 38	3eqtr4rd	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to \{⟨1, B⟩\} (n) = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A$
40	7 9 17 26 39	fsum	$⊢ (M \in V \land B \in ℂ) \to \sum_{m \in \{M\}} ⦋ m / k ⦌ A = seq 1 (+ \{⟨1, B⟩\}) (1)$
41	6 40	syl5eq	$⊢ (M \in V \land B \in ℂ) \to \sum_{k \in \{M\}} A = seq 1 (+ \{⟨1, B⟩\}) (1)$
42	13 37	seq1i	$⊢ (M \in V \land B \in ℂ) \to seq 1 (+ \{⟨1, B⟩\}) (1) = B$
43	41 42	eqtrd	$⊢ (M \in V \land B \in ℂ) \to \sum_{k \in \{M\}} A = B$

Metamath Proof Explorer

Theorem sumsnf

Proof