Metamath Proof Explorer

Theorem esumcocn

Description: Lemma for esummulc2 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumcocn.j 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
esumcocn.a 
|- ( ph -> A e. V )
esumcocn.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumcocn.1 
|- ( ph -> C e. ( J Cn J ) )
esumcocn.0 
|- ( ph -> ( C ` 0 ) = 0 )
esumcocn.f 
|- ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) )
Assertion esumcocn 
|- ( ph -> ( C ` sum* k e. A B ) = sum* k e. A ( C ` B ) )

Proof

Step Hyp Ref Expression
1 esumcocn.j 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
2 esumcocn.a 
 |-  ( ph -> A e. V )
3 esumcocn.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4 esumcocn.1 
 |-  ( ph -> C e. ( J Cn J ) )
5 esumcocn.0 
 |-  ( ph -> ( C ` 0 ) = 0 )
6 esumcocn.f 
 |-  ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) )
7 nfv 
 |-  F/ k ph
8 nfcv 
 |-  F/_ k A
9 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
10 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
11 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
12 1 11 eqtr4i 
 |-  J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
13 10 12 tpsuni 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp -> ( 0 [,] +oo ) = U. J )
14 9 13 ax-mp 
 |-  ( 0 [,] +oo ) = U. J
15 14 14 cnf 
 |-  ( C e. ( J Cn J ) -> C : ( 0 [,] +oo ) --> ( 0 [,] +oo ) )
16 4 15 syl 
 |-  ( ph -> C : ( 0 [,] +oo ) --> ( 0 [,] +oo ) )
17 16 adantr 
 |-  ( ( ph /\ k e. A ) -> C : ( 0 [,] +oo ) --> ( 0 [,] +oo ) )
18 17 3 ffvelrnd 
 |-  ( ( ph /\ k e. A ) -> ( C ` B ) e. ( 0 [,] +oo ) )
19 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
20 19 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
21 9 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
22 cmnmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
23 19 22 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
24 23 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
25 6 3expib 
 |-  ( ph -> ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) ) )
26 25 ralrimivv 
 |-  ( ph -> A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) )
27 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
28 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
29 10 10 27 27 28 28 ismhm 
 |-  ( C e. ( ( RR*s |`s ( 0 [,] +oo ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) ) <-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd ) /\ ( C : ( 0 [,] +oo ) --> ( 0 [,] +oo ) /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) /\ ( C ` 0 ) = 0 ) ) )
30 29 biimpri 
 |-  ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd ) /\ ( C : ( 0 [,] +oo ) --> ( 0 [,] +oo ) /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) /\ ( C ` 0 ) = 0 ) ) -> C e. ( ( RR*s |`s ( 0 [,] +oo ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) ) )
31 24 24 16 26 5 30 syl23anc 
 |-  ( ph -> C e. ( ( RR*s |`s ( 0 [,] +oo ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) ) )
32 eqidd 
 |-  ( ph -> ( k e. A |-> B ) = ( k e. A |-> B ) )
33 32 3 fmpt3d 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
34 7 8 2 3 esumel 
 |-  ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
35 10 12 12 20 21 20 21 31 4 2 33 34 tsmsmhm 
 |-  ( ph -> ( C ` sum* k e. A B ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( C o. ( k e. A |-> B ) ) ) )
36 16 3 cofmpt 
 |-  ( ph -> ( C o. ( k e. A |-> B ) ) = ( k e. A |-> ( C ` B ) ) )
37 36 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( C o. ( k e. A |-> B ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( C ` B ) ) ) )
38 35 37 eleqtrd 
 |-  ( ph -> ( C ` sum* k e. A B ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( C ` B ) ) ) )
39 7 8 2 18 38 esumid 
 |-  ( ph -> sum* k e. A ( C ` B ) = ( C ` sum* k e. A B ) )
40 39 eqcomd 
 |-  ( ph -> ( C ` sum* k e. A B ) = sum* k e. A ( C ` B ) )