Metamath Proof Explorer

Theorem gsumesum

Description: Relate a group sum on ` ( RR*s |``s ( 0 , +oo ) ) ` to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

Ref Expression
Hypotheses gsumesum.0 
|- F/ k ph
gsumesum.1 
|- ( ph -> A e. Fin )
gsumesum.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
Assertion gsumesum 
|- ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = sum* k e. A B )

Proof

Step Hyp Ref Expression
1 gsumesum.0 
 |-  F/ k ph
2 gsumesum.1 
 |-  ( ph -> A e. Fin )
3 gsumesum.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4 nfcv 
 |-  F/_ k A
5 eqidd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
6 1 4 2 3 5 esumval 
 |-  ( ph -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) , RR* , < ) )
7 xrltso 
 |-  < Or RR*
8 7 a1i 
 |-  ( ph -> < Or RR* )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
11 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
12 11 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
13 3 ex 
 |-  ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
14 1 13 ralrimi 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
15 10 12 2 14 gsummptcl 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. ( 0 [,] +oo ) )
16 9 15 sselid 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. RR* )
17 pwidg 
 |-  ( A e. Fin -> A e. ~P A )
18 2 17 syl 
 |-  ( ph -> A e. ~P A )
19 18 2 elind 
 |-  ( ph -> A e. ( ~P A i^i Fin ) )
20 eqidd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
21 mpteq1 
 |-  ( x = A -> ( k e. x |-> B ) = ( k e. A |-> B ) )
22 21 oveq2d 
 |-  ( x = A -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
23 22 rspceeqv 
 |-  ( ( A e. ( ~P A i^i Fin ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) -> E. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
24 19 20 23 syl2anc 
 |-  ( ph -> E. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
25 eqid 
 |-  ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) = ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
26 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. _V
27 25 26 elrnmpti 
 |-  ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) <-> E. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) )
28 24 27 sylibr 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) )
29 mpteq1 
 |-  ( x = a -> ( k e. x |-> B ) = ( k e. a |-> B ) )
30 29 oveq2d 
 |-  ( x = a -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
31 30 cbvmptv 
 |-  ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) = ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
32 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. _V
33 31 32 elrnmpti 
 |-  ( y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) <-> E. a e. ( ~P A i^i Fin ) y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
34 33 bilani 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> E. a e. ( ~P A i^i Fin ) y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
35 11 a1i 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
36 inss2 
 |-  ( ~P A i^i Fin ) C_ Fin
37 simpr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
38 36 37 sselid 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. Fin )
39 nfv 
 |-  F/ k a e. ( ~P A i^i Fin )
40 1 39 nfan 
 |-  F/ k ( ph /\ a e. ( ~P A i^i Fin ) )
41 simpll 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> ph )
42 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
43 42 sseli 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. ~P A )
44 43 elpwid 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ A )
45 44 ad2antlr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> a C_ A )
46 simpr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. a )
47 45 46 sseldd 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. A )
48 41 47 3 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> B e. ( 0 [,] +oo ) )
49 48 ex 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( k e. a -> B e. ( 0 [,] +oo ) ) )
50 40 49 ralrimi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. k e. a B e. ( 0 [,] +oo ) )
51 10 35 38 50 gsummptcl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. ( 0 [,] +oo ) )
52 9 51 sselid 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. RR* )
53 diffi 
 |-  ( A e. Fin -> ( A \ a ) e. Fin )
54 2 53 syl 
 |-  ( ph -> ( A \ a ) e. Fin )
55 54 adantr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( A \ a ) e. Fin )
56 simpll 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> ph )
57 simpr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> k e. ( A \ a ) )
58 57 eldifad 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> k e. A )
59 56 58 3 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> B e. ( 0 [,] +oo ) )
60 59 ex 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( k e. ( A \ a ) -> B e. ( 0 [,] +oo ) ) )
61 40 60 ralrimi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. k e. ( A \ a ) B e. ( 0 [,] +oo ) )
62 10 35 55 61 gsummptcl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. ( 0 [,] +oo ) )
63 9 62 sselid 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. RR* )
64 elxrge0 
 |-  ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. ( 0 [,] +oo ) <-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. RR* /\ 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
65 64 simprbi 
 |-  ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. ( 0 [,] +oo ) -> 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) )
66 62 65 syl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) )
67 xraddge02 
 |-  ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. RR* /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. RR* ) -> ( 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) ) )
68 67 imp 
 |-  ( ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. RR* /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. RR* ) /\ 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
69 52 63 66 68 syl21anc 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
70 69 adantlr 
 |-  ( ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
71 simpll 
 |-  ( ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> ph )
72 44 adantl 
 |-  ( ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> a C_ A )
73 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
74 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
75 11 a1i 
 |-  ( ( ph /\ a C_ A ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
76 2 adantr 
 |-  ( ( ph /\ a C_ A ) -> A e. Fin )
77 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
78 1 3 77 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
79 78 adantr 
 |-  ( ( ph /\ a C_ A ) -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
80 77 fnmpt 
 |-  ( A. k e. A B e. ( 0 [,] +oo ) -> ( k e. A |-> B ) Fn A )
81 14 80 syl 
 |-  ( ph -> ( k e. A |-> B ) Fn A )
82 c0ex 
 |-  0 e. _V
83 82 a1i 
 |-  ( ph -> 0 e. _V )
84 81 2 83 fndmfifsupp 
 |-  ( ph -> ( k e. A |-> B ) finSupp 0 )
85 84 adantr 
 |-  ( ( ph /\ a C_ A ) -> ( k e. A |-> B ) finSupp 0 )
86 disjdif 
 |-  ( a i^i ( A \ a ) ) = (/)
87 86 a1i 
 |-  ( ( ph /\ a C_ A ) -> ( a i^i ( A \ a ) ) = (/) )
88 undif 
 |-  ( a C_ A <-> ( a u. ( A \ a ) ) = A )
89 88 biimpi 
 |-  ( a C_ A -> ( a u. ( A \ a ) ) = A )
90 89 eqcomd 
 |-  ( a C_ A -> A = ( a u. ( A \ a ) ) )
91 90 adantl 
 |-  ( ( ph /\ a C_ A ) -> A = ( a u. ( A \ a ) ) )
92 10 73 74 75 76 79 85 87 91 gsumsplit 
 |-  ( ( ph /\ a C_ A ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` a ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` ( A \ a ) ) ) ) )
93 resmpt 
 |-  ( a C_ A -> ( ( k e. A |-> B ) |` a ) = ( k e. a |-> B ) )
94 93 oveq2d 
 |-  ( a C_ A -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` a ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
95 94 adantl 
 |-  ( ( ph /\ a C_ A ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` a ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
96 difss 
 |-  ( A \ a ) C_ A
97 resmpt 
 |-  ( ( A \ a ) C_ A -> ( ( k e. A |-> B ) |` ( A \ a ) ) = ( k e. ( A \ a ) |-> B ) )
98 96 97 ax-mp 
 |-  ( ( k e. A |-> B ) |` ( A \ a ) ) = ( k e. ( A \ a ) |-> B )
99 98 oveq2i 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` ( A \ a ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) )
100 99 a1i 
 |-  ( ( ph /\ a C_ A ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` ( A \ a ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) )
101 95 100 oveq12d 
 |-  ( ( ph /\ a C_ A ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` a ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` ( A \ a ) ) ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
102 92 101 eqtrd 
 |-  ( ( ph /\ a C_ A ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
103 71 72 102 syl2anc 
 |-  ( ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) +e ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) ) )
104 70 103 breqtrrd 
 |-  ( ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
105 104 ralrimiva 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> A. a e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
106 r19.29r 
 |-  ( ( E. a e. ( ~P A i^i Fin ) y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) /\ A. a e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) -> E. a e. ( ~P A i^i Fin ) ( y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) )
107 breq1 
 |-  ( y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) -> ( y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) <-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) )
108 107 biimpar 
 |-  ( ( y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) -> y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
109 108 rexlimivw 
 |-  ( E. a e. ( ~P A i^i Fin ) ( y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) -> y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
110 106 109 syl 
 |-  ( ( E. a e. ( ~P A i^i Fin ) y = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) /\ A. a e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) -> y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
111 34 105 110 syl2anc 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
112 16 adantr 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. RR* )
113 11 a1i 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
114 simpr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
115 36 114 sselid 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
116 nfv 
 |-  F/ k x e. ( ~P A i^i Fin )
117 1 116 nfan 
 |-  F/ k ( ph /\ x e. ( ~P A i^i Fin ) )
118 simpll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ph )
119 42 sseli 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
120 119 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x e. ~P A )
121 120 elpwid 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x C_ A )
122 simpr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. x )
123 121 122 sseldd 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. A )
124 118 123 3 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. ( 0 [,] +oo ) )
125 124 ex 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( k e. x -> B e. ( 0 [,] +oo ) ) )
126 117 125 ralrimi 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> A. k e. x B e. ( 0 [,] +oo ) )
127 10 113 115 126 gsummptcl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. ( 0 [,] +oo ) )
128 9 127 sselid 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. RR* )
129 128 ralrimiva 
 |-  ( ph -> A. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. RR* )
130 25 rnmptss 
 |-  ( A. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. RR* -> ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) C_ RR* )
131 129 130 syl 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) C_ RR* )
132 131 sselda 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> y e. RR* )
133 xrltnle 
 |-  ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. RR* /\ y e. RR* ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) < y <-> -. y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) ) )
134 133 con2bid 
 |-  ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. RR* /\ y e. RR* ) -> ( y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) <-> -. ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) < y ) )
135 112 132 134 syl2anc 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> ( y <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) <-> -. ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) < y ) )
136 111 135 mpbid 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> -. ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) < y )
137 8 16 28 136 supmax 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) , RR* , < ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )
138 6 137 eqtr2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = sum* k e. A B )