Theorem esummulc2

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

	Ref	Expression
Hypotheses	esummulc2.a	|- ( ph -> A e. V )
	esummulc2.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
	esummulc2.c	|- ( ph -> C e. ( 0 [,) +oo ) )
Assertion	esummulc2	|- ( ph -> ( C *e sum* k e. A B ) = sum* k e. A ( C *e B ) )

Proof

Step	Hyp	Ref	Expression
1		esummulc2.a	|- ( ph -> A e. V )
2		esummulc2.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
3		esummulc2.c	|- ( ph -> C e. ( 0 [,) +oo ) )
4		icossxr	|- ( 0 [,) +oo ) C_ RR*
5	4 3	sselid	|- ( ph -> C e. RR* )
6		iccssxr	|- ( 0 [,] +oo ) C_ RR*
7	2	ralrimiva	|- ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
8		nfcv	|- F/_ k A
9	8	esumcl	|- ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
10	1 7 9	syl2anc	|- ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
11	6 10	sselid	|- ( ph -> sum* k e. A B e. RR* )
12		xmulcom	|- ( ( C e. RR* /\ sum* k e. A B e. RR* ) -> ( C *e sum* k e. A B ) = ( sum* k e. A B *e C ) )
13	5 11 12	syl2anc	|- ( ph -> ( C *e sum* k e. A B ) = ( sum* k e. A B *e C ) )
14	1 2 3	esummulc1	|- ( ph -> ( sum* k e. A B *e C ) = sum* k e. A ( B *e C ) )
15	6 2	sselid	|- ( ( ph /\ k e. A ) -> B e. RR* )
16	5	adantr	|- ( ( ph /\ k e. A ) -> C e. RR* )
17		xmulcom	|- ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) = ( C *e B ) )
18	15 16 17	syl2anc	|- ( ( ph /\ k e. A ) -> ( B *e C ) = ( C *e B ) )
19	18	esumeq2dv	|- ( ph -> sum* k e. A ( B *e C ) = sum* k e. A ( C *e B ) )
20	13 14 19	3eqtrd	|- ( ph -> ( C *e sum* k e. A B ) = sum* k e. A ( C *e B ) )