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