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 fex 
 |-  ( ( F : C --> A /\ C e. V ) -> F e. _V )
75 25 4 74 syl2anc 
 |-  ( ph -> F e. _V )
76 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
77 75 76 syl 
 |-  ( ph -> `' F e. _V )
78 imaexg 
 |-  ( `' F e. _V -> ( `' F " y ) e. _V )
79 77 78 syl 
 |-  ( ph -> ( `' F " y ) e. _V )
80 elpwg 
 |-  ( ( `' F " y ) e. _V -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
81 79 80 syl 
 |-  ( ph -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
82 73 81 mpbird 
 |-  ( ph -> ( `' F " y ) e. ~P C )
83 82 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ~P C )
84 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
85 5 84 syl 
 |-  ( ph -> `' F : A -1-1-onto-> C )
86 f1ofun 
 |-  ( `' F : A -1-1-onto-> C -> Fun `' F )
87 85 86 syl 
 |-  ( ph -> Fun `' F )
88 87 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> Fun `' F )
89 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
90 89 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
91 imafi 
 |-  ( ( Fun `' F /\ y e. Fin ) -> ( `' F " y ) e. Fin )
92 88 90 91 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. Fin )
93 83 92 elind 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
94 93 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
95 nfv 
 |-  F/ k -. +oo e. ran ( n e. C |-> D )
96 1 95 nfan 
 |-  F/ k ( ph /\ -. +oo e. ran ( n e. C |-> D ) )
97 nfv 
 |-  F/ k y e. ( ~P A i^i Fin )
98 96 97 nfan 
 |-  F/ k ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) )
99 nfcv 
 |-  F/_ n +oo
100 nfmpt1 
 |-  F/_ n ( n e. C |-> D )
101 100 nfrn 
 |-  F/_ n ran ( n e. C |-> D )
102 99 101 nfel 
 |-  F/ n +oo e. ran ( n e. C |-> D )
103 102 nfn 
 |-  F/ n -. +oo e. ran ( n e. C |-> D )
104 2 103 nfan 
 |-  F/ n ( ph /\ -. +oo e. ran ( n e. C |-> D ) )
105 nfv 
 |-  F/ n y e. ( ~P A i^i Fin )
106 104 105 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) )
107 92 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) e. Fin )
108 f1of1 
 |-  ( F : C -1-1-onto-> A -> F : C -1-1-> A )
109 5 108 syl 
 |-  ( ph -> F : C -1-1-> A )
110 109 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> F : C -1-1-> A )
111 81 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( `' F " y ) e. ~P C <-> ( `' F " y ) C_ C ) )
112 83 111 mpbid 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( `' F " y ) C_ C )
113 f1ores 
 |-  ( ( F : C -1-1-> A /\ ( `' F " y ) C_ C ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> ( F " ( `' F " y ) ) )
114 110 112 113 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> ( F " ( `' F " y ) ) )
115 9 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> F : C -onto-> A )
116 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
117 116 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
118 foimacnv 
 |-  ( ( F : C -onto-> A /\ y C_ A ) -> ( F " ( `' F " y ) ) = y )
119 115 117 118 syl2anc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F " ( `' F " y ) ) = y )
120 119 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 ) )
121 114 120 mpbid 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( F |` ( `' F " y ) ) : ( `' F " y ) -1-1-onto-> y )
122 121 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 )
123 79 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( `' F " y ) e. _V )
124 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ph )
125 93 adantr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( `' F " y ) e. ( ~P C i^i Fin ) )
126 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> n e. ( `' F " y ) )
127 124 125 126 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 ) ) )
128 eleq1 
 |-  ( x = ( `' F " y ) -> ( x e. ( ~P C i^i Fin ) <-> ( `' F " y ) e. ( ~P C i^i Fin ) ) )
129 128 anbi2d 
 |-  ( x = ( `' F " y ) -> ( ( ph /\ x e. ( ~P C i^i Fin ) ) <-> ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) ) )
130 eleq2 
 |-  ( x = ( `' F " y ) -> ( n e. x <-> n e. ( `' F " y ) ) )
131 129 130 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 ) ) ) )
132 reseq2 
 |-  ( x = ( `' F " y ) -> ( F |` x ) = ( F |` ( `' F " y ) ) )
133 132 fveq1d 
 |-  ( x = ( `' F " y ) -> ( ( F |` x ) ` n ) = ( ( F |` ( `' F " y ) ) ` n ) )
134 133 eqeq1d 
 |-  ( x = ( `' F " y ) -> ( ( ( F |` x ) ` n ) = G <-> ( ( F |` ( `' F " y ) ) ` n ) = G ) )
135 131 134 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 ) ) )
136 fvres 
 |-  ( n e. x -> ( ( F |` x ) ` n ) = ( F ` n ) )
137 136 adantl 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = ( F ` n ) )
138 simpll 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ph )
139 elpwinss 
 |-  ( x e. ( ~P C i^i Fin ) -> x C_ C )
