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

Proof

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

Metamath Proof Explorer

Theorem sumsnd

Proof