# 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 ${⊢}{\phi }\to {A}\in {V}$
esummulc2.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
esummulc2.c ${⊢}{\phi }\to {C}\in \left[0,\mathrm{+\infty }\right)$
Assertion esummulc1 ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}{\cdot }_{𝑒}{C}=\underset{{k}\in {A}}{{\sum }^{*}}\left({B}{\cdot }_{𝑒}{C}\right)$

### Proof

Step Hyp Ref Expression
1 esummulc2.a ${⊢}{\phi }\to {A}\in {V}$
2 esummulc2.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
3 esummulc2.c ${⊢}{\phi }\to {C}\in \left[0,\mathrm{+\infty }\right)$
4 eqid ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
5 eqid ${⊢}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)$
6 4 5 3 xrge0mulc1cn ${⊢}{\phi }\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\in \left(\left(\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\right)\mathrm{Cn}\left(\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\right)\right)$
7 eqidd ${⊢}{\phi }\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)$
8 oveq1 ${⊢}{z}=0\to {z}{\cdot }_{𝑒}{C}=0{\cdot }_{𝑒}{C}$
9 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
10 9 3 sseldi ${⊢}{\phi }\to {C}\in {ℝ}^{*}$
11 xmul02 ${⊢}{C}\in {ℝ}^{*}\to 0{\cdot }_{𝑒}{C}=0$
12 10 11 syl ${⊢}{\phi }\to 0{\cdot }_{𝑒}{C}=0$
13 8 12 sylan9eqr ${⊢}\left({\phi }\wedge {z}=0\right)\to {z}{\cdot }_{𝑒}{C}=0$
14 0e0iccpnf ${⊢}0\in \left[0,\mathrm{+\infty }\right]$
15 14 a1i ${⊢}{\phi }\to 0\in \left[0,\mathrm{+\infty }\right]$
16 7 13 15 15 fvmptd ${⊢}{\phi }\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left(0\right)=0$
17 simp2 ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {x}\in \left[0,\mathrm{+\infty }\right]$
18 simp3 ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {y}\in \left[0,\mathrm{+\infty }\right]$
19 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
20 3 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {C}\in \left[0,\mathrm{+\infty }\right)$
21 19 20 sseldi ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {C}\in \left[0,\mathrm{+\infty }\right]$
22 xrge0adddir ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\wedge {C}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}{+}_{𝑒}{y}\right){\cdot }_{𝑒}{C}=\left({x}{\cdot }_{𝑒}{C}\right){+}_{𝑒}\left({y}{\cdot }_{𝑒}{C}\right)$
23 17 18 21 22 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}{+}_{𝑒}{y}\right){\cdot }_{𝑒}{C}=\left({x}{\cdot }_{𝑒}{C}\right){+}_{𝑒}\left({y}{\cdot }_{𝑒}{C}\right)$
24 eqidd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)$
25 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={x}{+}_{𝑒}{y}\right)\to {z}={x}{+}_{𝑒}{y}$
26 25 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={x}{+}_{𝑒}{y}\right)\to {z}{\cdot }_{𝑒}{C}=\left({x}{+}_{𝑒}{y}\right){\cdot }_{𝑒}{C}$
27 ge0xaddcl ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {x}{+}_{𝑒}{y}\in \left[0,\mathrm{+\infty }\right]$
28 27 3adant1 ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {x}{+}_{𝑒}{y}\in \left[0,\mathrm{+\infty }\right]$
29 ovexd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}{+}_{𝑒}{y}\right){\cdot }_{𝑒}{C}\in \mathrm{V}$
30 24 26 28 29 fvmptd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({x}{+}_{𝑒}{y}\right)=\left({x}{+}_{𝑒}{y}\right){\cdot }_{𝑒}{C}$
31 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={x}\right)\to {z}={x}$
32 31 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={x}\right)\to {z}{\cdot }_{𝑒}{C}={x}{\cdot }_{𝑒}{C}$
33 ovexd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {x}{\cdot }_{𝑒}{C}\in \mathrm{V}$
34 24 32 17 33 fvmptd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({x}\right)={x}{\cdot }_{𝑒}{C}$
35 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={y}\right)\to {z}={y}$
36 35 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {z}={y}\right)\to {z}{\cdot }_{𝑒}{C}={y}{\cdot }_{𝑒}{C}$
37 ovexd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to {y}{\cdot }_{𝑒}{C}\in \mathrm{V}$
38 24 36 18 37 fvmptd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({y}\right)={y}{\cdot }_{𝑒}{C}$
39 34 38 oveq12d ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({x}\right){+}_{𝑒}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({y}\right)=\left({x}{\cdot }_{𝑒}{C}\right){+}_{𝑒}\left({y}{\cdot }_{𝑒}{C}\right)$
40 23 30 39 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({x}{+}_{𝑒}{y}\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({x}\right){+}_{𝑒}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({y}\right)$
41 4 1 2 6 16 40 esumcocn ${⊢}{\phi }\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left(\underset{{k}\in {A}}{{\sum }^{*}}{B}\right)=\underset{{k}\in {A}}{{\sum }^{*}}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({B}\right)$
42 simpr ${⊢}\left({\phi }\wedge {z}=\underset{{k}\in {A}}{{\sum }^{*}}{B}\right)\to {z}=\underset{{k}\in {A}}{{\sum }^{*}}{B}$
43 42 oveq1d ${⊢}\left({\phi }\wedge {z}=\underset{{k}\in {A}}{{\sum }^{*}}{B}\right)\to {z}{\cdot }_{𝑒}{C}=\underset{{k}\in {A}}{{\sum }^{*}}{B}{\cdot }_{𝑒}{C}$
44 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \left[0,\mathrm{+\infty }\right]$
45 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
46 45 esumcl ${⊢}\left({A}\in {V}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{{k}\in {A}}{{\sum }^{*}}{B}\in \left[0,\mathrm{+\infty }\right]$
47 1 44 46 syl2anc ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}\in \left[0,\mathrm{+\infty }\right]$
48 ovexd ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}{\cdot }_{𝑒}{C}\in \mathrm{V}$
49 7 43 47 48 fvmptd ${⊢}{\phi }\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left(\underset{{k}\in {A}}{{\sum }^{*}}{B}\right)=\underset{{k}\in {A}}{{\sum }^{*}}{B}{\cdot }_{𝑒}{C}$
50 eqidd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)$
51 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {A}\right)\wedge {z}={B}\right)\to {z}={B}$
52 51 oveq1d ${⊢}\left(\left({\phi }\wedge {k}\in {A}\right)\wedge {z}={B}\right)\to {z}{\cdot }_{𝑒}{C}={B}{\cdot }_{𝑒}{C}$
53 ovexd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}{\cdot }_{𝑒}{C}\in \mathrm{V}$
54 50 52 2 53 fvmptd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({B}\right)={B}{\cdot }_{𝑒}{C}$
55 54 esumeq2dv ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼{z}{\cdot }_{𝑒}{C}\right)\left({B}\right)=\underset{{k}\in {A}}{{\sum }^{*}}\left({B}{\cdot }_{𝑒}{C}\right)$
56 41 49 55 3eqtr3d ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}{\cdot }_{𝑒}{C}=\underset{{k}\in {A}}{{\sum }^{*}}\left({B}{\cdot }_{𝑒}{C}\right)$