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