Metamath Proof Explorer

Theorem fsum2dlem

Description: Lemma for fsum2d - induction step. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fsum2d.1 
|- ( z = <. j , k >. -> D = C )
fsum2d.2 
|- ( ph -> A e. Fin )
fsum2d.3 
|- ( ( ph /\ j e. A ) -> B e. Fin )
fsum2d.4 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
fsum2d.5 
|- ( ph -> -. y e. x )
fsum2d.6 
|- ( ph -> ( x u. { y } ) C_ A )
fsum2d.7 
|- ( ps <-> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D )
Assertion fsum2dlem 
|- ( ( ph /\ ps ) -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )

Proof

Step Hyp Ref Expression
1 fsum2d.1 
 |-  ( z = <. j , k >. -> D = C )
2 fsum2d.2 
 |-  ( ph -> A e. Fin )
3 fsum2d.3 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fsum2d.4 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5 fsum2d.5 
 |-  ( ph -> -. y e. x )
6 fsum2d.6 
 |-  ( ph -> ( x u. { y } ) C_ A )
7 fsum2d.7 
 |-  ( ps <-> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D )
8 7 bilani 
 |-  ( ( ph /\ ps ) -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D )
9 csbeq1a 
 |-  ( j = m -> B = [_ m / j ]_ B )
10 csbeq1a 
 |-  ( j = m -> C = [_ m / j ]_ C )
11 10 adantr 
 |-  ( ( j = m /\ k e. B ) -> C = [_ m / j ]_ C )
12 9 11 sumeq12dv 
 |-  ( j = m -> sum_ k e. B C = sum_ k e. [_ m / j ]_ B [_ m / j ]_ C )
13 nfcv 
 |-  F/_ m sum_ k e. B C
14 nfcsb1v 
 |-  F/_ j [_ m / j ]_ B
15 nfcsb1v 
 |-  F/_ j [_ m / j ]_ C
16 14 15 nfsum 
 |-  F/_ j sum_ k e. [_ m / j ]_ B [_ m / j ]_ C
17 12 13 16 cbvsum 
 |-  sum_ j e. { y } sum_ k e. B C = sum_ m e. { y } sum_ k e. [_ m / j ]_ B [_ m / j ]_ C
18 6 unssbd 
 |-  ( ph -> { y } C_ A )
19 vex 
 |-  y e. _V
20 19 snss 
 |-  ( y e. A <-> { y } C_ A )
21 18 20 sylibr 
 |-  ( ph -> y e. A )
22 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
23 nfcsb1v 
 |-  F/_ j [_ y / j ]_ B
24 23 nfel1 
 |-  F/ j [_ y / j ]_ B e. Fin
25 csbeq1a 
 |-  ( j = y -> B = [_ y / j ]_ B )
26 25 eleq1d 
 |-  ( j = y -> ( B e. Fin <-> [_ y / j ]_ B e. Fin ) )
27 24 26 rspc 
 |-  ( y e. A -> ( A. j e. A B e. Fin -> [_ y / j ]_ B e. Fin ) )
28 21 22 27 sylc 
 |-  ( ph -> [_ y / j ]_ B e. Fin )
29 4 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B C e. CC )
30 nfcsb1v 
 |-  F/_ j [_ y / j ]_ C
31 30 nfel1 
 |-  F/ j [_ y / j ]_ C e. CC
32 23 31 nfralw 
 |-  F/ j A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC
33 csbeq1a 
 |-  ( j = y -> C = [_ y / j ]_ C )
34 33 eleq1d 
 |-  ( j = y -> ( C e. CC <-> [_ y / j ]_ C e. CC ) )
35 25 34 raleqbidv 
 |-  ( j = y -> ( A. k e. B C e. CC <-> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
36 32 35 rspc 
 |-  ( y e. A -> ( A. j e. A A. k e. B C e. CC -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
37 21 29 36 sylc 
 |-  ( ph -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
38 37 r19.21bi 
 |-  ( ( ph /\ k e. [_ y / j ]_ B ) -> [_ y / j ]_ C e. CC )
39 28 38 fsumcl 
 |-  ( ph -> sum_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
40 csbeq1 
 |-  ( m = y -> [_ m / j ]_ B = [_ y / j ]_ B )
41 csbeq1 
 |-  ( m = y -> [_ m / j ]_ C = [_ y / j ]_ C )
42 41 adantr 
 |-  ( ( m = y /\ k e. [_ m / j ]_ B ) -> [_ m / j ]_ C = [_ y / j ]_ C )
43 40 42 sumeq12dv 
 |-  ( m = y -> sum_ k e. [_ m / j ]_ B [_ m / j ]_ C = sum_ k e. [_ y / j ]_ B [_ y / j ]_ C )
44 43 sumsn 
 |-  ( ( y e. A /\ sum_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) -> sum_ m e. { y } sum_ k e. [_ m / j ]_ B [_ m / j ]_ C = sum_ k e. [_ y / j ]_ B [_ y / j ]_ C )
45 21 39 44 syl2anc 
 |-  ( ph -> sum_ m e. { y } sum_ k e. [_ m / j ]_ B [_ m / j ]_ C = sum_ k e. [_ y / j ]_ B [_ y / j ]_ C )
46 csbeq1a 
 |-  ( k = m -> [_ y / j ]_ C = [_ m / k ]_ [_ y / j ]_ C )
47 nfcv 
 |-  F/_ m [_ y / j ]_ C
48 nfcsb1v 
 |-  F/_ k [_ m / k ]_ [_ y / j ]_ C
49 46 47 48 cbvsum 
 |-  sum_ k e. [_ y / j ]_ B [_ y / j ]_ C = sum_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C
50 csbeq1 
 |-  ( m = ( 2nd ` z ) -> [_ m / k ]_ [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
51 snfi 
 |-  { y } e. Fin
52 xpfi 
 |-  ( ( { y } e. Fin /\ [_ y / j ]_ B e. Fin ) -> ( { y } X. [_ y / j ]_ B ) e. Fin )
53 51 28 52 sylancr 
 |-  ( ph -> ( { y } X. [_ y / j ]_ B ) e. Fin )
54 2ndconst 
 |-  ( y e. A -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
55 21 54 syl 
 |-  ( ph -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
56 fvres 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
57 56 adantl 
 |-  ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
58 48 nfel1 
 |-  F/ k [_ m / k ]_ [_ y / j ]_ C e. CC
59 46 eleq1d 
 |-  ( k = m -> ( [_ y / j ]_ C e. CC <-> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
60 58 59 rspc 
 |-  ( m e. [_ y / j ]_ B -> ( A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC -> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
61 37 60 mpan9 
 |-  ( ( ph /\ m e. [_ y / j ]_ B ) -> [_ m / k ]_ [_ y / j ]_ C e. CC )
62 50 53 55 57 61 fsumf1o 
 |-  ( ph -> sum_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = sum_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
63 elxp 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) )
64 nfv 
 |-  F/ j z = <. m , k >.
65 nfv 
 |-  F/ j m e. { y }
66 23 nfcri 
 |-  F/ j k e. [_ y / j ]_ B
67 65 66 nfan 
 |-  F/ j ( m e. { y } /\ k e. [_ y / j ]_ B )
68 64 67 nfan 
 |-  F/ j ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
69 68 nfex 
 |-  F/ j E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
70 nfv 
 |-  F/ m E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) )
71 opeq1 
 |-  ( m = j -> <. m , k >. = <. j , k >. )
72 71 eqeq2d 
 |-  ( m = j -> ( z = <. m , k >. <-> z = <. j , k >. ) )
73 velsn 
 |-  ( m e. { y } <-> m = y )
74 73 anbi1i 
 |-  ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( m = y /\ k e. [_ y / j ]_ B ) )
75 eqtr2 
 |-  ( ( m = j /\ m = y ) -> j = y )
76 75 25 syl 
 |-  ( ( m = j /\ m = y ) -> B = [_ y / j ]_ B )
77 76 eleq2d 
 |-  ( ( m = j /\ m = y ) -> ( k e. B <-> k e. [_ y / j ]_ B ) )
78 77 pm5.32da 
 |-  ( m = j -> ( ( m = y /\ k e. B ) <-> ( m = y /\ k e. [_ y / j ]_ B ) ) )
79 74 78 bitr4id 
 |-  ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( m = y /\ k e. B ) ) )
80 equequ1 
 |-  ( m = j -> ( m = y <-> j = y ) )
81 80 anbi1d 
 |-  ( m = j -> ( ( m = y /\ k e. B ) <-> ( j = y /\ k e. B ) ) )
82 79 81 bitrd 
 |-  ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. B ) ) )
83 72 82 anbi12d 
 |-  ( m = j -> ( ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
84 83 exbidv 
 |-  ( m = j -> ( E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
85 69 70 84 cbvexv1 
 |-  ( E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
86 63 85 bitri 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
87 nfv 
 |-  F/ j ph
88 nfcv 
 |-  F/_ j ( 2nd ` z )
89 88 30 nfcsbw 
 |-  F/_ j [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
90 89 nfeq2 
 |-  F/ j D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
91 nfv 
 |-  F/ k ph
92 nfcsb1v 
 |-  F/_ k [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
93 92 nfeq2 
 |-  F/ k D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
94 1 ad2antlr 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = C )
95 33 ad2antrl 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> C = [_ y / j ]_ C )
96 fveq2 
 |-  ( z = <. j , k >. -> ( 2nd ` z ) = ( 2nd ` <. j , k >. ) )
97 vex 
 |-  j e. _V
98 vex 
 |-  k e. _V
99 97 98 op2nd 
 |-  ( 2nd ` <. j , k >. ) = k
100 96 99 eqtr2di 
 |-  ( z = <. j , k >. -> k = ( 2nd ` z ) )
101 100 ad2antlr 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> k = ( 2nd ` z ) )
102 csbeq1a 
 |-  ( k = ( 2nd ` z ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
103 101 102 syl 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
104 94 95 103 3eqtrd 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
105 104 expl 
 |-  ( ph -> ( ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
106 91 93 105 exlimd 
 |-  ( ph -> ( E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
107 87 90 106 exlimd 
 |-  ( ph -> ( E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
108 86 107 biimtrid 
 |-  ( ph -> ( z e. ( { y } X. [_ y / j ]_ B ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
109 108 imp 
 |-  ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
110 109 sumeq2dv 
 |-  ( ph -> sum_ z e. ( { y } X. [_ y / j ]_ B ) D = sum_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
111 62 110 eqtr4d 
 |-  ( ph -> sum_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = sum_ z e. ( { y } X. [_ y / j ]_ B ) D )
112 49 111 eqtrid 
 |-  ( ph -> sum_ k e. [_ y / j ]_ B [_ y / j ]_ C = sum_ z e. ( { y } X. [_ y / j ]_ B ) D )
113 45 112 eqtrd 
 |-  ( ph -> sum_ m e. { y } sum_ k e. [_ m / j ]_ B [_ m / j ]_ C = sum_ z e. ( { y } X. [_ y / j ]_ B ) D )
114 17 113 eqtrid 
 |-  ( ph -> sum_ j e. { y } sum_ k e. B C = sum_ z e. ( { y } X. [_ y / j ]_ B ) D )
115 114 adantr 
 |-  ( ( ph /\ ps ) -> sum_ j e. { y } sum_ k e. B C = sum_ z e. ( { y } X. [_ y / j ]_ B ) D )
116 8 115 oveq12d 
 |-  ( ( ph /\ ps ) -> ( sum_ j e. x sum_ k e. B C + sum_ j e. { y } sum_ k e. B C ) = ( sum_ z e. U_ j e. x ( { j } X. B ) D + sum_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
117 disjsn 
 |-  ( ( x i^i { y } ) = (/) <-> -. y e. x )
118 5 117 sylibr 
 |-  ( ph -> ( x i^i { y } ) = (/) )
119 eqidd 
 |-  ( ph -> ( x u. { y } ) = ( x u. { y } ) )
120 2 6 ssfid 
 |-  ( ph -> ( x u. { y } ) e. Fin )
121 6 sselda 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> j e. A )
122 4 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. CC )
123 3 122 fsumcl 
 |-  ( ( ph /\ j e. A ) -> sum_ k e. B C e. CC )
124 121 123 syldan 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> sum_ k e. B C e. CC )
125 118 119 120 124 fsumsplit 
 |-  ( ph -> sum_ j e. ( x u. { y } ) sum_ k e. B C = ( sum_ j e. x sum_ k e. B C + sum_ j e. { y } sum_ k e. B C ) )
126 125 adantr 
 |-  ( ( ph /\ ps ) -> sum_ j e. ( x u. { y } ) sum_ k e. B C = ( sum_ j e. x sum_ k e. B C + sum_ j e. { y } sum_ k e. B C ) )
127 eliun 
 |-  ( z e. U_ j e. x ( { j } X. B ) <-> E. j e. x z e. ( { j } X. B ) )
128 xp1st 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
129 elsni 
 |-  ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j )
130 128 129 syl 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
131 130 adantl 
 |-  ( ( j e. x /\ z e. ( { j } X. B ) ) -> ( 1st ` z ) = j )
132 simpl 
 |-  ( ( j e. x /\ z e. ( { j } X. B ) ) -> j e. x )
133 131 132 eqeltrd 
 |-  ( ( j e. x /\ z e. ( { j } X. B ) ) -> ( 1st ` z ) e. x )
134 133 rexlimiva 
 |-  ( E. j e. x z e. ( { j } X. B ) -> ( 1st ` z ) e. x )
135 127 134 sylbi 
 |-  ( z e. U_ j e. x ( { j } X. B ) -> ( 1st ` z ) e. x )
136 xp1st 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) -> ( 1st ` z ) e. { y } )
137 135 136 anim12i 
 |-  ( ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
138 elin 
 |-  ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) <-> ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) )
139 elin 
 |-  ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
140 137 138 139 3imtr4i 
 |-  ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> ( 1st ` z ) e. ( x i^i { y } ) )
141 118 eleq2d 
 |-  ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( 1st ` z ) e. (/) ) )
142 noel 
 |-  -. ( 1st ` z ) e. (/)
143 142 pm2.21i 
 |-  ( ( 1st ` z ) e. (/) -> z e. (/) )
144 141 143 biimtrdi 
 |-  ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) -> z e. (/) ) )
145 140 144 syl5 
 |-  ( ph -> ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> z e. (/) ) )
146 145 ssrdv 
 |-  ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) )
147 ss0 
 |-  ( ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
148 146 147 syl 
 |-  ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
149 iunxun 
 |-  U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) )
150 nfcv 
 |-  F/_ m ( { j } X. B )
151 nfcv 
 |-  F/_ j { m }
152 151 14 nfxp 
 |-  F/_ j ( { m } X. [_ m / j ]_ B )
153 sneq 
 |-  ( j = m -> { j } = { m } )
154 153 9 xpeq12d 
 |-  ( j = m -> ( { j } X. B ) = ( { m } X. [_ m / j ]_ B ) )
155 150 152 154 cbviun 
 |-  U_ j e. { y } ( { j } X. B ) = U_ m e. { y } ( { m } X. [_ m / j ]_ B )
156 sneq 
 |-  ( m = y -> { m } = { y } )
157 156 40 xpeq12d 
 |-  ( m = y -> ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B ) )
158 19 157 iunxsn 
 |-  U_ m e. { y } ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B )
159 155 158 eqtri 
 |-  U_ j e. { y } ( { j } X. B ) = ( { y } X. [_ y / j ]_ B )
160 159 uneq2i 
 |-  ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
161 149 160 eqtri 
 |-  U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
162 161 a1i 
 |-  ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) ) )
163 snfi 
 |-  { j } e. Fin
164 121 3 syldan 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> B e. Fin )
165 xpfi 
 |-  ( ( { j } e. Fin /\ B e. Fin ) -> ( { j } X. B ) e. Fin )
166 163 164 165 sylancr 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( { j } X. B ) e. Fin )
167 166 ralrimiva 
 |-  ( ph -> A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
168 iunfi 
 |-  ( ( ( x u. { y } ) e. Fin /\ A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin ) -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
169 120 167 168 syl2anc 
 |-  ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
170 eliun 
 |-  ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) <-> E. j e. ( x u. { y } ) z e. ( { j } X. B ) )
171 elxp 
 |-  ( z e. ( { j } X. B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) )
172 simprl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. m , k >. )
173 simprrl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m e. { j } )
174 elsni 
 |-  ( m e. { j } -> m = j )
175 173 174 syl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m = j )
176 175 opeq1d 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> <. m , k >. = <. j , k >. )
177 172 176 eqtrd 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. j , k >. )
178 177 1 syl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D = C )
179 simpll 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> ph )
180 121 adantr 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> j e. A )
181 simprrr 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> k e. B )
182 179 180 181 4 syl12anc 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> C e. CC )
183 178 182 eqeltrd 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D e. CC )
184 183 ex 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
185 184 exlimdvv 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
186 171 185 biimtrid 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( z e. ( { j } X. B ) -> D e. CC ) )
187 186 rexlimdva 
 |-  ( ph -> ( E. j e. ( x u. { y } ) z e. ( { j } X. B ) -> D e. CC ) )
188 170 187 biimtrid 
 |-  ( ph -> ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) -> D e. CC ) )
189 188 imp 
 |-  ( ( ph /\ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) ) -> D e. CC )
190 148 162 169 189 fsumsplit 
 |-  ( ph -> sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( sum_ z e. U_ j e. x ( { j } X. B ) D + sum_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
191 190 adantr 
 |-  ( ( ph /\ ps ) -> sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( sum_ z e. U_ j e. x ( { j } X. B ) D + sum_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
192 116 126 191 3eqtr4d 
 |-  ( ( ph /\ ps ) -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )