sge0ss

Description: Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0ss.kph	$⊢ Ⅎ k φ$
	sge0ss.b	$⊢ φ \to B \in V$
	sge0ss.a	$⊢ φ \to A \subseteq B$
	sge0ss.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
	sge0ss.c0	$⊢ (φ \land k \in (B ∖ A)) \to C = 0$
Assertion	sge0ss	$⊢ φ \to sum^((k \in A ⟼ C)) = sum^((k \in B ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		sge0ss.kph	$⊢ Ⅎ k φ$
2		sge0ss.b	$⊢ φ \to B \in V$
3		sge0ss.a	$⊢ φ \to A \subseteq B$
4		sge0ss.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
5		sge0ss.c0	$⊢ (φ \land k \in (B ∖ A)) \to C = 0$
6		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
7	3 2 6	syl2anc	$⊢ φ \to A \in V$
8	2	difexd	$⊢ φ \to B ∖ A \in V$
9		disjdif	$⊢ A \cap (B ∖ A) = \emptyset$
10	9	a1i	$⊢ φ \to A \cap (B ∖ A) = \emptyset$
11		0e0iccpnf	$⊢ 0 \in [0, +∞]$
12	11	a1i	$⊢ (φ \land k \in (B ∖ A)) \to 0 \in [0, +∞]$
13	5 12	eqeltrd	$⊢ (φ \land k \in (B ∖ A)) \to C \in [0, +∞]$
14	1 7 8 10 4 13	sge0splitmpt	$⊢ φ \to sum^((k \in (A \cup (B ∖ A)) ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in (B ∖ A) ⟼ C))$
15	14	eqcomd	$⊢ φ \to sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in (B ∖ A) ⟼ C)) = sum^((k \in (A \cup (B ∖ A)) ⟼ C))$
16	1 5	mpteq2da	$⊢ φ \to (k \in (B ∖ A) ⟼ C) = (k \in (B ∖ A) ⟼ 0)$
17	16	fveq2d	$⊢ φ \to sum^((k \in (B ∖ A) ⟼ C)) = sum^((k \in (B ∖ A) ⟼ 0))$
18	1 8	sge0z	$⊢ φ \to sum^((k \in (B ∖ A) ⟼ 0)) = 0$
19	17 18	eqtrd	$⊢ φ \to sum^((k \in (B ∖ A) ⟼ C)) = 0$
20	19	oveq2d	$⊢ φ \to sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in (B ∖ A) ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} 0$
21		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
22	1 4 21	fmptdf	$⊢ φ \to (k \in A ⟼ C) : A ⟶ [0, +∞]$
23	7 22	sge0xrcl	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ^{*}$
24		xaddrid	$⊢ sum^((k \in A ⟼ C)) \in ℝ^{*} \to sum^((k \in A ⟼ C)) +_{𝑒} 0 = sum^((k \in A ⟼ C))$
25	23 24	syl	$⊢ φ \to sum^((k \in A ⟼ C)) +_{𝑒} 0 = sum^((k \in A ⟼ C))$
26		eqidd	$⊢ φ \to sum^((k \in A ⟼ C)) = sum^((k \in A ⟼ C))$
27	20 25 26	3eqtrrd	$⊢ φ \to sum^((k \in A ⟼ C)) = sum^((k \in A ⟼ C)) +_{𝑒} sum^((k \in (B ∖ A) ⟼ C))$
28		undif	$⊢ A \subseteq B \leftrightarrow A \cup (B ∖ A) = B$
29	3 28	sylib	$⊢ φ \to A \cup (B ∖ A) = B$
30	29	eqcomd	$⊢ φ \to B = A \cup (B ∖ A)$
31	30	mpteq1d	$⊢ φ \to (k \in B ⟼ C) = (k \in (A \cup (B ∖ A)) ⟼ C)$
32	31	fveq2d	$⊢ φ \to sum^((k \in B ⟼ C)) = sum^((k \in (A \cup (B ∖ A)) ⟼ C))$
33	15 27 32	3eqtr4d	$⊢ φ \to sum^((k \in A ⟼ C)) = sum^((k \in B ⟼ C))$

Metamath Proof Explorer

Theorem sge0ss

Proof