Metamath Proof Explorer

Theorem esumpad

Description: Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020)

Ref Expression
Hypotheses esumpad.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumpad.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
esumpad.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esumpad.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
Assertion esumpad ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 esumpad.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 esumpad.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 esumpad.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4 esumpad.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
5 nfv ⊢ Ⅎ 𝑘 𝜑
6 nfcv ⊢ Ⅎ 𝑘 𝐴
7 nfcv ⊢ Ⅎ 𝑘 ( 𝐵 ∖ 𝐴 )
8 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
9 1 8 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
10 2 difexd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ V )
11 disjdif ⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
12 11 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
13 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 )
14 13 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑘 ∈ 𝐵 )
15 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
16 4 15 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
17 14 16 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
18 5 6 7 9 10 12 3 17 esumsplit ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝐶 = ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 ) )
19 undif2 ⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
20 esumeq1 ⊢ ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 ) → Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
21 19 20 ax-mp ⊢ Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶
22 21 a1i ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
23 14 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = 0 )
25 5 24 esumeq2d ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 0 )
26 7 esum0 ⊢ ( ( 𝐵 ∖ 𝐴 ) ∈ V → Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 0 = 0 )
27 10 26 syl ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 0 = 0 )
28 25 27 eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 = 0 )
29 28 oveq2d ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 ) = ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 0 ) )
30 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
31 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
32 6 esumcl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
33 1 31 32 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
34 30 33 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* )
35 xaddid1 ⊢ ( Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* → ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 0 ) = Σ* 𝑘 ∈ 𝐴 𝐶 )
36 34 35 syl ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 0 ) = Σ* 𝑘 ∈ 𝐴 𝐶 )
37 29 36 eqtrd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐶 +𝑒 Σ* 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) 𝐶 ) = Σ* 𝑘 ∈ 𝐴 𝐶 )
38 18 22 37 3eqtr3d ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )