sge0splitsn

Description: Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0splitsn.ph	$⊢ Ⅎ k φ$
	sge0splitsn.a	$⊢ φ \to A \in V$
	sge0splitsn.b	$⊢ φ \to B \in W$
	sge0splitsn.n	$⊢ φ \to \neg B \in A$
	sge0splitsn.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
	sge0splitsn.d	$⊢ k = B \to C = D$
	sge0splitsn.e	$⊢ φ \to D \in [0, +∞]$
Assertion	sge0splitsn	$⊢ φ \to sum^((k \in (A \cup \{B\}) ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} D$

Step	Hyp	Ref	Expression
1		sge0splitsn.ph	$⊢ Ⅎ k φ$
2		sge0splitsn.a	$⊢ φ \to A \in V$
3		sge0splitsn.b	$⊢ φ \to B \in W$
4		sge0splitsn.n	$⊢ φ \to \neg B \in A$
5		sge0splitsn.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
6		sge0splitsn.d	$⊢ k = B \to C = D$
7		sge0splitsn.e	$⊢ φ \to D \in [0, +∞]$
8		snfi	$⊢ \{B\} \in Fin$
9	8	a1i	$⊢ φ \to \{B\} \in Fin$
10	9	elexd	$⊢ φ \to \{B\} \in V$
11		disjsn	$⊢ A \cap \{B\} = \emptyset \leftrightarrow \neg B \in A$
12	4 11	sylibr	$⊢ φ \to A \cap \{B\} = \emptyset$
13		elsni	$⊢ k \in \{B\} \to k = B$
14	6	adantl	$⊢ (φ \land k = B) \to C = D$
15	13 14	sylan2	$⊢ (φ \land k \in \{B\}) \to C = D$
16	7	adantr	$⊢ (φ \land k \in \{B\}) \to D \in [0, +∞]$
17	15 16	eqeltrd	$⊢ (φ \land k \in \{B\}) \to C \in [0, +∞]$
18	1 2 10 12 5 17	sge0splitmpt	$⊢ φ \to sum^((k \in (A \cup \{B\}) ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in \{B\} ⟼ C))$
19	1 3 7 6	sge0snmptf	$⊢ φ \to sum^((k \in \{B\} ⟼ C)) = D$
20	19	oveq2d	$⊢ φ \to sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in \{B\} ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} D$
21	18 20	eqtrd	$⊢ φ \to sum^((k \in (A \cup \{B\}) ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} D$

Metamath Proof Explorer