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 
|- ( ph -> A e. V )
esummulc2.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esummulc2.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
Assertion esummulc1 
|- ( ph -> ( sum* k e. A B *e C ) = sum* k e. A ( B *e C ) )

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 eqid 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
5 eqid 
 |-  ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) = ( z e. ( 0 [,] +oo ) |-> ( z *e C ) )
6 4 5 3 xrge0mulc1cn 
 |-  ( ph -> ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) e. ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) )
7 eqidd 
 |-  ( ph -> ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) = ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) )
8 oveq1 
 |-  ( z = 0 -> ( z *e C ) = ( 0 *e C ) )
9 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
10 9 3 sseldi 
 |-  ( ph -> C e. RR* )
11 xmul02 
 |-  ( C e. RR* -> ( 0 *e C ) = 0 )
12 10 11 syl 
 |-  ( ph -> ( 0 *e C ) = 0 )
13 8 12 sylan9eqr 
 |-  ( ( ph /\ z = 0 ) -> ( z *e C ) = 0 )
14 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
15 14 a1i 
 |-  ( ph -> 0 e. ( 0 [,] +oo ) )
16 7 13 15 15 fvmptd 
 |-  ( ph -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` 0 ) = 0 )
17 simp2 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> x e. ( 0 [,] +oo ) )
18 simp3 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> y e. ( 0 [,] +oo ) )
19 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
20 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> C e. ( 0 [,) +oo ) )
21 19 20 sseldi 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> C e. ( 0 [,] +oo ) )
22 xrge0adddir 
 |-  ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( x +e y ) *e C ) = ( ( x *e C ) +e ( y *e C ) ) )
23 17 18 21 22 syl3anc 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( x +e y ) *e C ) = ( ( x *e C ) +e ( y *e C ) ) )
24 eqidd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) = ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) )
25 simpr 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = ( x +e y ) ) -> z = ( x +e y ) )
26 25 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = ( x +e y ) ) -> ( z *e C ) = ( ( x +e y ) *e C ) )
27 ge0xaddcl 
 |-  ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x +e y ) e. ( 0 [,] +oo ) )
28 27 3adant1 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x +e y ) e. ( 0 [,] +oo ) )
29 ovexd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( x +e y ) *e C ) e. _V )
30 24 26 28 29 fvmptd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` ( x +e y ) ) = ( ( x +e y ) *e C ) )
31 simpr 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = x ) -> z = x )
32 31 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = x ) -> ( z *e C ) = ( x *e C ) )
33 ovexd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x *e C ) e. _V )
34 24 32 17 33 fvmptd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` x ) = ( x *e C ) )
35 simpr 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = y ) -> z = y )
36 35 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) /\ z = y ) -> ( z *e C ) = ( y *e C ) )
37 ovexd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( y *e C ) e. _V )
38 24 36 18 37 fvmptd 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` y ) = ( y *e C ) )
39 34 38 oveq12d 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` x ) +e ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` y ) ) = ( ( x *e C ) +e ( y *e C ) ) )
40 23 30 39 3eqtr4d 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` ( x +e y ) ) = ( ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` x ) +e ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` y ) ) )
41 4 1 2 6 16 40 esumcocn 
 |-  ( ph -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` sum* k e. A B ) = sum* k e. A ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` B ) )
42 simpr 
 |-  ( ( ph /\ z = sum* k e. A B ) -> z = sum* k e. A B )
43 42 oveq1d 
 |-  ( ( ph /\ z = sum* k e. A B ) -> ( z *e C ) = ( sum* k e. A B *e C ) )
44 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
45 nfcv 
 |-  F/_ k A
46 45 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
47 1 44 46 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
48 ovexd 
 |-  ( ph -> ( sum* k e. A B *e C ) e. _V )
49 7 43 47 48 fvmptd 
 |-  ( ph -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` sum* k e. A B ) = ( sum* k e. A B *e C ) )
50 eqidd 
 |-  ( ( ph /\ k e. A ) -> ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) = ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) )
51 simpr 
 |-  ( ( ( ph /\ k e. A ) /\ z = B ) -> z = B )
52 51 oveq1d 
 |-  ( ( ( ph /\ k e. A ) /\ z = B ) -> ( z *e C ) = ( B *e C ) )
53 ovexd 
 |-  ( ( ph /\ k e. A ) -> ( B *e C ) e. _V )
54 50 52 2 53 fvmptd 
 |-  ( ( ph /\ k e. A ) -> ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` B ) = ( B *e C ) )
55 54 esumeq2dv 
 |-  ( ph -> sum* k e. A ( ( z e. ( 0 [,] +oo ) |-> ( z *e C ) ) ` B ) = sum* k e. A ( B *e C ) )
56 41 49 55 3eqtr3d 
 |-  ( ph -> ( sum* k e. A B *e C ) = sum* k e. A ( B *e C ) )