Metamath Proof Explorer

Theorem sge0iunmptlemfi

Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iunmptlemfi.a 
|- ( ph -> A e. Fin )
sge0iunmptlemfi.b 
|- ( ( ph /\ x e. A ) -> B e. V )
sge0iunmptlemfi.dj 
|- ( ph -> Disj_ x e. A B )
sge0iunmptlemfi.c 
|- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
sge0iunmptlemfi.re 
|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
Assertion sge0iunmptlemfi 
|- ( 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 sge0iunmptlemfi.a 
 |-  ( ph -> A e. Fin )
2 sge0iunmptlemfi.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 sge0iunmptlemfi.dj 
 |-  ( ph -> Disj_ x e. A B )
4 sge0iunmptlemfi.c 
 |-  ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
5 sge0iunmptlemfi.re 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
6 iuneq1 
 |-  ( y = (/) -> U_ x e. y B = U_ x e. (/) B )
7 6 mpteq1d 
 |-  ( y = (/) -> ( k e. U_ x e. y B |-> C ) = ( k e. U_ x e. (/) B |-> C ) )
8 7 fveq2d 
 |-  ( y = (/) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( k e. U_ x e. (/) B |-> C ) ) )
9 mpteq1 
 |-  ( y = (/) -> ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) )
10 9 fveq2d 
 |-  ( y = (/) -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
11 8 10 eqeq12d 
 |-  ( y = (/) -> ( ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <-> ( sum^ ` ( k e. U_ x e. (/) B |-> C ) ) = ( sum^ ` ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
12 iuneq1 
 |-  ( y = z -> U_ x e. y B = U_ x e. z B )
13 12 mpteq1d 
 |-  ( y = z -> ( k e. U_ x e. y B |-> C ) = ( k e. U_ x e. z B |-> C ) )
14 13 fveq2d 
 |-  ( y = z -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( k e. U_ x e. z B |-> C ) ) )
15 mpteq1 
 |-  ( y = z -> ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) )
16 15 fveq2d 
 |-  ( y = z -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
17 14 16 eqeq12d 
 |-  ( y = z -> ( ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <-> ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
18 iuneq1 
 |-  ( y = ( z u. { w } ) -> U_ x e. y B = U_ x e. ( z u. { w } ) B )
19 18 mpteq1d 
 |-  ( y = ( z u. { w } ) -> ( k e. U_ x e. y B |-> C ) = ( k e. U_ x e. ( z u. { w } ) B |-> C ) )
20 19 fveq2d 
 |-  ( y = ( z u. { w } ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) )
21 mpteq1 
 |-  ( y = ( z u. { w } ) -> ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) )
22 21 fveq2d 
 |-  ( y = ( z u. { w } ) -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
23 20 22 eqeq12d 
 |-  ( y = ( z u. { w } ) -> ( ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <-> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
24 iuneq1 
 |-  ( y = A -> U_ x e. y B = U_ x e. A B )
25 24 mpteq1d 
 |-  ( y = A -> ( k e. U_ x e. y B |-> C ) = ( k e. U_ x e. A B |-> C ) )
26 25 fveq2d 
 |-  ( y = A -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
27 mpteq1 
 |-  ( y = A -> ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) )
28 27 fveq2d 
 |-  ( y = A -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
29 26 28 eqeq12d 
 |-  ( y = A -> ( ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <-> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
30 0iun 
 |-  U_ x e. (/) B = (/)
31 mpteq1 
 |-  ( U_ x e. (/) B = (/) -> ( k e. U_ x e. (/) B |-> C ) = ( k e. (/) |-> C ) )
32 30 31 ax-mp 
 |-  ( k e. U_ x e. (/) B |-> C ) = ( k e. (/) |-> C )
33 mpt0 
 |-  ( k e. (/) |-> C ) = (/)
34 32 33 eqtri 
 |-  ( k e. U_ x e. (/) B |-> C ) = (/)
35 34 fveq2i 
 |-  ( sum^ ` ( k e. U_ x e. (/) B |-> C ) ) = ( sum^ ` (/) )
36 mpt0 
 |-  ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) = (/)
37 36 fveq2i 
 |-  ( sum^ ` ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` (/) )
38 35 37 eqtr4i 
 |-  ( sum^ ` ( k e. U_ x e. (/) B |-> C ) ) = ( sum^ ` ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) )
39 38 a1i 
 |-  ( ph -> ( sum^ ` ( k e. U_ x e. (/) B |-> C ) ) = ( sum^ ` ( x e. (/) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
40 nfv 
 |-  F/ x ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) )
41 nfcv 
 |-  F/_ x sum^
42 nfiu1 
 |-  F/_ x U_ x e. { w } B
43 nfcv 
 |-  F/_ x C
44 42 43 nfmpt 
 |-  F/_ x ( k e. U_ x e. { w } B |-> C )
45 41 44 nffv 
 |-  F/_ x ( sum^ ` ( k e. U_ x e. { w } B |-> C ) )
46 simprl 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> z C_ A )
47 1 adantr 
 |-  ( ( ph /\ z C_ A ) -> A e. Fin )
48 simpr 
 |-  ( ( ph /\ z C_ A ) -> z C_ A )
49 ssfi 
 |-  ( ( A e. Fin /\ z C_ A ) -> z e. Fin )
50 47 48 49 syl2anc 
 |-  ( ( ph /\ z C_ A ) -> z e. Fin )
51 46 50 syldan 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> z e. Fin )
52 simprr 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> w e. ( A \ z ) )
53 eldifn 
 |-  ( w e. ( A \ z ) -> -. w e. z )
54 disjsn 
 |-  ( ( z i^i { w } ) = (/) <-> -. w e. z )
55 53 54 sylibr 
 |-  ( w e. ( A \ z ) -> ( z i^i { w } ) = (/) )
56 55 adantl 
 |-  ( ( z C_ A /\ w e. ( A \ z ) ) -> ( z i^i { w } ) = (/) )
57 56 adantl 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( z i^i { w } ) = (/) )
58 57 54 sylib 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> -. w e. z )
59 simpll 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ph )
60 ssel2 
 |-  ( ( z C_ A /\ x e. z ) -> x e. A )
61 60 adantll 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> x e. A )
62 59 61 5 syl2anc 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
63 62 recnd 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( sum^ ` ( k e. B |-> C ) ) e. CC )
64 63 adantlrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. z ) -> ( sum^ ` ( k e. B |-> C ) ) e. CC )
65 csbeq1a 
 |-  ( x = w -> B = [_ w / x ]_ B )
66 nfcsb1v 
 |-  F/_ x [_ w / x ]_ B
67 vex 
 |-  w e. _V
68 66 67 65 iunxsnf 
 |-  U_ x e. { w } B = [_ w / x ]_ B
69 65 68 eqtr4di 
 |-  ( x = w -> B = U_ x e. { w } B )
70 69 mpteq1d 
 |-  ( x = w -> ( k e. B |-> C ) = ( k e. U_ x e. { w } B |-> C ) )
71 70 fveq2d 
 |-  ( x = w -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) )
72 68 mpteq1i 
 |-  ( k e. U_ x e. { w } B |-> C ) = ( k e. [_ w / x ]_ B |-> C )
73 72 a1i 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( k e. U_ x e. { w } B |-> C ) = ( k e. [_ w / x ]_ B |-> C ) )
74 73 fveq2d 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) = ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) )
75 eldifi 
 |-  ( w e. ( A \ z ) -> w e. A )
76 nfv 
 |-  F/ x ( ph /\ w e. A )
77 66 43 nfmpt 
 |-  F/_ x ( k e. [_ w / x ]_ B |-> C )
78 41 77 nffv 
 |-  F/_ x ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) )
79 nfcv 
 |-  F/_ x RR
80 78 79 nfel 
 |-  F/ x ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR
81 76 80 nfim 
 |-  F/ x ( ( ph /\ w e. A ) -> ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR )
82 eleq1w 
 |-  ( x = w -> ( x e. A <-> w e. A ) )
83 82 anbi2d 
 |-  ( x = w -> ( ( ph /\ x e. A ) <-> ( ph /\ w e. A ) ) )
84 70 72 eqtrdi 
 |-  ( x = w -> ( k e. B |-> C ) = ( k e. [_ w / x ]_ B |-> C ) )
85 84 fveq2d 
 |-  ( x = w -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) )
86 85 eleq1d 
 |-  ( x = w -> ( ( sum^ ` ( k e. B |-> C ) ) e. RR <-> ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR ) )
87 83 86 imbi12d 
 |-  ( x = w -> ( ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR ) <-> ( ( ph /\ w e. A ) -> ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR ) ) )
88 81 87 5 chvarfv 
 |-  ( ( ph /\ w e. A ) -> ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR )
89 75 88 sylan2 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( sum^ ` ( k e. [_ w / x ]_ B |-> C ) ) e. RR )
90 74 89 eqeltrd 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) e. RR )
91 90 adantrl 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) e. RR )
92 91 recnd 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) e. CC )
93 40 45 51 52 58 64 71 92 fsumsplitsn 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> sum_ x e. ( z u. { w } ) ( sum^ ` ( k e. B |-> C ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
94 93 eqcomd 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = sum_ x e. ( z u. { w } ) ( sum^ ` ( k e. B |-> C ) ) )
95 94 adantr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = sum_ x e. ( z u. { w } ) ( sum^ ` ( k e. B |-> C ) ) )
96 iunxun 
 |-  U_ x e. ( z u. { w } ) B = ( U_ x e. z B u. U_ x e. { w } B )
97 96 mpteq1i 
 |-  ( k e. U_ x e. ( z u. { w } ) B |-> C ) = ( k e. ( U_ x e. z B u. U_ x e. { w } B ) |-> C )
98 97 fveq2i 
 |-  ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum^ ` ( k e. ( U_ x e. z B u. U_ x e. { w } B ) |-> C ) )
99 98 a1i 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum^ ` ( k e. ( U_ x e. z B u. U_ x e. { w } B ) |-> C ) ) )
100 nfv 
 |-  F/ k ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) )
101 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. V )
102 iunexg 
 |-  ( ( A e. Fin /\ A. x e. A B e. V ) -> U_ x e. A B e. _V )
103 1 101 102 syl2anc 
 |-  ( ph -> U_ x e. A B e. _V )
104 103 adantr 
 |-  ( ( ph /\ z C_ A ) -> U_ x e. A B e. _V )
105 iunss1 
 |-  ( z C_ A -> U_ x e. z B C_ U_ x e. A B )
106 105 adantl 
 |-  ( ( ph /\ z C_ A ) -> U_ x e. z B C_ U_ x e. A B )
107 104 106 ssexd 
 |-  ( ( ph /\ z C_ A ) -> U_ x e. z B e. _V )
108 107 adantrr 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> U_ x e. z B e. _V )
109 103 adantr 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> U_ x e. A B e. _V )
110 snssi 
 |-  ( w e. A -> { w } C_ A )
111 75 110 syl 
 |-  ( w e. ( A \ z ) -> { w } C_ A )
112 iunss1 
 |-  ( { w } C_ A -> U_ x e. { w } B C_ U_ x e. A B )
113 111 112 syl 
 |-  ( w e. ( A \ z ) -> U_ x e. { w } B C_ U_ x e. A B )
114 113 adantl 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> U_ x e. { w } B C_ U_ x e. A B )
115 109 114 ssexd 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> U_ x e. { w } B e. _V )
116 115 adantrl 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> U_ x e. { w } B e. _V )
117 3 adantr 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> Disj_ x e. A B )
118 111 ad2antll 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> { w } C_ A )
119 disjiun 
 |-  ( ( Disj_ x e. A B /\ ( z C_ A /\ { w } C_ A /\ ( z i^i { w } ) = (/) ) ) -> ( U_ x e. z B i^i U_ x e. { w } B ) = (/) )
120 117 46 118 57 119 syl13anc 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( U_ x e. z B i^i U_ x e. { w } B ) = (/) )
121 eliun 
 |-  ( k e. U_ x e. z B <-> E. x e. z k e. B )
122 121 biimpi 
 |-  ( k e. U_ x e. z B -> E. x e. z k e. B )
123 122 adantl 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> E. x e. z k e. B )
124 simp1l 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> ph )
125 61 3adant3 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> x e. A )
126 simp3 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> k e. B )
127 124 125 126 4 syl3anc 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> C e. ( 0 [,] +oo ) )
128 127 3exp 
 |-  ( ( ph /\ z C_ A ) -> ( x e. z -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
129 128 rexlimdv 
 |-  ( ( ph /\ z C_ A ) -> ( E. x e. z k e. B -> C e. ( 0 [,] +oo ) ) )
130 129 adantr 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> ( E. x e. z k e. B -> C e. ( 0 [,] +oo ) ) )
131 123 130 mpd 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> C e. ( 0 [,] +oo ) )
132 131 adantlrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ k e. U_ x e. z B ) -> C e. ( 0 [,] +oo ) )
133 eliun 
 |-  ( k e. U_ x e. { w } B <-> E. x e. { w } k e. B )
134 133 biimpi 
 |-  ( k e. U_ x e. { w } B -> E. x e. { w } k e. B )
135 134 adantl 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> E. x e. { w } k e. B )
136 simp1l 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> ph )
137 111 sselda 
 |-  ( ( w e. ( A \ z ) /\ x e. { w } ) -> x e. A )
138 137 adantll 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } ) -> x e. A )
139 138 3adant3 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> x e. A )
140 simp3 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> k e. B )
141 136 139 140 4 syl3anc 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> C e. ( 0 [,] +oo ) )
142 141 3exp 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( x e. { w } -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
143 142 rexlimdv 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( E. x e. { w } k e. B -> C e. ( 0 [,] +oo ) ) )
144 143 adantr 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> ( E. x e. { w } k e. B -> C e. ( 0 [,] +oo ) ) )
145 135 144 mpd 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> C e. ( 0 [,] +oo ) )
146 145 adantlrl 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ k e. U_ x e. { w } B ) -> C e. ( 0 [,] +oo ) )
147 100 108 116 120 132 146 sge0splitmpt 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( k e. ( U_ x e. z B u. U_ x e. { w } B ) |-> C ) ) = ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
148 99 147 eqtrd 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
149 148 adantr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
150 id 
 |-  ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) -> ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
151 150 adantl 
 |-  ( ( ( ph /\ z C_ A ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
152 4 3expa 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
153 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
154 152 153 fmptd 
 |-  ( ( ph /\ x e. A ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
155 2 154 sge0ge0 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( sum^ ` ( k e. B |-> C ) ) )
156 5 155 jca 
 |-  ( ( ph /\ x e. A ) -> ( ( sum^ ` ( k e. B |-> C ) ) e. RR /\ 0 <_ ( sum^ ` ( k e. B |-> C ) ) ) )
157 elrege0 
 |-  ( ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) <-> ( ( sum^ ` ( k e. B |-> C ) ) e. RR /\ 0 <_ ( sum^ ` ( k e. B |-> C ) ) ) )
158 156 157 sylibr 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
159 59 61 158 syl2anc 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
160 eqid 
 |-  ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) )
161 159 160 fmptd 
 |-  ( ( ph /\ z C_ A ) -> ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) : z --> ( 0 [,) +oo ) )
162 50 161 sge0fsum 
 |-  ( ( ph /\ z C_ A ) -> ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) )
163 162 adantr 
 |-  ( ( ( ph /\ z C_ A ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) )
164 fveq2 
 |-  ( y = x -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) )
165 nfmpt1 
 |-  F/_ x ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) )
166 nfcv 
 |-  F/_ x y
167 165 166 nffv 
 |-  F/_ x ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y )
168 nfcv 
 |-  F/_ y ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x )
169 164 167 168 cbvsum 
 |-  sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = sum_ x e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x )
170 169 a1i 
 |-  ( ( ph /\ z C_ A ) -> sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = sum_ x e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) )
171 id 
 |-  ( x e. z -> x e. z )
172 fvexd 
 |-  ( x e. z -> ( sum^ ` ( k e. B |-> C ) ) e. _V )
173 160 fvmpt2 
 |-  ( ( x e. z /\ ( sum^ ` ( k e. B |-> C ) ) e. _V ) -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
174 171 172 173 syl2anc 
 |-  ( x e. z -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
175 174 adantl 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
176 175 ralrimiva 
 |-  ( ( ph /\ z C_ A ) -> A. x e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
177 176 sumeq2d 
 |-  ( ( ph /\ z C_ A ) -> sum_ x e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) )
178 170 177 eqtrd 
 |-  ( ( ph /\ z C_ A ) -> sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) )
179 178 adantr 
 |-  ( ( ( ph /\ z C_ A ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> sum_ y e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) )
180 151 163 179 3eqtrd 
 |-  ( ( ( ph /\ z C_ A ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) )
181 180 adantlrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) )
182 181 oveq1d 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
183 50 62 fsumrecl 
 |-  ( ( ph /\ z C_ A ) -> sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) e. RR )
184 183 adantrr 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) e. RR )
185 rexadd 
 |-  ( ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) e. RR /\ ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) e. RR ) -> ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
186 184 91 185 syl2anc 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
187 186 adantr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) +e ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
188 149 182 187 3eqtrd 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) + ( sum^ ` ( k e. U_ x e. { w } B |-> C ) ) ) )
189 snfi 
 |-  { w } e. Fin
190 189 a1i 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> { w } e. Fin )
191 unfi 
 |-  ( ( z e. Fin /\ { w } e. Fin ) -> ( z u. { w } ) e. Fin )
192 51 190 191 syl2anc 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( z u. { w } ) e. Fin )
193 simpll 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> ph )
194 60 ad4ant14 
 |-  ( ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) /\ x e. z ) -> x e. A )
195 simpll 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> w e. ( A \ z ) )
196 elunnel1 
 |-  ( ( x e. ( z u. { w } ) /\ -. x e. z ) -> x e. { w } )
197 elsni 
 |-  ( x e. { w } -> x = w )
198 196 197 syl 
 |-  ( ( x e. ( z u. { w } ) /\ -. x e. z ) -> x = w )
199 198 adantll 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x = w )
200 simpr 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> x = w )
201 75 adantr 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> w e. A )
202 200 201 eqeltrd 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> x e. A )
203 195 199 202 syl2anc 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x e. A )
204 203 adantlll 
 |-  ( ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x e. A )
205 194 204 pm2.61dan 
 |-  ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) -> x e. A )
206 205 adantll 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> x e. A )
207 193 206 158 syl2anc 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
208 192 207 sge0fsummpt 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = sum_ x e. ( z u. { w } ) ( sum^ ` ( k e. B |-> C ) ) )
209 208 adantr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = sum_ x e. ( z u. { w } ) ( sum^ ` ( k e. B |-> C ) ) )
210 95 188 209 3eqtr4d 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
211 210 ex 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( ( sum^ ` ( k e. U_ x e. z B |-> C ) ) = ( sum^ ` ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ) -> ( sum^ ` ( k e. U_ x e. ( z u. { w } ) B |-> C ) ) = ( sum^ ` ( x e. ( z u. { w } ) |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
212 11 17 23 29 39 211 1 findcard2d 
 |-  ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )