Metamath Proof Explorer

Theorem esum2dlem

Description: Lemma for esum2d (finite case). (Contributed by Thierry Arnoux, 17-May-2020) (Proof shortened by AV, 17-Sep-2021)

Ref Expression
Hypotheses esum2d.0 
|- F/_ k F
esum2d.1 
|- ( z = <. j , k >. -> F = C )
esum2d.2 
|- ( ph -> A e. V )
esum2d.3 
|- ( ( ph /\ j e. A ) -> B e. W )
esum2d.4 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
esum2dlem.e 
|- ( ph -> A e. Fin )
Assertion esum2dlem 
|- ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F )

Proof

Step Hyp Ref Expression
1 esum2d.0 
 |-  F/_ k F
2 esum2d.1 
 |-  ( z = <. j , k >. -> F = C )
3 esum2d.2 
 |-  ( ph -> A e. V )
4 esum2d.3 
 |-  ( ( ph /\ j e. A ) -> B e. W )
5 esum2d.4 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
6 esum2dlem.e 
 |-  ( ph -> A e. Fin )
7 esumeq1 
 |-  ( a = (/) -> sum* j e. a sum* k e. B C = sum* j e. (/) sum* k e. B C )
8 nfv 
 |-  F/ z a = (/)
9 iuneq1 
 |-  ( a = (/) -> U_ j e. a ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
10 8 9 esumeq1d 
 |-  ( a = (/) -> sum* z e. U_ j e. a ( { j } X. B ) F = sum* z e. U_ j e. (/) ( { j } X. B ) F )
11 7 10 eqeq12d 
 |-  ( a = (/) -> ( sum* j e. a sum* k e. B C = sum* z e. U_ j e. a ( { j } X. B ) F <-> sum* j e. (/) sum* k e. B C = sum* z e. U_ j e. (/) ( { j } X. B ) F ) )
12 esumeq1 
 |-  ( a = b -> sum* j e. a sum* k e. B C = sum* j e. b sum* k e. B C )
13 nfv 
 |-  F/ z a = b
14 iuneq1 
 |-  ( a = b -> U_ j e. a ( { j } X. B ) = U_ j e. b ( { j } X. B ) )
15 13 14 esumeq1d 
 |-  ( a = b -> sum* z e. U_ j e. a ( { j } X. B ) F = sum* z e. U_ j e. b ( { j } X. B ) F )
16 12 15 eqeq12d 
 |-  ( a = b -> ( sum* j e. a sum* k e. B C = sum* z e. U_ j e. a ( { j } X. B ) F <-> sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) )
17 esumeq1 
 |-  ( a = ( b u. { l } ) -> sum* j e. a sum* k e. B C = sum* j e. ( b u. { l } ) sum* k e. B C )
18 nfv 
 |-  F/ z a = ( b u. { l } )
19 iuneq1 
 |-  ( a = ( b u. { l } ) -> U_ j e. a ( { j } X. B ) = U_ j e. ( b u. { l } ) ( { j } X. B ) )
20 18 19 esumeq1d 
 |-  ( a = ( b u. { l } ) -> sum* z e. U_ j e. a ( { j } X. B ) F = sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F )
21 17 20 eqeq12d 
 |-  ( a = ( b u. { l } ) -> ( sum* j e. a sum* k e. B C = sum* z e. U_ j e. a ( { j } X. B ) F <-> sum* j e. ( b u. { l } ) sum* k e. B C = sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F ) )
22 esumeq1 
 |-  ( a = A -> sum* j e. a sum* k e. B C = sum* j e. A sum* k e. B C )
23 nfv 
 |-  F/ z a = A
24 iuneq1 
 |-  ( a = A -> U_ j e. a ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
25 23 24 esumeq1d 
 |-  ( a = A -> sum* z e. U_ j e. a ( { j } X. B ) F = sum* z e. U_ j e. A ( { j } X. B ) F )
26 22 25 eqeq12d 
 |-  ( a = A -> ( sum* j e. a sum* k e. B C = sum* z e. U_ j e. a ( { j } X. B ) F <-> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F ) )
27 esumnul 
 |-  sum* z e. (/) F = 0
28 0iun 
 |-  U_ j e. (/) ( { j } X. B ) = (/)
29 esumeq1 
 |-  ( U_ j e. (/) ( { j } X. B ) = (/) -> sum* z e. U_ j e. (/) ( { j } X. B ) F = sum* z e. (/) F )
30 28 29 ax-mp 
 |-  sum* z e. U_ j e. (/) ( { j } X. B ) F = sum* z e. (/) F
31 esumnul 
 |-  sum* j e. (/) sum* k e. B C = 0
32 27 30 31 3eqtr4ri 
 |-  sum* j e. (/) sum* k e. B C = sum* z e. U_ j e. (/) ( { j } X. B ) F
33 32 a1i 
 |-  ( ph -> sum* j e. (/) sum* k e. B C = sum* z e. U_ j e. (/) ( { j } X. B ) F )
34 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F )
35 nfcsb1v 
 |-  F/_ j [_ l / j ]_ B
36 nfcsb1v 
 |-  F/_ j [_ l / j ]_ C
37 35 36 nfesum2 
 |-  F/_ j sum* k e. [_ l / j ]_ B [_ l / j ]_ C
38 csbeq1a 
 |-  ( j = l -> B = [_ l / j ]_ B )
39 csbeq1a 
 |-  ( j = l -> C = [_ l / j ]_ C )
40 38 39 esumeq12d 
 |-  ( j = l -> sum* k e. B C = sum* k e. [_ l / j ]_ B [_ l / j ]_ C )
41 40 adantl 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j = l ) -> sum* k e. B C = sum* k e. [_ l / j ]_ B [_ l / j ]_ C )
42 simprr 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. ( A \ b ) )
43 42 eldifad 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. A )
44 4 adantlr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. A ) -> B e. W )
45 44 ralrimiva 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. A B e. W )
46 rspcsbela 
 |-  ( ( l e. A /\ A. j e. A B e. W ) -> [_ l / j ]_ B e. W )
47 43 45 46 syl2anc 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> [_ l / j ]_ B e. W )
48 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ph )
49 43 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. A )
50 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> k e. [_ l / j ]_ B )
51 5 ex 
 |-  ( ph -> ( ( j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) )
52 51 sbcimdv 
 |-  ( ph -> ( [. l / j ]. ( j e. A /\ k e. B ) -> [. l / j ]. C e. ( 0 [,] +oo ) ) )
53 sbcan 
 |-  ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) )
54 sbcel1v 
 |-  ( [. l / j ]. j e. A <-> l e. A )
55 sbcel2 
 |-  ( [. l / j ]. k e. B <-> k e. [_ l / j ]_ B )
56 54 55 anbi12i 
 |-  ( ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
57 53 56 bitri 
 |-  ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
58 vex 
 |-  l e. _V
59 sbcel1g 
 |-  ( l e. _V -> ( [. l / j ]. C e. ( 0 [,] +oo ) <-> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
60 58 59 ax-mp 
 |-  ( [. l / j ]. C e. ( 0 [,] +oo ) <-> [_ l / j ]_ C e. ( 0 [,] +oo ) )
61 52 57 60 3imtr3g 
 |-  ( ph -> ( ( l e. A /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
62 61 imp 
 |-  ( ( ph /\ ( l e. A /\ k e. [_ l / j ]_ B ) ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
63 48 49 50 62 syl12anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
64 63 ralrimiva 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
65 nfcv 
 |-  F/_ k [_ l / j ]_ B
66 65 esumcl 
 |-  ( ( [_ l / j ]_ B e. W /\ A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) ) -> sum* k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
67 47 64 66 syl2anc 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
68 37 41 42 67 esumsnf 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* j e. { l } sum* k e. B C = sum* k e. [_ l / j ]_ B [_ l / j ]_ C )
69 nfv 
 |-  F/ k ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
70 nfv 
 |-  F/ j z = <. l , k >.
71 36 nfeq2 
 |-  F/ j F = [_ l / j ]_ C
72 70 71 nfim 
 |-  F/ j ( z = <. l , k >. -> F = [_ l / j ]_ C )
73 opeq1 
 |-  ( j = l -> <. j , k >. = <. l , k >. )
74 73 eqeq2d 
 |-  ( j = l -> ( z = <. j , k >. <-> z = <. l , k >. ) )
75 39 eqeq2d 
 |-  ( j = l -> ( F = C <-> F = [_ l / j ]_ C ) )
76 74 75 imbi12d 
 |-  ( j = l -> ( ( z = <. j , k >. -> F = C ) <-> ( z = <. l , k >. -> F = [_ l / j ]_ C ) ) )
77 72 76 2 chvarfv 
 |-  ( z = <. l , k >. -> F = [_ l / j ]_ C )
78 vsnid 
 |-  j e. { j }
79 78 a1i 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> j e. { j } )
80 simpr 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> k e. B )
81 79 80 opelxpd 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> <. j , k >. e. ( { j } X. B ) )
82 xp2nd 
 |-  ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
83 xp1st 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
84 fvex 
 |-  ( 1st ` z ) e. _V
85 84 elsn 
 |-  ( ( 1st ` z ) e. { j } <-> ( 1st ` z ) = j )
86 83 85 sylib 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
87 eqop 
 |-  ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
88 86 87 mpbirand 
 |-  ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( 2nd ` z ) = k ) )
89 eqcom 
 |-  ( ( 2nd ` z ) = k <-> k = ( 2nd ` z ) )
90 88 89 bitrdi 
 |-  ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
91 90 ad2antlr 
 |-  ( ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
92 91 ralrimiva 
 |-  ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
93 reu6i 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) ) -> E! k e. B z = <. j , k >. )
94 82 92 93 syl2an2 
 |-  ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E! k e. B z = <. j , k >. )
95 81 94 f1mptrn 
 |-  ( ( ph /\ j e. A ) -> Fun `' ( k e. B |-> <. j , k >. ) )
96 95 ex 
 |-  ( ph -> ( j e. A -> Fun `' ( k e. B |-> <. j , k >. ) ) )
97 96 sbcimdv 
 |-  ( ph -> ( [. l / j ]. j e. A -> [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) ) )
98 sbcfung 
 |-  ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) ) )
99 csbcnv 
 |-  `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = [_ l / j ]_ `' ( k e. B |-> <. j , k >. )
100 csbmpt12 
 |-  ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) )
101 csbopg 
 |-  ( l e. _V -> [_ l / j ]_ <. j , k >. = <. [_ l / j ]_ j , [_ l / j ]_ k >. )
102 csbvarg 
 |-  ( l e. _V -> [_ l / j ]_ j = l )
103 csbconstg 
 |-  ( l e. _V -> [_ l / j ]_ k = k )
104 102 103 opeq12d 
 |-  ( l e. _V -> <. [_ l / j ]_ j , [_ l / j ]_ k >. = <. l , k >. )
105 101 104 eqtrd 
 |-  ( l e. _V -> [_ l / j ]_ <. j , k >. = <. l , k >. )
106 105 mpteq2dv 
 |-  ( l e. _V -> ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
107 100 106 eqtrd 
 |-  ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
108 107 cnveqd 
 |-  ( l e. _V -> `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
109 99 108 syl5eqr 
 |-  ( l e. _V -> [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
110 109 funeqd 
 |-  ( l e. _V -> ( Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
111 98 110 bitrd 
 |-  ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
112 58 111 ax-mp 
 |-  ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
113 97 54 112 3imtr3g 
 |-  ( ph -> ( l e. A -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
114 113 imp 
 |-  ( ( ph /\ l e. A ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
115 43 114 syldan 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
116 vsnid 
 |-  l e. { l }
117 116 a1i 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. { l } )
118 117 50 opelxpd 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> <. l , k >. e. ( { l } X. [_ l / j ]_ B ) )
119 1 69 65 77 47 115 63 118 esumc 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* k e. [_ l / j ]_ B [_ l / j ]_ C = sum* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F )
120 nfab1 
 |-  F/_ t { t | E. k e. [_ l / j ]_ B t = <. l , k >. }
121 nfcv 
 |-  F/_ t ( { l } X. [_ l / j ]_ B )
122 opeq1 
 |-  ( i = l -> <. i , k >. = <. l , k >. )
123 122 eqeq2d 
 |-  ( i = l -> ( t = <. i , k >. <-> t = <. l , k >. ) )
124 123 rexbidv 
 |-  ( i = l -> ( E. k e. [_ l / j ]_ B t = <. i , k >. <-> E. k e. [_ l / j ]_ B t = <. l , k >. ) )
125 58 124 rexsn 
 |-  ( E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. <-> E. k e. [_ l / j ]_ B t = <. l , k >. )
126 elxp2 
 |-  ( t e. ( { l } X. [_ l / j ]_ B ) <-> E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. )
127 abid 
 |-  ( t e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } <-> E. k e. [_ l / j ]_ B t = <. l , k >. )
128 125 126 127 3bitr4ri 
 |-  ( t e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } <-> t e. ( { l } X. [_ l / j ]_ B ) )
129 120 121 128 eqri 
 |-  { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B )
130 esumeq1 
 |-  ( { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B ) -> sum* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F = sum* z e. ( { l } X. [_ l / j ]_ B ) F )
131 129 130 ax-mp 
 |-  sum* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F = sum* z e. ( { l } X. [_ l / j ]_ B ) F
132 119 131 eqtrdi 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* k e. [_ l / j ]_ B [_ l / j ]_ C = sum* z e. ( { l } X. [_ l / j ]_ B ) F )
133 68 132 eqtrd 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* j e. { l } sum* k e. B C = sum* z e. ( { l } X. [_ l / j ]_ B ) F )
134 133 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> sum* j e. { l } sum* k e. B C = sum* z e. ( { l } X. [_ l / j ]_ B ) F )
135 34 134 oveq12d 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> ( sum* j e. b sum* k e. B C +e sum* j e. { l } sum* k e. B C ) = ( sum* z e. U_ j e. b ( { j } X. B ) F +e sum* z e. ( { l } X. [_ l / j ]_ B ) F ) )
136 nfv 
 |-  F/ j ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
137 nfcv 
 |-  F/_ j b
138 nfcv 
 |-  F/_ j { l }
139 vex 
 |-  b e. _V
140 139 a1i 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b e. _V )
141 snex 
 |-  { l } e. _V
142 141 a1i 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } e. _V )
143 42 eldifbd 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> -. l e. b )
144 disjsn 
 |-  ( ( b i^i { l } ) = (/) <-> -. l e. b )
145 143 144 sylibr 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( b i^i { l } ) = (/) )
146 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ph )
147 simprl 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b C_ A )
148 147 sselda 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. A )
149 5 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
150 149 ralrimiva 
 |-  ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
151 nfcv 
 |-  F/_ k B
152 151 esumcl 
 |-  ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> sum* k e. B C e. ( 0 [,] +oo ) )
153 4 150 152 syl2anc 
 |-  ( ( ph /\ j e. A ) -> sum* k e. B C e. ( 0 [,] +oo ) )
154 146 148 153 syl2anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> sum* k e. B C e. ( 0 [,] +oo ) )
155 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> ph )
156 43 snssd 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } C_ A )
157 156 sselda 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> j e. A )
158 155 157 153 syl2anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> sum* k e. B C e. ( 0 [,] +oo ) )
159 136 137 138 140 142 145 154 158 esumsplit 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* j e. ( b u. { l } ) sum* k e. B C = ( sum* j e. b sum* k e. B C +e sum* j e. { l } sum* k e. B C ) )
160 159 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> sum* j e. ( b u. { l } ) sum* k e. B C = ( sum* j e. b sum* k e. B C +e sum* j e. { l } sum* k e. B C ) )
161 iunxun 
 |-  U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. U_ j e. { l } ( { j } X. B ) )
162 138 35 nfxp 
 |-  F/_ j ( { l } X. [_ l / j ]_ B )
163 sneq 
 |-  ( j = l -> { j } = { l } )
164 163 38 xpeq12d 
 |-  ( j = l -> ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
165 162 164 iunxsngf 
 |-  ( l e. _V -> U_ j e. { l } ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
166 58 165 ax-mp 
 |-  U_ j e. { l } ( { j } X. B ) = ( { l } X. [_ l / j ]_ B )
167 166 uneq2i 
 |-  ( U_ j e. b ( { j } X. B ) u. U_ j e. { l } ( { j } X. B ) ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) )
168 161 167 eqtri 
 |-  U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) )
169 esumeq1 
 |-  ( U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) -> sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = sum* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F )
170 168 169 ax-mp 
 |-  sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = sum* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F
171 nfv 
 |-  F/ z ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
172 nfcv 
 |-  F/_ z U_ j e. b ( { j } X. B )
173 nfcv 
 |-  F/_ z ( { l } X. [_ l / j ]_ B )
174 snex 
 |-  { j } e. _V
175 148 44 syldan 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> B e. W )
176 xpexg 
 |-  ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
177 174 175 176 sylancr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( { j } X. B ) e. _V )
178 177 ralrimiva 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. b ( { j } X. B ) e. _V )
179 iunexg 
 |-  ( ( b e. _V /\ A. j e. b ( { j } X. B ) e. _V ) -> U_ j e. b ( { j } X. B ) e. _V )
180 139 178 179 sylancr 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) e. _V )
181 xpexg 
 |-  ( ( { l } e. _V /\ [_ l / j ]_ B e. W ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
182 141 47 181 sylancr 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
183 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. b )
184 143 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> -. l e. b )
185 nelne2 
 |-  ( ( j e. b /\ -. l e. b ) -> j =/= l )
186 183 184 185 syl2anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j =/= l )
187 disjsn2 
 |-  ( j =/= l -> ( { j } i^i { l } ) = (/) )
188 xpdisj1 
 |-  ( ( { j } i^i { l } ) = (/) -> ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
189 186 187 188 3syl 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
190 189 iuneq2dv 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = U_ j e. b (/) )
191 162 iunin1f 
 |-  U_ j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = ( U_ j e. b ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) )
192 iun0 
 |-  U_ j e. b (/) = (/)
193 190 191 192 3eqtr3g 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( U_ j e. b ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
194 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> ph )
195 iunss1 
 |-  ( b C_ A -> U_ j e. b ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
196 147 195 syl 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
197 196 sselda 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
198 nfv 
 |-  F/ j ph
199 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. B )
200 199 nfcri 
 |-  F/ j z e. U_ j e. A ( { j } X. B )
201 198 200 nfan 
 |-  F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
202 nfv 
 |-  F/ k ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) )
203 nfcv 
 |-  F/_ k ( 0 [,] +oo )
204 1 203 nfel 
 |-  F/ k F e. ( 0 [,] +oo )
205 2 adantl 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F = C )
206 simp-5l 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> ph )
207 simp-4r 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> j e. A )
208 simplr 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> k e. B )
209 206 207 208 5 syl12anc 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> C e. ( 0 [,] +oo ) )
210 205 209 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F e. ( 0 [,] +oo ) )
211 elsnxp 
 |-  ( j e. A -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) )
212 211 biimpa 
 |-  ( ( j e. A /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
213 212 adantll 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
214 202 204 210 213 r19.29af2 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
215 simpr 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
216 eliun 
 |-  ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
217 215 216 sylib 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A z e. ( { j } X. B ) )
218 201 214 217 r19.29af 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
219 194 197 218 syl2anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
220 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> ph )
221 nfcv 
 |-  F/_ j A
222 nfcv 
 |-  F/_ j l
223 221 222 162 164 ssiun2sf 
 |-  ( l e. A -> ( { l } X. [_ l / j ]_ B ) C_ U_ j e. A ( { j } X. B ) )
224 43 223 syl 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) C_ U_ j e. A ( { j } X. B ) )
225 224 sselda 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> z e. U_ j e. A ( { j } X. B ) )
226 220 225 218 syl2anc 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> F e. ( 0 [,] +oo ) )
227 171 172 173 180 182 193 219 226 esumsplit 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F = ( sum* z e. U_ j e. b ( { j } X. B ) F +e sum* z e. ( { l } X. [_ l / j ]_ B ) F ) )
228 170 227 syl5eq 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = ( sum* z e. U_ j e. b ( { j } X. B ) F +e sum* z e. ( { l } X. [_ l / j ]_ B ) F ) )
229 228 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = ( sum* z e. U_ j e. b ( { j } X. B ) F +e sum* z e. ( { l } X. [_ l / j ]_ B ) F ) )
230 135 160 229 3eqtr4d 
 |-  ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F ) -> sum* j e. ( b u. { l } ) sum* k e. B C = sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F )
231 230 ex 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( sum* j e. b sum* k e. B C = sum* z e. U_ j e. b ( { j } X. B ) F -> sum* j e. ( b u. { l } ) sum* k e. B C = sum* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F ) )
232 11 16 21 26 33 231 6 findcard2d 
 |-  ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F )