Metamath Proof Explorer

Theorem sge0splitmpt

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0splitmpt.xph ⊢ Ⅎ 𝑥 𝜑
sge0splitmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0splitmpt.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
sge0splitmpt.in ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
sge0splitmpt.ac ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
sge0splitmpt.bc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion sge0splitmpt ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0splitmpt.xph ⊢ Ⅎ 𝑥 𝜑
2 sge0splitmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 sge0splitmpt.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 sge0splitmpt.in ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
5 sge0splitmpt.ac ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 sge0splitmpt.bc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
7 eqid ⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
8 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
9 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝜑 )
10 elunnel1 ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
11 10 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
12 9 11 6 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
13 8 12 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 )
15 1 13 14 fmptdf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 0 [,] +∞ ) )
16 2 3 7 4 15 sge0split ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) ) )
17 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
18 17 resmpti ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
19 18 fveq2i ⊢ ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
20 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
21 20 resmpti ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
22 21 fveq2i ⊢ ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
23 19 22 oveq12i ⊢ ( ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) )
24 23 a1i ⊢ ( 𝜑 → ( ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) ) )
25 16 24 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) ) )