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	2	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ V )
9		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
10	9	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
11		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 0 ∈ ( 0 [,] +∞ ) )
13	5 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14	1 7 8 10 4 13	sge0splitmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) )
15	14	eqcomd	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) )
16	1 5	mpteq2da	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) ) )
18	1 8	sge0z	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) ) = 0 )
19	17 18	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) = 0 )
20	19	oveq2d	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 0 ) )
21		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
22	1 4 21	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
23	7 22	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* )
24		xaddrid	⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 0 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
25	23 24	syl	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 0 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
26		eqidd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
27	20 25 26	3eqtrrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ) ) )
28		undif	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
29	3 28	sylib	⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
30	29	eqcomd	⊢ ( 𝜑 → 𝐵 = ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) )
31	30	mpteq1d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) )
32	31	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↦ 𝐶 ) ) )
33	15 27 32	3eqtr4d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )