Metamath Proof Explorer

Theorem esummulc1

Description: An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses esummulc2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esummulc2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esummulc2.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
Assertion esummulc1 ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 ·e 𝐶 ) = Σ* 𝑘 ∈ 𝐴 ( 𝐵 ·e 𝐶 ) )

Proof

Step Hyp Ref Expression
1 esummulc2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 esummulc2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
3 esummulc2.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
4 eqid ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
5 eqid ⊢ ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) )
6 4 5 3 xrge0mulc1cn ⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ∈ ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) )
7 eqidd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) )
8 oveq1 ⊢ ( 𝑧 = 0 → ( 𝑧 ·e 𝐶 ) = ( 0 ·e 𝐶 ) )
9 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
10 9 3 sselid ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
11 xmul02 ⊢ ( 𝐶 ∈ ℝ* → ( 0 ·e 𝐶 ) = 0 )
12 10 11 syl ⊢ ( 𝜑 → ( 0 ·e 𝐶 ) = 0 )
13 8 12 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑧 = 0 ) → ( 𝑧 ·e 𝐶 ) = 0 )
14 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
15 14 a1i ⊢ ( 𝜑 → 0 ∈ ( 0 [,] +∞ ) )
16 7 13 15 15 fvmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 0 ) = 0 )
17 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
18 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 𝑦 ∈ ( 0 [,] +∞ ) )
19 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
20 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
21 19 20 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
22 xrge0adddir ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 +𝑒 𝑦 ) ·e 𝐶 ) = ( ( 𝑥 ·e 𝐶 ) +𝑒 ( 𝑦 ·e 𝐶 ) ) )
23 17 18 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 +𝑒 𝑦 ) ·e 𝐶 ) = ( ( 𝑥 ·e 𝐶 ) +𝑒 ( 𝑦 ·e 𝐶 ) ) )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = ( 𝑥 +𝑒 𝑦 ) ) → 𝑧 = ( 𝑥 +𝑒 𝑦 ) )
26 25 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = ( 𝑥 +𝑒 𝑦 ) ) → ( 𝑧 ·e 𝐶 ) = ( ( 𝑥 +𝑒 𝑦 ) ·e 𝐶 ) )
27 ge0xaddcl ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( 0 [,] +∞ ) )
28 27 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( 0 [,] +∞ ) )
29 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 +𝑒 𝑦 ) ·e 𝐶 ) ∈ V )
30 24 26 28 29 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ ( 𝑥 +𝑒 𝑦 ) ) = ( ( 𝑥 +𝑒 𝑦 ) ·e 𝐶 ) )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = 𝑥 ) → 𝑧 = 𝑥 )
32 31 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 ·e 𝐶 ) = ( 𝑥 ·e 𝐶 ) )
33 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 𝐶 ) ∈ V )
34 24 32 17 33 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑥 ) = ( 𝑥 ·e 𝐶 ) )
35 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = 𝑦 ) → 𝑧 = 𝑦 )
36 35 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑧 ·e 𝐶 ) = ( 𝑦 ·e 𝐶 ) )
37 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑦 ·e 𝐶 ) ∈ V )
38 24 36 18 37 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑦 ) = ( 𝑦 ·e 𝐶 ) )
39 34 38 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑥 ) +𝑒 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 ·e 𝐶 ) +𝑒 ( 𝑦 ·e 𝐶 ) ) )
40 23 30 39 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ ( 𝑥 +𝑒 𝑦 ) ) = ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑥 ) +𝑒 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝑦 ) ) )
41 4 1 2 6 16 40 esumcocn ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ Σ* 𝑘 ∈ 𝐴 𝐵 ) = Σ* 𝑘 ∈ 𝐴 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝐵 ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑧 = Σ* 𝑘 ∈ 𝐴 𝐵 ) → 𝑧 = Σ* 𝑘 ∈ 𝐴 𝐵 )
43 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 = Σ* 𝑘 ∈ 𝐴 𝐵 ) → ( 𝑧 ·e 𝐶 ) = ( Σ* 𝑘 ∈ 𝐴 𝐵 ·e 𝐶 ) )
44 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
45 nfcv ⊢ Ⅎ 𝑘 𝐴
46 45 esumcl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
47 1 44 46 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
48 ovexd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 ·e 𝐶 ) ∈ V )
49 7 43 47 48 fvmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ Σ* 𝑘 ∈ 𝐴 𝐵 ) = ( Σ* 𝑘 ∈ 𝐴 𝐵 ·e 𝐶 ) )
50 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
52 51 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 = 𝐵 ) → ( 𝑧 ·e 𝐶 ) = ( 𝐵 ·e 𝐶 ) )
53 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ·e 𝐶 ) ∈ V )
54 50 52 2 53 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 ·e 𝐶 ) )
55 54 esumeq2dv ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ ( 𝑧 ·e 𝐶 ) ) ‘ 𝐵 ) = Σ* 𝑘 ∈ 𝐴 ( 𝐵 ·e 𝐶 ) )
56 41 49 55 3eqtr3d ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 ·e 𝐶 ) = Σ* 𝑘 ∈ 𝐴 ( 𝐵 ·e 𝐶 ) )