Theorem esummulc2

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	esummulc2	$$⊢\phi \to C{\cdot }_{𝑒}\underset{k\in A}{{\sum }^{*}}B=\underset{k\in A}{{\sum }^{*}}\left(C{\cdot }_{𝑒}B\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		icossxr	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$$
5	4 3	sseldi	$$⊢\phi \to C\in {ℝ}^{*}$$
6		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
7	2	ralrimiva	$$⊢\phi \to \forall k\in AB\in \left[0,\mathrm{+\infty }\right]$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
9	8	esumcl	$$⊢\left(A\in V\wedge \forall k\in AB\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
10	1 7 9	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
11	6 10	sseldi	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}$$
12		xmulcom	$$⊢\left(C\in {ℝ}^{*}\wedge \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}\right)\to C{\cdot }_{𝑒}\underset{k\in A}{{\sum }^{*}}B=\underset{k\in A}{{\sum }^{*}}B{\cdot }_{𝑒}C$$
13	5 11 12	syl2anc	$$⊢\phi \to C{\cdot }_{𝑒}\underset{k\in A}{{\sum }^{*}}B=\underset{k\in A}{{\sum }^{*}}B{\cdot }_{𝑒}C$$
14	1 2 3	esummulc1	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B{\cdot }_{𝑒}C=\underset{k\in A}{{\sum }^{*}}\left(B{\cdot }_{𝑒}C\right)$$
15	6 2	sseldi	$$⊢\left(\phi \wedge k\in A\right)\to B\in {ℝ}^{*}$$
16	5	adantr	$$⊢\left(\phi \wedge k\in A\right)\to C\in {ℝ}^{*}$$
17		xmulcom	$$⊢\left(B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to B{\cdot }_{𝑒}C=C{\cdot }_{𝑒}B$$
18	15 16 17	syl2anc	$$⊢\left(\phi \wedge k\in A\right)\to B{\cdot }_{𝑒}C=C{\cdot }_{𝑒}B$$
19	18	esumeq2dv	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}\left(B{\cdot }_{𝑒}C\right)=\underset{k\in A}{{\sum }^{*}}\left(C{\cdot }_{𝑒}B\right)$$
20	13 14 19	3eqtrd	$$⊢\phi \to C{\cdot }_{𝑒}\underset{k\in A}{{\sum }^{*}}B=\underset{k\in A}{{\sum }^{*}}\left(C{\cdot }_{𝑒}B\right)$$