Metamath Proof Explorer

Theorem sge0f1o

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0f1o.1 
|- F/ k ph
sge0f1o.2 
|- F/ n ph
sge0f1o.3 
|- ( k = G -> B = D )
sge0f1o.4 
|- ( ph -> C e. V )
sge0f1o.5 
|- ( ph -> F : C -1-1-onto-> A )
sge0f1o.6 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
sge0f1o.7 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
Assertion sge0f1o 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )

Proof

Step Hyp Ref Expression
1 sge0f1o.1 
 |-  F/ k ph
2 sge0f1o.2 
 |-  F/ n ph
3 sge0f1o.3 
 |-  ( k = G -> B = D )
4 sge0f1o.4 
 |-  ( ph -> C e. V )
5 sge0f1o.5 
 |-  ( ph -> F : C -1-1-onto-> A )
6 sge0f1o.6 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) = G )
7 sge0f1o.7 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
8 f1ofo 
 |-  ( F : C -1-1-onto-> A -> F : C -onto-> A )
9 5 8 syl 
 |-  ( ph -> F : C -onto-> A )
10 fornex 
 |-  ( C e. V -> ( F : C -onto-> A -> A e. _V ) )
11 4 9 10 sylc 
 |-  ( ph -> A e. _V )
12 11 adantr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> A e. _V )
13 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
14 1 7 13 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
15 14 adantr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
16 pnfex 
 |-  +oo e. _V
17 eqid 
 |-  ( n e. C |-> D ) = ( n e. C |-> D )
18 17 elrnmpt 
 |-  ( +oo e. _V -> ( +oo e. ran ( n e. C |-> D ) <-> E. n e. C +oo = D ) )
19 16 18 ax-mp 
 |-  ( +oo e. ran ( n e. C |-> D ) <-> E. n e. C +oo = D )
20 19 biimpi 
 |-  ( +oo e. ran ( n e. C |-> D ) -> E. n e. C +oo = D )
21 20 adantl 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> E. n e. C +oo = D )
22 nfv 
 |-  F/ n +oo e. ran ( k e. A |-> B )
23 simp3 
 |-  ( ( ph /\ n e. C /\ +oo = D ) -> +oo = D )
24 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
25 5 24 syl 
 |-  ( ph -> F : C --> A )
26 25 ffvelrnda 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) e. A )
27 nfcv 
 |-  F/_ k ( F ` n )
28 nfv 
 |-  F/ k ( F ` n ) = G
29 27 nfcsb1 
 |-  F/_ k [_ ( F ` n ) / k ]_ B
30 nfcv 
 |-  F/_ k D
31 29 30 nfeq 
 |-  F/ k [_ ( F ` n ) / k ]_ B = D
32 28 31 nfim 
 |-  F/ k ( ( F ` n ) = G -> [_ ( F ` n ) / k ]_ B = D )
33 eqeq1 
 |-  ( k = ( F ` n ) -> ( k = G <-> ( F ` n ) = G ) )
34 csbeq1a 
 |-  ( k = ( F ` n ) -> B = [_ ( F ` n ) / k ]_ B )
35 34 eqeq1d 
 |-  ( k = ( F ` n ) -> ( B = D <-> [_ ( F ` n ) / k ]_ B = D ) )
36 33 35 imbi12d 
 |-  ( k = ( F ` n ) -> ( ( k = G -> B = D ) <-> ( ( F ` n ) = G -> [_ ( F ` n ) / k ]_ B = D ) ) )
37 27 32 36 3 vtoclgf 
 |-  ( ( F ` n ) e. A -> ( ( F ` n ) = G -> [_ ( F ` n ) / k ]_ B = D ) )
38 26 6 37 sylc 
 |-  ( ( ph /\ n e. C ) -> [_ ( F ` n ) / k ]_ B = D )
39 38 eqcomd 
 |-  ( ( ph /\ n e. C ) -> D = [_ ( F ` n ) / k ]_ B )
40 39 3adant3 
 |-  ( ( ph /\ n e. C /\ +oo = D ) -> D = [_ ( F ` n ) / k ]_ B )
41 23 40 eqtrd 
 |-  ( ( ph /\ n e. C /\ +oo = D ) -> +oo = [_ ( F ` n ) / k ]_ B )
42 simpl 
 |-  ( ( ph /\ n e. C ) -> ph )
43 42 26 jca 
 |-  ( ( ph /\ n e. C ) -> ( ph /\ ( F ` n ) e. A ) )
44 nfv 
 |-  F/ k ( F ` n ) e. A
45 1 44 nfan 
 |-  F/ k ( ph /\ ( F ` n ) e. A )
46 29 nfel1 
 |-  F/ k [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo )
47 45 46 nfim 
 |-  F/ k ( ( ph /\ ( F ` n ) e. A ) -> [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) )
48 eleq1 
 |-  ( k = ( F ` n ) -> ( k e. A <-> ( F ` n ) e. A ) )
49 48 anbi2d 
 |-  ( k = ( F ` n ) -> ( ( ph /\ k e. A ) <-> ( ph /\ ( F ` n ) e. A ) ) )
50 34 eleq1d 
 |-  ( k = ( F ` n ) -> ( B e. ( 0 [,] +oo ) <-> [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) ) )
51 49 50 imbi12d 
 |-  ( k = ( F ` n ) -> ( ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) ) <-> ( ( ph /\ ( F ` n ) e. A ) -> [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) ) ) )
52 27 47 51 7 vtoclgf 
 |-  ( ( F ` n ) e. A -> ( ( ph /\ ( F ` n ) e. A ) -> [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) ) )
53 26 43 52 sylc 
 |-  ( ( ph /\ n e. C ) -> [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) )
54 29 13 34 elrnmpt1sf 
 |-  ( ( ( F ` n ) e. A /\ [_ ( F ` n ) / k ]_ B e. ( 0 [,] +oo ) ) -> [_ ( F ` n ) / k ]_ B e. ran ( k e. A |-> B ) )
55 26 53 54 syl2anc 
 |-  ( ( ph /\ n e. C ) -> [_ ( F ` n ) / k ]_ B e. ran ( k e. A |-> B ) )
56 55 3adant3 
 |-  ( ( ph /\ n e. C /\ +oo = D ) -> [_ ( F ` n ) / k ]_ B e. ran ( k e. A |-> B ) )
57 41 56 eqeltrd 
 |-  ( ( ph /\ n e. C /\ +oo = D ) -> +oo e. ran ( k e. A |-> B ) )
58 57 3exp 
 |-  ( ph -> ( n e. C -> ( +oo = D -> +oo e. ran ( k e. A |-> B ) ) ) )
59 2 22 58 rexlimd 
 |-  ( ph -> ( E. n e. C +oo = D -> +oo e. ran ( k e. A |-> B ) ) )
60 59 adantr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( E. n e. C +oo = D -> +oo e. ran ( k e. A |-> B ) ) )
61 21 60 mpd 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> +oo e. ran ( k e. A |-> B ) )
62 12 15 61 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( k e. A |-> B ) ) = +oo )
63 4 adantr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> C e. V )
64 39 53 eqeltrd 
 |-  ( ( ph /\ n e. C ) -> D e. ( 0 [,] +oo ) )
65 2 64 17 fmptdf 
 |-  ( ph -> ( n e. C |-> D ) : C --> ( 0 [,] +oo ) )
66 65 adantr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( n e. C |-> D ) : C --> ( 0 [,] +oo ) )
67 simpr 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> +oo e. ran ( n e. C |-> D ) )
68 63 66 67 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( n e. C |-> D ) ) = +oo )
69 62 68 eqtr4d 
 |-  ( ( ph /\ +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )
70 sumex 
 |-  sum_ k e. y B e. _V
71 70 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y B e. _V )
72 cnvimass 
 |-  ( `' F " y ) C_ dom F
73 72 25 fssdm 
 |-  ( ph -> ( `' F " y ) C_ C )
74 25 4 fexd 
 |-  ( ph -> F e. _V )
75 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
76 74 75 syl 
 |-  ( ph -> `' F e. _V )
77 imaexg 
 |-  ( `' F e. _V -> ( `' F " y ) e. _V )
78 76 77 syl 
 |-  ( ph -> ( `' F " y ) e. _V )
79 elpwg 
 |-  ( ( `' F " y ) e. _V -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
80 78 79 syl 
 |-  ( ph -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
81 73 80 mpbird 
 |-  ( ph -> ( `' F " y ) e. ~P C )
82 81 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ~P C )
83 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
84 5 83 syl 
 |-  ( ph -> `' F : A -1-1-onto-> C )
85 f1ofun 
 |-  ( `' F : A -1-1-onto-> C -> Fun `' F )
86 84 85 syl 
 |-  ( ph -> Fun `' F )
87 86 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> Fun `' F )
88 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
89 88 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
90 imafi 
 |-  ( ( Fun `' F /\ y e. Fin ) -> ( `' F " y ) e. Fin )
91 87 89 90 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. Fin )
92 82 91 elind 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
93 92 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
94 nfv 
 |-  F/ k -. +oo e. ran ( n e. C |-> D )
95 1 94 nfan 
 |-  F/ k ( ph /\ -. +oo e. ran ( n e. C |-> D ) )
96 nfv 
 |-  F/ k y e. ( ~P A i^i Fin )
97 95 96 nfan 
 |-  F/ k ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) )
98 nfcv 
 |-  F/_ n +oo
99 nfmpt1 
 |-  F/_ n ( n e. C |-> D )
100 99 nfrn 
 |-  F/_ n ran ( n e. C |-> D )
101 98 100 nfel 
 |-  F/ n +oo e. ran ( n e. C |-> D )
102 101 nfn 
 |-  F/ n -. +oo e. ran ( n e. C |-> D )
103 2 102 nfan 
 |-  F/ n ( ph /\ -. +oo e. ran ( n e. C |-> D ) )
104 nfv 
 |-  F/ n y e. ( ~P A i^i Fin )
105 103 104 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) )
106 91 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. Fin )
107 f1of1 
 |-  ( F : C -1-1-onto-> A -> F : C -1-1-> A )
108 5 107 syl 
 |-  ( ph -> F : C -1-1-> A )
109 108 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> F : C -1-1-> A )
110 80 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
111 82 110 mpbid 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) C_ C )
112 f1ores 
 |-  ( ( F : C -1-1-> A /\ ( `' F " y ) C_ C ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> ( F " ( `' F " y ) ) )
113 109 111 112 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> ( F " ( `' F " y ) ) )
114 9 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> F : C -onto-> A )
115 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
116 115 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
117 foimacnv 
 |-  ( ( F : C -onto-> A /\ y C_ A ) -> ( F " ( `' F " y ) ) = y )
118 114 116 117 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F " ( `' F " y ) ) = y )
119 118 f1oeq3d 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> ( F " ( `' F " y ) ) <-> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> y ) )
120 113 119 mpbid 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> y )
121 120 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> y )
122 78 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( `' F " y ) e. _V )
123 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ph )
124 92 adantr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
125 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> n e. ( `' F " y ) )
126 123 124 125 jca31 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ n e. ( `' F " y ) ) )
127 eleq1 
 |-  ( x = ( `' F " y ) -> ( x e. ( ~P C i^i Fin ) <-> ( `' F " y ) e. ( ~P C i^i Fin ) ) )
128 127 anbi2d 
 |-  ( x = ( `' F " y ) -> ( ( ph /\ x e. ( ~P C i^i Fin ) ) <-> ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) ) )
129 eleq2 
 |-  ( x = ( `' F " y ) -> ( n e. x <-> n e. ( `' F " y ) ) )
130 128 129 anbi12d 
 |-  ( x = ( `' F " y ) -> ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) <-> ( ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ n e. ( `' F " y ) ) ) )
131 reseq2 
 |-  ( x = ( `' F " y ) -> ( F |` x ) = ( F |` ( `' F " y ) ) )
132 131 fveq1d 
 |-  ( x = ( `' F " y ) -> ( ( F |` x ) ` n ) = ( ( F |` ( `' F " y ) ) ` n ) )
133 132 eqeq1d 
 |-  ( x = ( `' F " y ) -> ( ( ( F |` x ) ` n ) = G <-> ( ( F |` ( `' F " y ) ) ` n ) = G ) )
134 130 133 imbi12d 
 |-  ( x = ( `' F " y ) -> ( ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = G ) <-> ( ( ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G ) ) )
135 fvres 
 |-  ( n e. x -> ( ( F |` x ) ` n ) = ( F ` n ) )
136 135 adantl 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = ( F ` n ) )
137 simpll 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ph )
138 elpwinss 
 |-  ( x e. ( ~P C i^i Fin ) -> x C_ C )
139 138 adantl 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> x C_ C )
140 139 sselda 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> n e. C )
141 137 140 6 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( F ` n ) = G )
142 136 141 eqtrd 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = G )
143 134 142 vtoclg 
 |-  ( ( `' F " y ) e. _V -> ( ( ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G ) )
144 122 126 143 sylc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G )
145 144 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G )
146 78 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. _V )
147 simpll 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) )
148 81 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. ~P C )
149 106 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. Fin )
150 148 149 elind 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
151 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. y )
152 118 eqcomd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y = ( F " ( `' F " y ) ) )
153 152 adantr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> y = ( F " ( `' F " y ) ) )
154 151 153 eleqtrd 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. ( F " ( `' F " y ) ) )
155 154 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. ( F " ( `' F " y ) ) )
156 147 150 155 jca31 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ k e. ( F " ( `' F " y ) ) ) )
157 127 anbi2d 
 |-  ( x = ( `' F " y ) -> ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) <-> ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) ) )
158 imaeq2 
 |-  ( x = ( `' F " y ) -> ( F " x ) = ( F " ( `' F " y ) ) )
159 158 eleq2d 
 |-  ( x = ( `' F " y ) -> ( k e. ( F " x ) <-> k e. ( F " ( `' F " y ) ) ) )
160 157 159 anbi12d 
 |-  ( x = ( `' F " y ) -> ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) <-> ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ k e. ( F " ( `' F " y ) ) ) ) )
161 160 imbi1d 
 |-  ( x = ( `' F " y ) -> ( ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. CC ) <-> ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ k e. ( F " ( `' F " y ) ) ) -> B e. CC ) ) )
162 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
163 ax-resscn 
 |-  RR C_ CC
164 162 163 sstri 
 |-  ( 0 [,) +oo ) C_ CC
165 simplll 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> ph )
166 simpllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> -. +oo e. ran ( n e. C |-> D ) )
167 fimass 
 |-  ( F : C --> A -> ( F " x ) C_ A )
168 25 167 syl 
 |-  ( ph -> ( F " x ) C_ A )
169 168 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> ( F " x ) C_ A )
170 simpr 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. ( F " x ) )
171 169 170 sseldd 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. A )
172 171 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. A )
173 foelrni 
 |-  ( ( F : C -onto-> A /\ k e. A ) -> E. n e. C ( F ` n ) = k )
174 9 173 sylan 
 |-  ( ( ph /\ k e. A ) -> E. n e. C ( F ` n ) = k )
175 174 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> E. n e. C ( F ` n ) = k )
176 nfv 
 |-  F/ n k e. A
177 103 176 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A )
178 nfv 
 |-  F/ n B e. ( 0 [,) +oo )
179 csbid 
 |-  [_ k / k ]_ B = B
180 179 eqcomi 
 |-  B = [_ k / k ]_ B
181 180 a1i 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> B = [_ k / k ]_ B )
182 id 
 |-  ( ( F ` n ) = k -> ( F ` n ) = k )
183 182 eqcomd 
 |-  ( ( F ` n ) = k -> k = ( F ` n ) )
184 183 csbeq1d 
 |-  ( ( F ` n ) = k -> [_ k / k ]_ B = [_ ( F ` n ) / k ]_ B )
185 184 3ad2ant3 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> [_ k / k ]_ B = [_ ( F ` n ) / k ]_ B )
186 38 idi 
 |-  ( ( ph /\ n e. C ) -> [_ ( F ` n ) / k ]_ B = D )
187 186 3adant3 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> [_ ( F ` n ) / k ]_ B = D )
188 181 185 187 3eqtrd 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> B = D )
189 188 3adant1r 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> B = D )
190 0xr 
 |-  0 e. RR*
191 190 a1i 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> 0 e. RR* )
192 pnfxr 
 |-  +oo e. RR*
193 192 a1i 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. RR* )
194 64 adantr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D e. ( 0 [,] +oo ) )
195 simpr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> -. D e. ( 0 [,) +oo ) )
196 191 193 194 195 eliccnelico 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D = +oo )
197 196 eqcomd 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo = D )
198 simpr 
 |-  ( ( ph /\ n e. C ) -> n e. C )
199 64 idi 
 |-  ( ( ph /\ n e. C ) -> D e. ( 0 [,] +oo ) )
200 17 elrnmpt1 
 |-  ( ( n e. C /\ D e. ( 0 [,] +oo ) ) -> D e. ran ( n e. C |-> D ) )
201 198 199 200 syl2anc 
 |-  ( ( ph /\ n e. C ) -> D e. ran ( n e. C |-> D ) )
202 201 adantr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D e. ran ( n e. C |-> D ) )
203 197 202 eqeltrd 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. ran ( n e. C |-> D ) )
204 203 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. ran ( n e. C |-> D ) )
205 simpllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> -. +oo e. ran ( n e. C |-> D ) )
206 204 205 condan 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) -> D e. ( 0 [,) +oo ) )
207 206 3adant3 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> D e. ( 0 [,) +oo ) )
208 189 207 eqeltrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> B e. ( 0 [,) +oo ) )
209 208 3exp 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( n e. C -> ( ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) ) )
210 209 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> ( n e. C -> ( ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) ) )
211 177 178 210 rexlimd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> ( E. n e. C ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) )
212 175 211 mpd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> B e. ( 0 [,) +oo ) )
213 165 166 172 212 syl21anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. ( 0 [,) +oo ) )
214 164 213 sselid 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. CC )
215 214 idi 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. CC )
216 161 215 vtoclg 
 |-  ( ( `' F " y ) e. _V -> ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ k e. ( F " ( `' F " y ) ) ) -> B e. CC ) )
217 146 156 216 sylc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> B e. CC )
218 97 105 3 106 121 145 217 fsumf1of 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y B = sum_ n e. ( `' F " y ) D )
219 sumeq1 
 |-  ( x = ( `' F " y ) -> sum_ n e. x D = sum_ n e. ( `' F " y ) D )
220 219 rspceeqv 
 |-  ( ( ( `' F " y ) e. ( ~P C i^i Fin ) /\ sum_ k e. y B = sum_ n e. ( `' F " y ) D ) -> E. x e. ( ~P C i^i Fin ) sum_ k e. y B = sum_ n e. x D )
221 93 218 220 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> E. x e. ( ~P C i^i Fin ) sum_ k e. y B = sum_ n e. x D )
222 71 221 rnmptssrn 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) C_ ran ( x e. ( ~P C i^i Fin ) |-> sum_ n e. x D ) )
223 sumex 
 |-  sum_ n e. x D e. _V
224 223 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> sum_ n e. x D e. _V )
225 11 168 ssexd 
 |-  ( ph -> ( F " x ) e. _V )
226 elpwg 
 |-  ( ( F " x ) e. _V -> ( ( F " x ) e. ~P A <-> ( F " x ) C_ A ) )
227 225 226 syl 
 |-  ( ph -> ( ( F " x ) e. ~P A <-> ( F " x ) C_ A ) )
228 168 227 mpbird 
 |-  ( ph -> ( F " x ) e. ~P A )
229 228 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ~P A )
230 25 ffund 
 |-  ( ph -> Fun F )
231 230 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> Fun F )
232 elinel2 
 |-  ( x e. ( ~P C i^i Fin ) -> x e. Fin )
233 232 adantl 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> x e. Fin )
234 imafi 
 |-  ( ( Fun F /\ x e. Fin ) -> ( F " x ) e. Fin )
235 231 233 234 syl2anc 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. Fin )
236 229 235 elind 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ( ~P A i^i Fin ) )
237 236 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ( ~P A i^i Fin ) )
238 nfv 
 |-  F/ k x e. ( ~P C i^i Fin )
239 95 238 nfan 
 |-  F/ k ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) )
240 nfv 
 |-  F/ n x e. ( ~P C i^i Fin )
241 103 240 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) )
242 232 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> x e. Fin )
243 108 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> F : C -1-1-> A )
244 f1ores 
 |-  ( ( F : C -1-1-> A /\ x C_ C ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
245 243 139 244 syl2anc 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
246 245 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
247 142 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = G )
248 239 241 3 242 246 247 214 fsumf1of 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> sum_ k e. ( F " x ) B = sum_ n e. x D )
249 248 eqcomd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> sum_ n e. x D = sum_ k e. ( F " x ) B )
250 sumeq1 
 |-  ( y = ( F " x ) -> sum_ k e. y B = sum_ k e. ( F " x ) B )
251 250 rspceeqv 
 |-  ( ( ( F " x ) e. ( ~P A i^i Fin ) /\ sum_ n e. x D = sum_ k e. ( F " x ) B ) -> E. y e. ( ~P A i^i Fin ) sum_ n e. x D = sum_ k e. y B )
252 237 249 251 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> E. y e. ( ~P A i^i Fin ) sum_ n e. x D = sum_ k e. y B )
253 224 252 rnmptssrn 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ran ( x e. ( ~P C i^i Fin ) |-> sum_ n e. x D ) C_ ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) )
254 222 253 eqssd 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) = ran ( x e. ( ~P C i^i Fin ) |-> sum_ n e. x D ) )
255 254 supeq1d 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) = sup ( ran ( x e. ( ~P C i^i Fin ) |-> sum_ n e. x D ) , RR* , < ) )
256 11 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> A e. _V )
257 95 256 212 sge0revalmpt 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( k e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) )
258 4 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> C e. V )
259 103 258 206 sge0revalmpt 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( n e. C |-> D ) ) = sup ( ran ( x e. ( ~P C i^i Fin ) |-> sum_ n e. x D ) , RR* , < ) )
260 255 257 259 3eqtr4d 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )
261 69 260 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )