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