fsumsplitsndif

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018)

		Ref	Expression
	Assertion	fsumsplitsndif	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B = \sum_{k \in A ∖ \{X\}} B + ⦋ X / k ⦌ B$

Proof

Step	Hyp	Ref	Expression
1		neldifsnd	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \neg X \in (A ∖ \{X\})$
2		disjsn	$⊢ (A ∖ \{X\}) \cap \{X\} = \emptyset \leftrightarrow \neg X \in (A ∖ \{X\})$
3	1 2	sylibr	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to (A ∖ \{X\}) \cap \{X\} = \emptyset$
4		uncom	$⊢ (A ∖ \{X\}) \cup \{X\} = \{X\} \cup (A ∖ \{X\})$
5		simp2	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to X \in A$
6	5	snssd	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \{X\} \subseteq A$
7		undif	$⊢ \{X\} \subseteq A \leftrightarrow \{X\} \cup (A ∖ \{X\}) = A$
8	6 7	sylib	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \{X\} \cup (A ∖ \{X\}) = A$
9	4 8	eqtr2id	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to A = (A ∖ \{X\}) \cup \{X\}$
10		simp1	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to A \in Fin$
11		rspcsbela	$⊢ (x \in A \land \forall k \in A B \in ℤ) \to ⦋ x / k ⦌ B \in ℤ$
12	11	zcnd	$⊢ (x \in A \land \forall k \in A B \in ℤ) \to ⦋ x / k ⦌ B \in ℂ$
13	12	expcom	$⊢ \forall k \in A B \in ℤ \to (x \in A \to ⦋ x / k ⦌ B \in ℂ)$
14	13	3ad2ant3	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to (x \in A \to ⦋ x / k ⦌ B \in ℂ)$
15	14	imp	$⊢ ((A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \land x \in A) \to ⦋ x / k ⦌ B \in ℂ$
16	3 9 10 15	fsumsplit	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{x \in A} ⦋ x / k ⦌ B = \sum_{x \in A ∖ \{X\}} ⦋ x / k ⦌ B + \sum_{x \in \{X\}} ⦋ x / k ⦌ B$
17		csbeq1a	$⊢ k = x \to B = ⦋ x / k ⦌ B$
18		nfcv	$⊢ \underline{Ⅎ} x B$
19		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ x / k ⦌ B$
20	17 18 19	cbvsum	$⊢ \sum_{k \in A} B = \sum_{x \in A} ⦋ x / k ⦌ B$
21	17 18 19	cbvsum	$⊢ \sum_{k \in A ∖ \{X\}} B = \sum_{x \in A ∖ \{X\}} ⦋ x / k ⦌ B$
22	17 18 19	cbvsum	$⊢ \sum_{k \in \{X\}} B = \sum_{x \in \{X\}} ⦋ x / k ⦌ B$
23	21 22	oveq12i	$⊢ \sum_{k \in A ∖ \{X\}} B + \sum_{k \in \{X\}} B = \sum_{x \in A ∖ \{X\}} ⦋ x / k ⦌ B + \sum_{x \in \{X\}} ⦋ x / k ⦌ B$
24	16 20 23	3eqtr4g	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B = \sum_{k \in A ∖ \{X\}} B + \sum_{k \in \{X\}} B$
25		rspcsbela	$⊢ (X \in A \land \forall k \in A B \in ℤ) \to ⦋ X / k ⦌ B \in ℤ$
26	25	zcnd	$⊢ (X \in A \land \forall k \in A B \in ℤ) \to ⦋ X / k ⦌ B \in ℂ$
27	26	3adant1	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to ⦋ X / k ⦌ B \in ℂ$
28		sumsns	$⊢ (X \in A \land ⦋ X / k ⦌ B \in ℂ) \to \sum_{k \in \{X\}} B = ⦋ X / k ⦌ B$
29	5 27 28	syl2anc	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{k \in \{X\}} B = ⦋ X / k ⦌ B$
30	29	oveq2d	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{k \in A ∖ \{X\}} B + \sum_{k \in \{X\}} B = \sum_{k \in A ∖ \{X\}} B + ⦋ X / k ⦌ B$
31	24 30	eqtrd	$⊢ (A \in Fin \land X \in A \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B = \sum_{k \in A ∖ \{X\}} B + ⦋ X / k ⦌ B$

Metamath Proof Explorer

Theorem fsumsplitsndif

Proof