Metamath Proof Explorer

Theorem esumsplit

Description: Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017)

Ref Expression
Hypotheses esumsplit.1 ⊢ Ⅎ 𝑘 𝜑
esumsplit.2 ⊢ Ⅎ 𝑘 𝐴
esumsplit.3 ⊢ Ⅎ 𝑘 𝐵
esumsplit.4 ⊢ ( 𝜑 → 𝐴 ∈ V )
esumsplit.5 ⊢ ( 𝜑 → 𝐵 ∈ V )
esumsplit.6 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
esumsplit.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esumsplit.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion esumsplit ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step Hyp Ref Expression
1 esumsplit.1 ⊢ Ⅎ 𝑘 𝜑
2 esumsplit.2 ⊢ Ⅎ 𝑘 𝐴
3 esumsplit.3 ⊢ Ⅎ 𝑘 𝐵
4 esumsplit.4 ⊢ ( 𝜑 → 𝐴 ∈ V )
5 esumsplit.5 ⊢ ( 𝜑 → 𝐵 ∈ V )
6 esumsplit.6 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
7 esumsplit.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
8 esumsplit.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
9 2 3 nfun ⊢ Ⅎ 𝑘 ( 𝐴 ∪ 𝐵 )
10 unexg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
11 4 5 10 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
12 elun ⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
13 7 8 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14 12 13 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
15 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
16 xrge0plusg ⊢ +𝑒 = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
17 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
18 17 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
19 xrge0tmd ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd
20 19 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd )
21 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
22 eqid ⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 )
23 1 9 21 14 22 fmptdF ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 0 [,] +∞ ) )
24 1 2 4 7 esumel ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
25 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
26 9 2 resmptf ⊢ ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
27 25 26 mp1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
28 27 oveq2d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
29 24 28 eleqtrrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐴 ) ) )
30 1 3 5 8 esumel ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
31 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
32 9 3 resmptf ⊢ ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) )
33 31 32 mp1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) )
34 33 oveq2d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
35 30 34 eleqtrrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ↾ 𝐵 ) ) )
36 eqidd ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )
37 15 16 18 20 11 23 29 35 6 36 tsmssplit ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ 𝐵 𝐶 ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) ) )
38 1 9 11 14 37 esumid ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ 𝐵 𝐶 ) )