Metamath Proof Explorer

Theorem sge0iunmpt

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iunmpt.a 
|- ( ph -> A e. V )
sge0iunmpt.b 
|- ( ( ph /\ x e. A ) -> B e. W )
sge0iunmpt.dj 
|- ( ph -> Disj_ x e. A B )
sge0iunmpt.c 
|- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
Assertion sge0iunmpt 
|- ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iunmpt.a 
 |-  ( ph -> A e. V )
2 sge0iunmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 sge0iunmpt.dj 
 |-  ( ph -> Disj_ x e. A B )
4 sge0iunmpt.c 
 |-  ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
5 nfv 
 |-  F/ x ph
6 nfcv 
 |-  F/_ x sum^
7 nfiu1 
 |-  F/_ x U_ x e. A B
8 nfcv 
 |-  F/_ x C
9 7 8 nfmpt 
 |-  F/_ x ( k e. U_ x e. A B |-> C )
10 6 9 nffv 
 |-  F/_ x ( sum^ ` ( k e. U_ x e. A B |-> C ) )
11 nfmpt1 
 |-  F/_ x ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) )
12 6 11 nffv 
 |-  F/_ x ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
13 10 12 nfeq 
 |-  F/ x ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
14 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. W )
15 iunexg 
 |-  ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )
16 1 14 15 syl2anc 
 |-  ( ph -> U_ x e. A B e. _V )
17 eliun 
 |-  ( k e. U_ x e. A B <-> E. x e. A k e. B )
18 17 biimpi 
 |-  ( k e. U_ x e. A B -> E. x e. A k e. B )
19 18 adantl 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> E. x e. A k e. B )
20 nfcv 
 |-  F/_ x k
21 20 7 nfel 
 |-  F/ x k e. U_ x e. A B
22 5 21 nfan 
 |-  F/ x ( ph /\ k e. U_ x e. A B )
23 8 nfel1 
 |-  F/ x C e. ( 0 [,] +oo )
24 4 3exp 
 |-  ( ph -> ( x e. A -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
25 24 adantr 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> ( x e. A -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
26 22 23 25 rexlimd 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> ( E. x e. A k e. B -> C e. ( 0 [,] +oo ) ) )
27 19 26 mpd 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> C e. ( 0 [,] +oo ) )
28 eqid 
 |-  ( k e. U_ x e. A B |-> C ) = ( k e. U_ x e. A B |-> C )
29 27 28 fmptd 
 |-  ( ph -> ( k e. U_ x e. A B |-> C ) : U_ x e. A B --> ( 0 [,] +oo ) )
30 16 29 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) e. RR* )
31 30 3ad2ant1 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) e. RR* )
32 id 
 |-  ( ( sum^ ` ( k e. B |-> C ) ) = +oo -> ( sum^ ` ( k e. B |-> C ) ) = +oo )
33 32 eqcomd 
 |-  ( ( sum^ ` ( k e. B |-> C ) ) = +oo -> +oo = ( sum^ ` ( k e. B |-> C ) ) )
34 33 adantl 
 |-  ( ( x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> +oo = ( sum^ ` ( k e. B |-> C ) ) )
35 34 3adant1 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> +oo = ( sum^ ` ( k e. B |-> C ) ) )
36 16 adantr 
 |-  ( ( ph /\ x e. A ) -> U_ x e. A B e. _V )
37 27 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ k e. U_ x e. A B ) -> C e. ( 0 [,] +oo ) )
38 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
39 38 adantl 
 |-  ( ( ph /\ x e. A ) -> B C_ U_ x e. A B )
40 36 37 39 sge0lessmpt 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
41 40 3adant3 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. B |-> C ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
42 35 41 eqbrtrd 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> +oo <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
43 31 42 xrgepnfd 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = +oo )
44 1 3ad2ant1 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> A e. V )
45 nfv 
 |-  F/ x ( ph /\ y e. A )
46 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
47 nfcsb1v 
 |-  F/_ x [_ y / x ]_ W
48 46 47 nfel 
 |-  F/ x [_ y / x ]_ B e. [_ y / x ]_ W
49 45 48 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. [_ y / x ]_ W )
50 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
51 50 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
52 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
53 csbeq1a 
 |-  ( x = y -> W = [_ y / x ]_ W )
54 52 53 eleq12d 
 |-  ( x = y -> ( B e. W <-> [_ y / x ]_ B e. [_ y / x ]_ W ) )
55 51 54 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B e. W ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. [_ y / x ]_ W ) ) )
56 49 55 2 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. [_ y / x ]_ W )
57 56 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> [_ y / x ]_ B e. [_ y / x ]_ W )
58 46 8 nfmpt 
 |-  F/_ x ( k e. [_ y / x ]_ B |-> C )
59 nfcv 
 |-  F/_ x ( 0 [,] +oo )
60 58 46 59 nff 
 |-  F/ x ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo )
61 45 60 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) )
62 52 mpteq1d 
 |-  ( x = y -> ( k e. B |-> C ) = ( k e. [_ y / x ]_ B |-> C ) )
63 62 52 feq12d 
 |-  ( x = y -> ( ( k e. B |-> C ) : B --> ( 0 [,] +oo ) <-> ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) ) )
64 51 63 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) ) <-> ( ( ph /\ y e. A ) -> ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) ) ) )
65 24 imp31 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
66 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
67 65 66 fmptd 
 |-  ( ( ph /\ x e. A ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
68 61 64 67 chvarfv 
 |-  ( ( ph /\ y e. A ) -> ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) )
69 68 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( k e. [_ y / x ]_ B |-> C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) )
70 57 69 sge0cl 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( sum^ ` ( k e. [_ y / x ]_ B |-> C ) ) e. ( 0 [,] +oo ) )
71 nfcv 
 |-  F/_ y ( sum^ ` ( k e. B |-> C ) )
72 6 58 nffv 
 |-  F/_ x ( sum^ ` ( k e. [_ y / x ]_ B |-> C ) )
