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 ⊢Ⅎkφ
esumsplit.2 ⊢Ⅎ_kA
esumsplit.3 ⊢Ⅎ_kB
esumsplit.4 ⊢φ→A∈V
esumsplit.5 ⊢φ→B∈V
esumsplit.6 ⊢φ→A∩B=∅
esumsplit.7 ⊢φ∧k∈A→C∈0+∞
esumsplit.8 ⊢φ∧k∈B→C∈0+∞
Assertion esumsplit ⊢φ→∑*k∈A∪BC=∑*k∈AC+𝑒∑*k∈BC

Proof

Step Hyp Ref Expression
1 esumsplit.1 ⊢Ⅎkφ
2 esumsplit.2 ⊢Ⅎ_kA
3 esumsplit.3 ⊢Ⅎ_kB
4 esumsplit.4 ⊢φ→A∈V
5 esumsplit.5 ⊢φ→B∈V
6 esumsplit.6 ⊢φ→A∩B=∅
7 esumsplit.7 ⊢φ∧k∈A→C∈0+∞
8 esumsplit.8 ⊢φ∧k∈B→C∈0+∞
9 2 3 nfun ⊢Ⅎ_kA∪B
10 unexg ⊢A∈V∧B∈V→A∪B∈V
11 4 5 10 syl2anc ⊢φ→A∪B∈V
12 elun ⊢k∈A∪B↔k∈A∨k∈B
13 7 8 jaodan ⊢φ∧k∈A∨k∈B→C∈0+∞
14 12 13 sylan2b ⊢φ∧k∈A∪B→C∈0+∞
15 xrge0base ⊢0+∞=Baseℝ𝑠*↾𝑠0+∞
16 xrge0plusg ⊢+𝑒=+ℝ𝑠*↾𝑠0+∞
17 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
18 17 a1i ⊢φ→ℝ𝑠*↾𝑠0+∞∈CMnd
19 xrge0tmd ⊢ℝ𝑠*↾𝑠0+∞∈TopMnd
20 19 a1i ⊢φ→ℝ𝑠*↾𝑠0+∞∈TopMnd
21 nfcv ⊢Ⅎ_k0+∞
22 eqid ⊢k∈A∪B⟼C=k∈A∪B⟼C
23 1 9 21 14 22 fmptdF ⊢φ→k∈A∪B⟼C:A∪B⟶0+∞
24 1 2 4 7 esumel ⊢φ→∑*k∈AC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼C
25 ssun1 ⊢A⊆A∪B
26 9 2 resmptf ⊢A⊆A∪B→k∈A∪B⟼C↾A=k∈A⟼C
27 25 26 mp1i ⊢φ→k∈A∪B⟼C↾A=k∈A⟼C
28 27 oveq2d ⊢φ→ℝ𝑠*↾𝑠0+∞tsumsk∈A∪B⟼C↾A=ℝ𝑠*↾𝑠0+∞tsumsk∈A⟼C
29 24 28 eleqtrrd ⊢φ→∑*k∈AC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A∪B⟼C↾A
30 1 3 5 8 esumel ⊢φ→∑*k∈BC∈ℝ𝑠*↾𝑠0+∞tsumsk∈B⟼C
31 ssun2 ⊢B⊆A∪B
32 9 3 resmptf ⊢B⊆A∪B→k∈A∪B⟼C↾B=k∈B⟼C
33 31 32 mp1i ⊢φ→k∈A∪B⟼C↾B=k∈B⟼C
34 33 oveq2d ⊢φ→ℝ𝑠*↾𝑠0+∞tsumsk∈A∪B⟼C↾B=ℝ𝑠*↾𝑠0+∞tsumsk∈B⟼C
35 30 34 eleqtrrd ⊢φ→∑*k∈BC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A∪B⟼C↾B
36 eqidd ⊢φ→A∪B=A∪B
37 15 16 18 20 11 23 29 35 6 36 tsmssplit ⊢φ→∑*k∈AC+𝑒∑*k∈BC∈ℝ𝑠*↾𝑠0+∞tsumsk∈A∪B⟼C
38 1 9 11 14 37 esumid ⊢φ→∑*k∈A∪BC=∑*k∈AC+𝑒∑*k∈BC