140 139 adantl 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> x C_ C )
141 140 sselda 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> n e. C )
142 138 141 6 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( F ` n ) = G )
143 137 142 eqtrd 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = G )
144 135 143 vtoclg 
 |-  ( ( `' F " y ) e. _V -> ( ( ( ph /\ ( `' F " y ) e. ( ~P C i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G ) )
145 123 127 144 sylc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ n e. ( `' F " y ) ) -> ( ( F |` ( `' F " y ) ) ` n ) = G )
146 145 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 )
147 79 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. _V )
148 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 ) ) )
149 82 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. ~P C )
150 107 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( `' F " y ) e. Fin )
151 149 150 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 ) )
152 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. y )
153 119 eqcomd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y = ( F " ( `' F " y ) ) )
154 153 adantr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> y = ( F " ( `' F " y ) ) )
155 152 154 eleqtrd 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. ( F " ( `' F " y ) ) )
156 155 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. ( F " ( `' F " y ) ) )
157 148 151 156 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 ) ) ) )
158 128 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 ) ) ) )
159 imaeq2 
 |-  ( x = ( `' F " y ) -> ( F " x ) = ( F " ( `' F " y ) ) )
160 159 eleq2d 
 |-  ( x = ( `' F " y ) -> ( k e. ( F " x ) <-> k e. ( F " ( `' F " y ) ) ) )
161 158 160 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 ) ) ) ) )
162 161 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 ) ) )
163 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
164 ax-resscn 
 |-  RR C_ CC
165 163 164 sstri 
 |-  ( 0 [,) +oo ) C_ CC
166 simplll 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> ph )
167 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 ) )
168 fimass 
 |-  ( F : C --> A -> ( F " x ) C_ A )
169 25 168 syl 
 |-  ( ph -> ( F " x ) C_ A )
170 169 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> ( F " x ) C_ A )
171 simpr 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. ( F " x ) )
172 170 171 sseldd 
 |-  ( ( ( ph /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. A )
173 172 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> k e. A )
174 foelrni 
 |-  ( ( F : C -onto-> A /\ k e. A ) -> E. n e. C ( F ` n ) = k )
175 9 174 sylan 
 |-  ( ( ph /\ k e. A ) -> E. n e. C ( F ` n ) = k )
176 175 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> E. n e. C ( F ` n ) = k )
177 nfv 
 |-  F/ n k e. A
178 104 177 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A )
179 nfv 
 |-  F/ n B e. ( 0 [,) +oo )
180 csbid 
 |-  [_ k / k ]_ B = B
181 180 eqcomi 
 |-  B = [_ k / k ]_ B
182 181 a1i 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> B = [_ k / k ]_ B )
183 id 
 |-  ( ( F ` n ) = k -> ( F ` n ) = k )
184 183 eqcomd 
 |-  ( ( F ` n ) = k -> k = ( F ` n ) )
185 184 csbeq1d 
 |-  ( ( F ` n ) = k -> [_ k / k ]_ B = [_ ( F ` n ) / k ]_ B )
186 185 3ad2ant3 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> [_ k / k ]_ B = [_ ( F ` n ) / k ]_ B )
187 38 idi 
 |-  ( ( ph /\ n e. C ) -> [_ ( F ` n ) / k ]_ B = D )
188 187 3adant3 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> [_ ( F ` n ) / k ]_ B = D )
189 182 186 188 3eqtrd 
 |-  ( ( ph /\ n e. C /\ ( F ` n ) = k ) -> B = D )
190 189 3adant1r 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> B = D )
191 0xr 
 |-  0 e. RR*
192 191 a1i 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> 0 e. RR* )
193 pnfxr 
 |-  +oo e. RR*
194 193 a1i 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. RR* )
195 64 adantr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D e. ( 0 [,] +oo ) )
196 simpr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> -. D e. ( 0 [,) +oo ) )
197 192 194 195 196 eliccnelico 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D = +oo )
198 197 eqcomd 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo = D )
199 simpr 
 |-  ( ( ph /\ n e. C ) -> n e. C )
200 64 idi 
 |-  ( ( ph /\ n e. C ) -> D e. ( 0 [,] +oo ) )
201 17 elrnmpt1 
 |-  ( ( n e. C /\ D e. ( 0 [,] +oo ) ) -> D e. ran ( n e. C |-> D ) )
202 199 200 201 syl2anc 
 |-  ( ( ph /\ n e. C ) -> D e. ran ( n e. C |-> D ) )
203 202 adantr 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> D e. ran ( n e. C |-> D ) )
204 198 203 eqeltrd 
 |-  ( ( ( ph /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. ran ( n e. C |-> D ) )
205 204 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> +oo e. ran ( n e. C |-> D ) )
206 simpllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) /\ -. D e. ( 0 [,) +oo ) ) -> -. +oo e. ran ( n e. C |-> D ) )
207 205 206 condan 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C ) -> D e. ( 0 [,) +oo ) )
208 207 3adant3 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> D e. ( 0 [,) +oo ) )
209 190 208 eqeltrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ n e. C /\ ( F ` n ) = k ) -> B e. ( 0 [,) +oo ) )
210 209 3exp 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( n e. C -> ( ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) ) )
211 210 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> ( n e. C -> ( ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) ) )
212 178 179 211 rexlimd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> ( E. n e. C ( F ` n ) = k -> B e. ( 0 [,) +oo ) ) )
213 176 212 mpd 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ k e. A ) -> B e. ( 0 [,) +oo ) )
214 166 167 173 213 syl21anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. ( 0 [,) +oo ) )
215 165 214 sseldi 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. CC )
216 215 idi 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ k e. ( F " x ) ) -> B e. CC )
217 162 216 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 ) )
218 147 157 217 sylc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> B e. CC )
219 98 106 3 107 122 146 218 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 )
220 sumeq1 
 |-  ( x = ( `' F " y ) -> sum_ n e. x D = sum_ n e. ( `' F " y ) D )
221 220 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 )
222 94 219 221 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 )
223 71 222 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 ) )
224 sumex 
 |-  sum_ n e. x D e. _V
225 224 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> sum_ n e. x D e. _V )
226 11 169 ssexd 
 |-  ( ph -> ( F " x ) e. _V )
227 elpwg 
 |-  ( ( F " x ) e. _V -> ( ( F " x ) e. ~P A <-> ( F " x ) C_ A ) )
228 226 227 syl 
 |-  ( ph -> ( ( F " x ) e. ~P A <-> ( F " x ) C_ A ) )
229 169 228 mpbird 
 |-  ( ph -> ( F " x ) e. ~P A )
230 229 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ~P A )
231 25 ffund 
 |-  ( ph -> Fun F )
232 231 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> Fun F )
233 elinel2 
 |-  ( x e. ( ~P C i^i Fin ) -> x e. Fin )
234 233 adantl 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> x e. Fin )
235 imafi 
 |-  ( ( Fun F /\ x e. Fin ) -> ( F " x ) e. Fin )
236 232 234 235 syl2anc 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. Fin )
237 230 236 elind 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ( ~P A i^i Fin ) )
238 237 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> ( F " x ) e. ( ~P A i^i Fin ) )
239 nfv 
 |-  F/ k x e. ( ~P C i^i Fin )
240 96 239 nfan 
 |-  F/ k ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) )
241 nfv 
 |-  F/ n x e. ( ~P C i^i Fin )
242 104 241 nfan 
 |-  F/ n ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) )
243 233 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> x e. Fin )
244 109 adantr 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> F : C -1-1-> A )
245 f1ores 
 |-  ( ( F : C -1-1-> A /\ x C_ C ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
246 244 140 245 syl2anc 
 |-  ( ( ph /\ x e. ( ~P C i^i Fin ) ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
247 246 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) -> ( F |` x ) : x -1-1-onto-> ( F " x ) )
248 143 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) /\ x e. ( ~P C i^i Fin ) ) /\ n e. x ) -> ( ( F |` x ) ` n ) = G )
249 240 242 3 243 247 248 215 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 )
250 249 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 )
251 sumeq1 
 |-  ( y = ( F " x ) -> sum_ k e. y B = sum_ k e. ( F " x ) B )
252 251 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 )
253 238 250 252 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 )
254 225 253 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 ) )
255 223 254 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 ) )
256 255 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* , < ) )
257 11 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> A e. _V )
258 96 257 213 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* , < ) )
259 4 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> C e. V )
260 104 259 207 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* , < ) )
261 256 258 260 3eqtr4d 
 |-  ( ( ph /\ -. +oo e. ran ( n e. C |-> D ) ) -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )
262 69 261 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )