Metamath Proof Explorer


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 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 𝐷 ) )

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 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) ) )
19 1 3 7 6 sge0snmptf ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) = 𝐷 )
20 19 oveq2d ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 𝐷 ) )
21 18 20 eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 𝐷 ) )