73 62 fveq2d 
 |-  ( x = y -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. [_ y / x ]_ B |-> C ) ) )
74 71 72 73 cbvmpt 
 |-  ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( y e. A |-> ( sum^ ` ( k e. [_ y / x ]_ B |-> C ) ) )
75 70 74 fmptd 
 |-  ( ( ph /\ x e. A ) -> ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) : A --> ( 0 [,] +oo ) )
76 75 3adant3 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) : A --> ( 0 [,] +oo ) )
77 id 
 |-  ( x e. A -> x e. A )
78 fvexd 
 |-  ( x e. A -> ( sum^ ` ( k e. B |-> C ) ) e. _V )
79 eqid 
 |-  ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) )
80 79 elrnmpt1 
 |-  ( ( x e. A /\ ( sum^ ` ( k e. B |-> C ) ) e. _V ) -> ( sum^ ` ( k e. B |-> C ) ) e. ran ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
81 77 78 80 syl2anc 
 |-  ( x e. A -> ( sum^ ` ( k e. B |-> C ) ) e. ran ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
82 81 adantr 
 |-  ( ( x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. B |-> C ) ) e. ran ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
83 34 82 eqeltrd 
 |-  ( ( x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> +oo e. ran ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
84 83 3adant1 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> +oo e. ran ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
85 44 76 84 sge0pnfval 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = +oo )
86 43 85 eqtr4d 
 |-  ( ( ph /\ x e. A /\ ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
87 86 3exp 
 |-  ( ph -> ( x e. A -> ( ( sum^ ` ( k e. B |-> C ) ) = +oo -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) ) )
88 5 13 87 rexlimd 
 |-  ( ph -> ( E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
89 88 imp 
 |-  ( ( ph /\ E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
90 simpl 
 |-  ( ( ph /\ -. E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ph )
91 ralnex 
 |-  ( A. x e. A -. ( sum^ ` ( k e. B |-> C ) ) = +oo <-> -. E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo )
92 df-ne 
 |-  ( ( sum^ ` ( k e. B |-> C ) ) =/= +oo <-> -. ( sum^ ` ( k e. B |-> C ) ) = +oo )
93 92 bicomi 
 |-  ( -. ( sum^ ` ( k e. B |-> C ) ) = +oo <-> ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
94 93 ralbii 
 |-  ( A. x e. A -. ( sum^ ` ( k e. B |-> C ) ) = +oo <-> A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
95 91 94 sylbb1 
 |-  ( -. E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo -> A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
96 95 adantl 
 |-  ( ( ph /\ -. E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
97 1 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> A e. V )
98 nfcv 
 |-  F/_ x W
99 46 98 nfel 
 |-  F/ x [_ y / x ]_ B e. W
100 45 99 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. W )
101 52 eleq1d 
 |-  ( x = y -> ( B e. W <-> [_ y / x ]_ B e. W ) )
102 51 101 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B e. W ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. W ) ) )
103 100 102 2 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. W )
104 103 adantlr 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A ) -> [_ y / x ]_ B e. W )
105 nfcv 
 |-  F/_ y B
106 105 46 52 cbvdisj 
 |-  ( Disj_ x e. A B <-> Disj_ y e. A [_ y / x ]_ B )
107 3 106 sylib 
 |-  ( ph -> Disj_ y e. A [_ y / x ]_ B )
108 107 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> Disj_ y e. A [_ y / x ]_ B )
109 nfv 
 |-  F/ k ( ph /\ y e. A /\ j e. [_ y / x ]_ B )
110 nfcsb1v 
 |-  F/_ k [_ j / k ]_ C
111 110 nfel1 
 |-  F/ k [_ j / k ]_ C e. ( 0 [,] +oo )
112 109 111 nfim 
 |-  F/ k ( ( ph /\ y e. A /\ j e. [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) )
113 eleq1w 
 |-  ( k = j -> ( k e. [_ y / x ]_ B <-> j e. [_ y / x ]_ B ) )
114 113 3anbi3d 
 |-  ( k = j -> ( ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) <-> ( ph /\ y e. A /\ j e. [_ y / x ]_ B ) ) )
115 csbeq1a 
 |-  ( k = j -> C = [_ j / k ]_ C )
116 115 eleq1d 
 |-  ( k = j -> ( C e. ( 0 [,] +oo ) <-> [_ j / k ]_ C e. ( 0 [,] +oo ) ) )
117 114 116 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) -> C e. ( 0 [,] +oo ) ) <-> ( ( ph /\ y e. A /\ j e. [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) ) ) )
118 nfv 
 |-  F/ x y e. A
119 20 46 nfel 
 |-  F/ x k e. [_ y / x ]_ B
120 5 118 119 nf3an 
 |-  F/ x ( ph /\ y e. A /\ k e. [_ y / x ]_ B )
121 120 23 nfim 
 |-  F/ x ( ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) -> C e. ( 0 [,] +oo ) )
122 52 eleq2d 
 |-  ( x = y -> ( k e. B <-> k e. [_ y / x ]_ B ) )
123 50 122 3anbi23d 
 |-  ( x = y -> ( ( ph /\ x e. A /\ k e. B ) <-> ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) ) )
124 123 imbi1d 
 |-  ( x = y -> ( ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) <-> ( ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) -> C e. ( 0 [,] +oo ) ) ) )
125 121 124 4 chvarfv 
 |-  ( ( ph /\ y e. A /\ k e. [_ y / x ]_ B ) -> C e. ( 0 [,] +oo ) )
126 112 117 125 chvarfv 
 |-  ( ( ph /\ y e. A /\ j e. [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) )
127 126 3adant1r 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A /\ j e. [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) )
128 simpr 
 |-  ( ( A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo /\ y e. A ) -> y e. A )
129 simpl 
 |-  ( ( A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo /\ y e. A ) -> A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
130 simpl 
 |-  ( ( y e. A /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> y e. A )
131 simpr 
 |-  ( ( y e. A /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo )
132 nfcv 
 |-  F/_ x [_ j / k ]_ C
133 46 132 nfmpt 
 |-  F/_ x ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C )
134 6 133 nffv 
 |-  F/_ x ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) )
135 nfcv 
 |-  F/_ x +oo
136 134 135 nfne 
 |-  F/ x ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) =/= +oo
137 nfcv 
 |-  F/_ j C
138 137 110 115 cbvmpt 
 |-  ( k e. [_ y / x ]_ B |-> C ) = ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C )
139 138 a1i 
 |-  ( x = y -> ( k e. [_ y / x ]_ B |-> C ) = ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) )
140 62 139 eqtrd 
 |-  ( x = y -> ( k e. B |-> C ) = ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) )
141 140 fveq2d 
 |-  ( x = y -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) )
142 141 neeq1d 
 |-  ( x = y -> ( ( sum^ ` ( k e. B |-> C ) ) =/= +oo <-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) =/= +oo ) )
143 136 142 rspc 
 |-  ( y e. A -> ( A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo -> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) =/= +oo ) )
144 130 131 143 sylc 
 |-  ( ( y e. A /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) =/= +oo )
145 128 129 144 syl2anc 
 |-  ( ( A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo /\ y e. A ) -> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) =/= +oo )
146 145 neneqd 
 |-  ( ( A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo /\ y e. A ) -> -. ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) = +oo )
147 146 adantll 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A ) -> -. ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) = +oo )
148 126 3expa 
 |-  ( ( ( ph /\ y e. A ) /\ j e. [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) )
149 eqid 
 |-  ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) = ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C )
150 148 149 fmptd 
 |-  ( ( ph /\ y e. A ) -> ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) )
151 150 adantlr 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A ) -> ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) : [_ y / x ]_ B --> ( 0 [,] +oo ) )
152 104 151 sge0repnf 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A ) -> ( ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) e. RR <-> -. ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) = +oo ) )
153 147 152 mpbird 
 |-  ( ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) /\ y e. A ) -> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) e. RR )
154 137 110 115 cbvmpt 
 |-  ( k e. U_ x e. A B |-> C ) = ( j e. U_ x e. A B |-> [_ j / k ]_ C )
155 105 46 52 cbviun 
 |-  U_ x e. A B = U_ y e. A [_ y / x ]_ B
156 155 mpteq1i 
 |-  ( j e. U_ x e. A B |-> [_ j / k ]_ C ) = ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C )
157 154 156 eqtri 
 |-  ( k e. U_ x e. A B |-> C ) = ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C )
158 157 fveq2i 
 |-  ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) )
159 158 30 eqeltrrid 
 |-  ( ph -> ( sum^ ` ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) ) e. RR* )
160 159 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) ) e. RR* )
161 71 134 141 cbvmpt 
 |-  ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) )
162 161 fveq2i 
 |-  ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) ) )
163 2 67 sge0cl 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,] +oo ) )
164 163 79 fmptd 
 |-  ( ph -> ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) : A --> ( 0 [,] +oo ) )
165 1 164 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) e. RR* )
166 162 165 eqeltrrid 
 |-  ( ph -> ( sum^ ` ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) ) ) e. RR* )
167 166 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) ) ) e. RR* )
168 eliun 
 |-  ( j e. U_ y e. A [_ y / x ]_ B <-> E. y e. A j e. [_ y / x ]_ B )
169 168 biimpi 
 |-  ( j e. U_ y e. A [_ y / x ]_ B -> E. y e. A j e. [_ y / x ]_ B )
170 169 adantl 
 |-  ( ( ph /\ j e. U_ y e. A [_ y / x ]_ B ) -> E. y e. A j e. [_ y / x ]_ B )
171 nfv 
 |-  F/ y ph
172 nfcv 
 |-  F/_ y j
173 nfiu1 
 |-  F/_ y U_ y e. A [_ y / x ]_ B
174 172 173 nfel 
 |-  F/ y j e. U_ y e. A [_ y / x ]_ B
175 171 174 nfan 
 |-  F/ y ( ph /\ j e. U_ y e. A [_ y / x ]_ B )
176 nfv 
 |-  F/ y [_ j / k ]_ C e. ( 0 [,] +oo )
177 148 exp31 
 |-  ( ph -> ( y e. A -> ( j e. [_ y / x ]_ B -> [_ j / k ]_ C e. ( 0 [,] +oo ) ) ) )
178 177 adantr 
 |-  ( ( ph /\ j e. U_ y e. A [_ y / x ]_ B ) -> ( y e. A -> ( j e. [_ y / x ]_ B -> [_ j / k ]_ C e. ( 0 [,] +oo ) ) ) )
179 175 176 178 rexlimd 
 |-  ( ( ph /\ j e. U_ y e. A [_ y / x ]_ B ) -> ( E. y e. A j e. [_ y / x ]_ B -> [_ j / k ]_ C e. ( 0 [,] +oo ) ) )
180 170 179 mpd 
 |-  ( ( ph /\ j e. U_ y e. A [_ y / x ]_ B ) -> [_ j / k ]_ C e. ( 0 [,] +oo ) )
181 eqid 
 |-  ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) = ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C )
182 180 181 fmptd 
 |-  ( ph -> ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) : U_ y e. A [_ y / x ]_ B --> ( 0 [,] +oo ) )
183 182 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) : U_ y e. A [_ y / x ]_ B --> ( 0 [,] +oo ) )
184 155 16 eqeltrrid 
 |-  ( ph -> U_ y e. A [_ y / x ]_ B e. _V )
185 184 adantr 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> U_ y e. A [_ y / x ]_ B e. _V )
186 97 104 108 127 153 160 167 183 185 sge0iunmptlemre 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) ) = ( sum^ ` ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) ) ) )
187 158 a1i 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( j e. U_ y e. A [_ y / x ]_ B |-> [_ j / k ]_ C ) ) )
188 162 a1i 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( y e. A |-> ( sum^ ` ( j e. [_ y / x ]_ B |-> [_ j / k ]_ C ) ) ) ) )
189 186 187 188 3eqtr4d 
 |-  ( ( ph /\ A. x e. A ( sum^ ` ( k e. B |-> C ) ) =/= +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
190 90 96 189 syl2anc 
 |-  ( ( ph /\ -. E. x e. A ( sum^ ` ( k e. B |-> C ) ) = +oo ) -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
191 89 190 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )