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 sseldi 
 |-  ( 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 simpr 
 |-  ( ( ph /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) ) -> y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) )
30 mpteq1 
 |-  ( x = a -> ( k e. x |-> B ) = ( k e. a |-> B ) )
31 30 oveq2d 
 |-  ( x = a -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) )
32 31 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 ) ) )
33 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. _V
34 32 33 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 ) ) )
35 29 34 sylib 
 |-  ( ( 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 ) ) )
36 11 a1i 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
37 inss2 
 |-  ( ~P A i^i Fin ) C_ Fin
38 simpr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
39 37 38 sseldi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. Fin )
40 nfv 
 |-  F/ k a e. ( ~P A i^i Fin )
41 1 40 nfan 
 |-  F/ k ( ph /\ a e. ( ~P A i^i Fin ) )
42 simpll 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> ph )
43 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
44 43 sseli 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. ~P A )
45 44 elpwid 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ A )
46 45 ad2antlr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> a C_ A )
47 simpr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. a )
48 46 47 sseldd 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. A )
49 42 48 3 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> B e. ( 0 [,] +oo ) )
50 49 ex 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( k e. a -> B e. ( 0 [,] +oo ) ) )
51 41 50 ralrimi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. k e. a B e. ( 0 [,] +oo ) )
52 10 36 39 51 gsummptcl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. ( 0 [,] +oo ) )
53 9 52 sseldi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. a |-> B ) ) e. RR* )
54 diffi 
 |-  ( A e. Fin -> ( A \ a ) e. Fin )
55 2 54 syl 
 |-  ( ph -> ( A \ a ) e. Fin )
56 55 adantr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( A \ a ) e. Fin )
57 simpll 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> ph )
58 simpr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> k e. ( A \ a ) )
59 58 eldifad 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> k e. A )
60 57 59 3 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. ( A \ a ) ) -> B e. ( 0 [,] +oo ) )
61 60 ex 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( k e. ( A \ a ) -> B e. ( 0 [,] +oo ) ) )
62 41 61 ralrimi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. k e. ( A \ a ) B e. ( 0 [,] +oo ) )
63 10 36 56 62 gsummptcl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. ( 0 [,] +oo ) )
64 9 63 sseldi 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) e. RR* )
65 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 ) ) ) )
66 65 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 ) ) )
67 63 66 syl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> 0 <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) ) )
68 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 ) ) ) ) )
69 68 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 ) ) ) )
70 53 64 67 69 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 ) ) ) )
71 70 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 ) ) ) )
72 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 )
73 45 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 )
74 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
75 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
76 11 a1i 
 |-  ( ( ph /\ a C_ A ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
77 2 adantr 
 |-  ( ( ph /\ a C_ A ) -> A e. Fin )
78 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
79 1 3 78 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
80 79 adantr 
 |-  ( ( ph /\ a C_ A ) -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
81 78 fnmpt 
 |-  ( A. k e. A B e. ( 0 [,] +oo ) -> ( k e. A |-> B ) Fn A )
82 14 81 syl 
 |-  ( ph -> ( k e. A |-> B ) Fn A )
83 c0ex 
 |-  0 e. _V
84 83 a1i 
 |-  ( ph -> 0 e. _V )
85 82 2 84 fndmfifsupp 
 |-  ( ph -> ( k e. A |-> B ) finSupp 0 )
86 85 adantr 
 |-  ( ( ph /\ a C_ A ) -> ( k e. A |-> B ) finSupp 0 )
87 disjdif 
 |-  ( a i^i ( A \ a ) ) = (/)
88 87 a1i 
 |-  ( ( ph /\ a C_ A ) -> ( a i^i ( A \ a ) ) = (/) )
89 undif 
 |-  ( a C_ A <-> ( a u. ( A \ a ) ) = A )
90 89 biimpi 
 |-  ( a C_ A -> ( a u. ( A \ a ) ) = A )
91 90 eqcomd 
 |-  ( a C_ A -> A = ( a u. ( A \ a ) ) )
92 91 adantl 
 |-  ( ( ph /\ a C_ A ) -> A = ( a u. ( A \ a ) ) )
93 10 74 75 76 77 80 86 88 92 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 ) ) ) ) )
94 resmpt 
 |-  ( a C_ A -> ( ( k e. A |-> B ) |` a ) = ( k e. a |-> B ) )
95 94 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 ) ) )
96 95 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 ) ) )
97 difss 
 |-  ( A \ a ) C_ A
98 resmpt 
 |-  ( ( A \ a ) C_ A -> ( ( k e. A |-> B ) |` ( A \ a ) ) = ( k e. ( A \ a ) |-> B ) )
99 97 98 ax-mp 
 |-  ( ( k e. A |-> B ) |` ( A \ a ) ) = ( k e. ( A \ a ) |-> B )
100 99 oveq2i 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. A |-> B ) |` ( A \ a ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( A \ a ) |-> B ) )
101 100 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 ) ) )
102 96 101 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 ) ) ) )
103 93 102 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 ) ) ) )
104 72 73 103 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 ) ) ) )
105 71 104 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 ) ) )
106 105 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 ) ) )
107 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 ) ) ) )
108 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 ) ) ) )
109 108 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 ) ) )
110 109 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 ) ) )
111 107 110 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 ) ) )
112 35 106 111 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 ) ) )
113 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* )
114 11 a1i 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
115 simpr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
116 37 115 sseldi 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
117 nfv 
 |-  F/ k x e. ( ~P A i^i Fin )
118 1 117 nfan 
 |-  F/ k ( ph /\ x e. ( ~P A i^i Fin ) )
119 simpll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ph )
120 43 sseli 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
121 120 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x e. ~P A )
122 121 elpwid 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x C_ A )
123 simpr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. x )
124 122 123 sseldd 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. A )
125 119 124 3 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. ( 0 [,] +oo ) )
126 125 ex 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( k e. x -> B e. ( 0 [,] +oo ) ) )
127 118 126 ralrimi 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> A. k e. x B e. ( 0 [,] +oo ) )
128 10 114 116 127 gsummptcl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. ( 0 [,] +oo ) )
129 9 128 sseldi 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. RR* )
130 129 ralrimiva 
 |-  ( ph -> A. x e. ( ~P A i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) e. RR* )
131 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* )
132 130 131 syl 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) ) C_ RR* )
133 132 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* )
134 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 ) ) ) )
135 134 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 ) )
136 113 133 135 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 ) )
137 112 136 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 )
138 8 16 28 137 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 ) ) )
139 6 138 eqtr2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) = sum* k e. A B )