Theorem 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	⊢ Ⅎ 𝑘 𝜑
	sge0splitsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0splitsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	sge0splitsn.n	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐴 )
	sge0splitsn.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
	sge0splitsn.d	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐷 )
	sge0splitsn.e	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
Assertion	sge0splitsn	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0splitsn.ph	⊢ Ⅎ 𝑘 𝜑
2		sge0splitsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0splitsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		sge0splitsn.n	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐴 )
5		sge0splitsn.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6		sge0splitsn.d	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐷 )
7		sge0splitsn.e	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
8		snfi	⊢ { 𝐵 } ∈ Fin
9	8	a1i	⊢ ( 𝜑 → { 𝐵 } ∈ Fin )
10	9	elexd	⊢ ( 𝜑 → { 𝐵 } ∈ V )
11		disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
12	4 11	sylibr	⊢ ( 𝜑 → ( 𝐴 ∩ { 𝐵 } ) = ∅ )
13		elsni	⊢ ( 𝑘 ∈ { 𝐵 } → 𝑘 = 𝐵 )
14	6	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐷 )
15	13 14	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐶 = 𝐷 )
16	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
17	15 16	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
18	1 2 10 12 5 17	sge0splitmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) ) )
19	1 3 7 6	sge0snmptf	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) = 𝐷 )
20	19	oveq2d	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 𝐷 ) )
21	18 20	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) +e 𝐷 ) )