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