Metamath Proof Explorer

Theorem esumpfinvallem

Description: Lemma for esumpfinval . (Contributed by Thierry Arnoux, 28-Jun-2017)

Ref Expression
Assertion esumpfinvallem 
|- ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( CCfld gsum F ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum F ) )

Proof

Step Hyp Ref Expression
1 fex 
 |-  ( ( F : A --> ( 0 [,) +oo ) /\ A e. V ) -> F e. _V )
2 1 ancoms 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> F e. _V )
3 ovexd 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( CCfld |`s ( 0 [,) +oo ) ) e. _V )
4 ovexd 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( RR*s |`s ( 0 [,) +oo ) ) e. _V )
5 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
6 ax-resscn 
 |-  RR C_ CC
7 5 6 sstri 
 |-  ( 0 [,) +oo ) C_ CC
8 eqid 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( 0 [,) +oo ) )
9 cnfldbas 
 |-  CC = ( Base ` CCfld )
10 8 9 ressbas2 
 |-  ( ( 0 [,) +oo ) C_ CC -> ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
11 7 10 ax-mp 
 |-  ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) )
12 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
13 eqid 
 |-  ( RR*s |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( 0 [,) +oo ) )
14 xrsbas 
 |-  RR* = ( Base ` RR*s )
15 13 14 ressbas2 
 |-  ( ( 0 [,) +oo ) C_ RR* -> ( 0 [,) +oo ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
16 12 15 ax-mp 
 |-  ( 0 [,) +oo ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) )
17 11 16 eqtr3i 
 |-  ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) )
18 17 a1i 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
19 simprl 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
20 19 11 eleqtrrdi 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> x e. ( 0 [,) +oo ) )
21 simprr 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
22 21 11 eleqtrrdi 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> y e. ( 0 [,) +oo ) )
23 ge0addcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
24 ovex 
 |-  ( 0 [,) +oo ) e. _V
25 cnfldadd 
 |-  + = ( +g ` CCfld )
26 8 25 ressplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
27 24 26 ax-mp 
 |-  + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) )
28 27 oveqi 
 |-  ( x + y ) = ( x ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) y )
29 23 28 11 3eltr3g 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) y ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
30 20 22 29 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> ( x ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) y ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
31 simpl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> x e. ( 0 [,) +oo ) )
32 5 31 sselid 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> x e. RR )
33 simpr 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> y e. ( 0 [,) +oo ) )
34 5 33 sselid 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> y e. RR )
35 rexadd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x +e y ) = ( x + y ) )
36 35 eqcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) = ( x +e y ) )
37 32 34 36 syl2anc 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) = ( x +e y ) )
38 xrsadd 
 |-  +e = ( +g ` RR*s )
39 13 38 ressplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> +e = ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
40 24 39 ax-mp 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) )
41 40 oveqi 
 |-  ( x +e y ) = ( x ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) y )
42 37 28 41 3eqtr3g 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) y ) = ( x ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) y ) )
43 20 22 42 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ y e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> ( x ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) y ) = ( x ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) y ) )
44 simpr 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> F : A --> ( 0 [,) +oo ) )
45 44 ffund 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> Fun F )
46 44 frnd 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ran F C_ ( 0 [,) +oo ) )
47 46 11 sseqtrdi 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ran F C_ ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
48 2 3 4 18 30 43 45 47 gsumpropd2 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( ( CCfld |`s ( 0 [,) +oo ) ) gsum F ) = ( ( RR*s |`s ( 0 [,) +oo ) ) gsum F ) )
49 cnfldex 
 |-  CCfld e. _V
50 49 a1i 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> CCfld e. _V )
51 simpl 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> A e. V )
52 7 a1i 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( 0 [,) +oo ) C_ CC )
53 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
54 53 a1i 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> 0 e. ( 0 [,) +oo ) )
55 simpr 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. CC ) -> x e. CC )
56 55 addid2d 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. CC ) -> ( 0 + x ) = x )
57 55 addid1d 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. CC ) -> ( x + 0 ) = x )
58 56 57 jca 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. CC ) -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
59 9 25 8 50 51 52 44 54 58 gsumress 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( CCfld gsum F ) = ( ( CCfld |`s ( 0 [,) +oo ) ) gsum F ) )
60 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
61 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
62 ovex 
 |-  ( 0 [,] +oo ) e. _V
63 ressress 
 |-  ( ( ( 0 [,] +oo ) e. _V /\ ( 0 [,) +oo ) e. _V ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( ( 0 [,] +oo ) i^i ( 0 [,) +oo ) ) ) )
64 62 24 63 mp2an 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( ( 0 [,] +oo ) i^i ( 0 [,) +oo ) ) )
65 incom 
 |-  ( ( 0 [,] +oo ) i^i ( 0 [,) +oo ) ) = ( ( 0 [,) +oo ) i^i ( 0 [,] +oo ) )
66 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
67 dfss 
 |-  ( ( 0 [,) +oo ) C_ ( 0 [,] +oo ) <-> ( 0 [,) +oo ) = ( ( 0 [,) +oo ) i^i ( 0 [,] +oo ) ) )
68 66 67 mpbi 
 |-  ( 0 [,) +oo ) = ( ( 0 [,) +oo ) i^i ( 0 [,] +oo ) )
69 65 68 eqtr4i 
 |-  ( ( 0 [,] +oo ) i^i ( 0 [,) +oo ) ) = ( 0 [,) +oo )
70 69 oveq2i 
 |-  ( RR*s |`s ( ( 0 [,] +oo ) i^i ( 0 [,) +oo ) ) ) = ( RR*s |`s ( 0 [,) +oo ) )
71 64 70 eqtr2i 
 |-  ( RR*s |`s ( 0 [,) +oo ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) )
72 ovexd 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. _V )
73 66 a1i 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
74 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
75 simpr 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> x e. ( 0 [,] +oo ) )
76 74 75 sselid 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> x e. RR* )
77 xaddid2 
 |-  ( x e. RR* -> ( 0 +e x ) = x )
78 76 77 syl 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> ( 0 +e x ) = x )
79 xaddid1 
 |-  ( x e. RR* -> ( x +e 0 ) = x )
80 76 79 syl 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> ( x +e 0 ) = x )
81 78 80 jca 
 |-  ( ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
82 60 61 71 72 51 73 44 54 81 gsumress 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum F ) = ( ( RR*s |`s ( 0 [,) +oo ) ) gsum F ) )
83 48 59 82 3eqtr4d 
 |-  ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> ( CCfld gsum F ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum F ) )