Theorem 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	⊢ Ⅎ 𝑘 𝜑
	sge0ss.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	sge0ss.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	sge0ss.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
	sge0ss.c0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
Assertion	sge0ss	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0ss.kph	⊢ Ⅎ 𝑘 𝜑
2		sge0ss.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		sge0ss.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4		sge0ss.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5		sge0ss.c0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
6		ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
7	3 2 6	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ V )
8		difexg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∖ 𝐴 ) ∈ V )
9	2 8	syl	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ V )
10		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
11	10	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
12		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 0 ∈ ( 0 [,] +∞ ) )
14	5 13	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
15	1 7 9 11 4 14	sge0splitmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) )
16	15	eqcomd	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) )
17	1 5	mpteq2da	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
18	17	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) ) )
19	1 9	sge0z	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) ) = 0 )
20	18 19	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) = 0 )
21	20	oveq2d	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 0 ) )
22		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
23	1 4 22	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
24	7 23	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* )
25		xaddid1	⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
26	24 25	syl	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
27		eqidd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
28	21 26 27	3eqtrrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) )
29		undif	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
30	3 29	sylib	⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
31	30	eqcomd	⊢ ( 𝜑 → 𝐵 = ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) )
32	31	mpteq1d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) )
33	32	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) )
34	16 28 33	3eqtr4d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )