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 bilani 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> E. x e. z k e. B )
123 simp1l 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> ph )
124 61 3adant3 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> x e. A )
125 simp3 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> k e. B )
126 123 124 125 4 syl3anc 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z /\ k e. B ) -> C e. ( 0 [,] +oo ) )
127 126 3exp 
 |-  ( ( ph /\ z C_ A ) -> ( x e. z -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
128 127 rexlimdv 
 |-  ( ( ph /\ z C_ A ) -> ( E. x e. z k e. B -> C e. ( 0 [,] +oo ) ) )
129 128 adantr 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> ( E. x e. z k e. B -> C e. ( 0 [,] +oo ) ) )
130 122 129 mpd 
 |-  ( ( ( ph /\ z C_ A ) /\ k e. U_ x e. z B ) -> C e. ( 0 [,] +oo ) )
131 130 adantlrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ k e. U_ x e. z B ) -> C e. ( 0 [,] +oo ) )
132 eliun 
 |-  ( k e. U_ x e. { w } B <-> E. x e. { w } k e. B )
133 132 bilani 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> E. x e. { w } k e. B )
134 simp1l 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> ph )
135 111 sselda 
 |-  ( ( w e. ( A \ z ) /\ x e. { w } ) -> x e. A )
136 135 adantll 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } ) -> x e. A )
137 136 3adant3 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> x e. A )
138 simp3 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> k e. B )
139 134 137 138 4 syl3anc 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ x e. { w } /\ k e. B ) -> C e. ( 0 [,] +oo ) )
140 139 3exp 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( x e. { w } -> ( k e. B -> C e. ( 0 [,] +oo ) ) ) )
141 140 rexlimdv 
 |-  ( ( ph /\ w e. ( A \ z ) ) -> ( E. x e. { w } k e. B -> C e. ( 0 [,] +oo ) ) )
142 141 adantr 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> ( E. x e. { w } k e. B -> C e. ( 0 [,] +oo ) ) )
143 133 142 mpd 
 |-  ( ( ( ph /\ w e. ( A \ z ) ) /\ k e. U_ x e. { w } B ) -> C e. ( 0 [,] +oo ) )
144 143 adantlrl 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ k e. U_ x e. { w } B ) -> C e. ( 0 [,] +oo ) )
145 100 108 116 120 131 144 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 ) ) ) )
146 99 145 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 ) ) ) )
147 146 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 ) ) ) )
148 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 ) ) ) ) )
149 148 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 ) ) ) ) )
150 4 3expa 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
151 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
152 150 151 fmptd 
 |-  ( ( ph /\ x e. A ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
153 2 152 sge0ge0 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( sum^ ` ( k e. B |-> C ) ) )
154 5 153 jca 
 |-  ( ( ph /\ x e. A ) -> ( ( sum^ ` ( k e. B |-> C ) ) e. RR /\ 0 <_ ( sum^ ` ( k e. B |-> C ) ) ) )
155 elrege0 
 |-  ( ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) <-> ( ( sum^ ` ( k e. B |-> C ) ) e. RR /\ 0 <_ ( sum^ ` ( k e. B |-> C ) ) ) )
156 154 155 sylibr 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
157 59 61 156 syl2anc 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
158 eqid 
 |-  ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) )
159 157 158 fmptd 
 |-  ( ( ph /\ z C_ A ) -> ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) : z --> ( 0 [,) +oo ) )
160 50 159 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 ) )
161 160 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 ) )
162 fveq2 
 |-  ( y = x -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y ) = ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) )
163 nfmpt1 
 |-  F/_ x ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) )
164 nfcv 
 |-  F/_ x y
165 163 164 nffv 
 |-  F/_ x ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` y )
166 nfcv 
 |-  F/_ y ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x )
167 162 165 166 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 )
168 167 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 ) )
169 id 
 |-  ( x e. z -> x e. z )
170 fvexd 
 |-  ( x e. z -> ( sum^ ` ( k e. B |-> C ) ) e. _V )
171 158 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 ) ) )
172 169 170 171 syl2anc 
 |-  ( x e. z -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
173 172 adantl 
 |-  ( ( ( ph /\ z C_ A ) /\ x e. z ) -> ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
174 173 ralrimiva 
 |-  ( ( ph /\ z C_ A ) -> A. x e. z ( ( x e. z |-> ( sum^ ` ( k e. B |-> C ) ) ) ` x ) = ( sum^ ` ( k e. B |-> C ) ) )
175 174 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 ) ) )
176 168 175 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 ) ) )
177 176 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 ) ) )
178 149 161 177 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 ) ) )
179 178 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 ) ) )
180 179 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 ) ) ) )
181 50 62 fsumrecl 
 |-  ( ( ph /\ z C_ A ) -> sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) e. RR )
182 181 adantrr 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> sum_ x e. z ( sum^ ` ( k e. B |-> C ) ) e. RR )
183 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 ) ) ) )
184 182 91 183 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 ) ) ) )
185 184 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 ) ) ) )
186 147 180 185 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 ) ) ) )
187 snfi 
 |-  { w } e. Fin
188 187 a1i 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> { w } e. Fin )
189 unfi 
 |-  ( ( z e. Fin /\ { w } e. Fin ) -> ( z u. { w } ) e. Fin )
190 51 188 189 syl2anc 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( z u. { w } ) e. Fin )
191 simpll 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> ph )
192 60 ad4ant14 
 |-  ( ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) /\ x e. z ) -> x e. A )
193 simpll 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> w e. ( A \ z ) )
194 elunnel1 
 |-  ( ( x e. ( z u. { w } ) /\ -. x e. z ) -> x e. { w } )
195 elsni 
 |-  ( x e. { w } -> x = w )
196 194 195 syl 
 |-  ( ( x e. ( z u. { w } ) /\ -. x e. z ) -> x = w )
197 196 adantll 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x = w )
198 simpr 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> x = w )
199 75 adantr 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> w e. A )
200 198 199 eqeltrd 
 |-  ( ( w e. ( A \ z ) /\ x = w ) -> x e. A )
201 193 197 200 syl2anc 
 |-  ( ( ( w e. ( A \ z ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x e. A )
202 201 adantlll 
 |-  ( ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) /\ -. x e. z ) -> x e. A )
203 192 202 pm2.61dan 
 |-  ( ( ( z C_ A /\ w e. ( A \ z ) ) /\ x e. ( z u. { w } ) ) -> x e. A )
204 203 adantll 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> x e. A )
205 191 204 156 syl2anc 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ x e. ( z u. { w } ) ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
206 190 205 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 ) ) )
207 206 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 ) ) )
208 95 186 207 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 ) ) ) ) )
209 208 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 ) ) ) ) ) )
210 11 17 23 29 39 209 1 findcard2d 
 |-  ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )