ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fsum2dlemstep Unicode version

Theorem fsum2dlemstep 11154
Description: Lemma for fsum2d 11155- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
Hypotheses
Ref Expression
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 )
fsum2dlemstep.x  |-  ( ph  ->  x  e.  Fin )
fsum2d.7  |-  ( ps  <->  sum_ j  e.  x  sum_ k  e.  B  C  =  sum_ z  e.  U_  j  e.  x  ( { j }  X.  B ) D )
Assertion
Ref Expression
fsum2dlemstep  |-  ( (
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 )
Distinct variable groups:    j, k, x, y, z, A    B, k, x, y, z    D, j, k, x, y    x, C, y, z    ph, j,
k, z
Allowed substitution hints:    ph( x, y)    ps( x, y, z, j, k)    B( j)    C( j, k)    D( z)

Proof of Theorem fsum2dlemstep
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 simpr 109 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
2 fsum2d.7 . . . 4  |-  ( ps  <->  sum_ j  e.  x  sum_ k  e.  B  C  =  sum_ z  e.  U_  j  e.  x  ( { j }  X.  B ) D )
31, 2sylib 121 . . 3  |-  ( (
ph  /\  ps )  -> 
sum_ j  e.  x  sum_ k  e.  B  C  =  sum_ z  e.  U_  j  e.  x  ( { j }  X.  B ) D )
4 nfcv 2256 . . . . . 6  |-  F/_ m sum_ k  e.  B  C
5 nfcsb1v 3003 . . . . . . 7  |-  F/_ j [_ m  /  j ]_ B
6 nfcsb1v 3003 . . . . . . 7  |-  F/_ j [_ m  /  j ]_ C
75, 6nfsum 11077 . . . . . 6  |-  F/_ j sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C
8 csbeq1a 2981 . . . . . . 7  |-  ( j  =  m  ->  B  =  [_ m  /  j ]_ B )
9 csbeq1a 2981 . . . . . . . 8  |-  ( j  =  m  ->  C  =  [_ m  /  j ]_ C )
109adantr 272 . . . . . . 7  |-  ( ( j  =  m  /\  k  e.  B )  ->  C  =  [_ m  /  j ]_ C
)
118, 10sumeq12dv 11092 . . . . . 6  |-  ( j  =  m  ->  sum_ k  e.  B  C  =  sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C )
124, 7, 11cbvsumi 11082 . . . . 5  |-  sum_ j  e.  { y } sum_ k  e.  B  C  =  sum_ m  e.  {
y } sum_ k  e.  [_  m  /  j ]_ B [_ m  / 
j ]_ C
13 fsum2d.6 . . . . . . . . 9  |-  ( ph  ->  ( x  u.  {
y } )  C_  A )
1413unssbd 3222 . . . . . . . 8  |-  ( ph  ->  { y }  C_  A )
15 vex 2661 . . . . . . . . 9  |-  y  e. 
_V
1615snss 3617 . . . . . . . 8  |-  ( y  e.  A  <->  { y }  C_  A )
1714, 16sylibr 133 . . . . . . 7  |-  ( ph  ->  y  e.  A )
18 fsum2d.3 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  Fin )
1918ralrimiva 2480 . . . . . . . . 9  |-  ( ph  ->  A. j  e.  A  B  e.  Fin )
20 nfcsb1v 3003 . . . . . . . . . . 11  |-  F/_ j [_ y  /  j ]_ B
2120nfel1 2267 . . . . . . . . . 10  |-  F/ j
[_ y  /  j ]_ B  e.  Fin
22 csbeq1a 2981 . . . . . . . . . . 11  |-  ( j  =  y  ->  B  =  [_ y  /  j ]_ B )
2322eleq1d 2184 . . . . . . . . . 10  |-  ( j  =  y  ->  ( B  e.  Fin  <->  [_ y  / 
j ]_ B  e.  Fin ) )
2421, 23rspc 2755 . . . . . . . . 9  |-  ( y  e.  A  ->  ( A. j  e.  A  B  e.  Fin  ->  [_ y  /  j ]_ B  e.  Fin ) )
2517, 19, 24sylc 62 . . . . . . . 8  |-  ( ph  ->  [_ y  /  j ]_ B  e.  Fin )
26 fsum2d.4 . . . . . . . . . . 11  |-  ( (
ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )
2726ralrimivva 2489 . . . . . . . . . 10  |-  ( ph  ->  A. j  e.  A  A. k  e.  B  C  e.  CC )
28 nfcsb1v 3003 . . . . . . . . . . . . 13  |-  F/_ j [_ y  /  j ]_ C
2928nfel1 2267 . . . . . . . . . . . 12  |-  F/ j
[_ y  /  j ]_ C  e.  CC
3020, 29nfralxy 2446 . . . . . . . . . . 11  |-  F/ j A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC
31 csbeq1a 2981 . . . . . . . . . . . . 13  |-  ( j  =  y  ->  C  =  [_ y  /  j ]_ C )
3231eleq1d 2184 . . . . . . . . . . . 12  |-  ( j  =  y  ->  ( C  e.  CC  <->  [_ y  / 
j ]_ C  e.  CC ) )
3322, 32raleqbidv 2613 . . . . . . . . . . 11  |-  ( j  =  y  ->  ( A. k  e.  B  C  e.  CC  <->  A. k  e.  [_  y  /  j ]_ B [_ y  / 
j ]_ C  e.  CC ) )
3430, 33rspc 2755 . . . . . . . . . 10  |-  ( 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 ) )
3517, 27, 34sylc 62 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC )
3635r19.21bi 2495 . . . . . . . 8  |-  ( (
ph  /\  k  e.  [_ y  /  j ]_ B )  ->  [_ y  /  j ]_ C  e.  CC )
3725, 36fsumcl 11120 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC )
38 csbeq1 2976 . . . . . . . . 9  |-  ( m  =  y  ->  [_ m  /  j ]_ B  =  [_ y  /  j ]_ B )
39 csbeq1 2976 . . . . . . . . . 10  |-  ( m  =  y  ->  [_ m  /  j ]_ C  =  [_ y  /  j ]_ C )
4039adantr 272 . . . . . . . . 9  |-  ( ( m  =  y  /\  k  e.  [_ m  / 
j ]_ B )  ->  [_ m  /  j ]_ C  =  [_ y  /  j ]_ C
)
4138, 40sumeq12dv 11092 . . . . . . . 8  |-  ( m  =  y  ->  sum_ k  e.  [_  m  /  j ]_ B [_ m  / 
j ]_ C  =  sum_ k  e.  [_  y  / 
j ]_ B [_ y  /  j ]_ C
)
4241sumsn 11131 . . . . . . 7  |-  ( ( 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
)
4317, 37, 42syl2anc 406 . . . . . 6  |-  ( ph  -> 
sum_ m  e.  { y } sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C  =  sum_ k  e.  [_  y  / 
j ]_ B [_ y  /  j ]_ C
)
44 nfcv 2256 . . . . . . . 8  |-  F/_ m [_ y  /  j ]_ C
45 nfcsb1v 3003 . . . . . . . 8  |-  F/_ k [_ m  /  k ]_ [_ y  /  j ]_ C
46 csbeq1a 2981 . . . . . . . 8  |-  ( k  =  m  ->  [_ y  /  j ]_ C  =  [_ m  /  k ]_ [_ y  /  j ]_ C )
4744, 45, 46cbvsumi 11082 . . . . . . 7  |-  sum_ k  e.  [_  y  /  j ]_ B [_ y  / 
j ]_ C  =  sum_ m  e.  [_  y  / 
j ]_ B [_ m  /  k ]_ [_ y  /  j ]_ C
48 csbeq1 2976 . . . . . . . . 9  |-  ( m  =  ( 2nd `  z
)  ->  [_ m  / 
k ]_ [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
49 snfig 6674 . . . . . . . . . . 11  |-  ( y  e.  _V  ->  { y }  e.  Fin )
5049elv 2662 . . . . . . . . . 10  |-  { y }  e.  Fin
51 xpfi 6784 . . . . . . . . . 10  |-  ( ( { y }  e.  Fin  /\  [_ y  / 
j ]_ B  e.  Fin )  ->  ( { y }  X.  [_ y  /  j ]_ B
)  e.  Fin )
5250, 25, 51sylancr 408 . . . . . . . . 9  |-  ( ph  ->  ( { y }  X.  [_ y  / 
j ]_ B )  e. 
Fin )
53 2ndconst 6085 . . . . . . . . . 10  |-  ( y  e.  A  ->  ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B
) ) : ( { y }  X.  [_ y  /  j ]_ B ) -1-1-onto-> [_ y  /  j ]_ B )
5417, 53syl 14 . . . . . . . . 9  |-  ( ph  ->  ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B ) ) : ( { y }  X.  [_ y  / 
j ]_ B ) -1-1-onto-> [_ y  /  j ]_ B
)
55 fvres 5411 . . . . . . . . . 10  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  ->  ( ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B
) ) `  z
)  =  ( 2nd `  z ) )
5655adantl 273 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( { y }  X.  [_ y  /  j ]_ B ) )  -> 
( ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B ) ) `  z )  =  ( 2nd `  z ) )
5745nfel1 2267 . . . . . . . . . . 11  |-  F/ k
[_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC
5846eleq1d 2184 . . . . . . . . . . 11  |-  ( k  =  m  ->  ( [_ y  /  j ]_ C  e.  CC  <->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC )
)
5957, 58rspc 2755 . . . . . . . . . 10  |-  ( m  e.  [_ y  / 
j ]_ B  ->  ( A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC  ->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC ) )
6035, 59mpan9 277 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  [_ y  /  j ]_ B )  ->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC )
6148, 52, 54, 56, 60fsumf1o 11110 . . . . . . . 8  |-  ( 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 )
62 elxp 4524 . . . . . . . . . . . 12  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  <->  E. m E. k
( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) ) )
63 nfv 1491 . . . . . . . . . . . . . . 15  |-  F/ j  z  =  <. m ,  k >.
64 nfv 1491 . . . . . . . . . . . . . . . 16  |-  F/ j  m  e.  { y }
6520nfcri 2250 . . . . . . . . . . . . . . . 16  |-  F/ j  k  e.  [_ y  /  j ]_ B
6664, 65nfan 1527 . . . . . . . . . . . . . . 15  |-  F/ j ( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )
6763, 66nfan 1527 . . . . . . . . . . . . . 14  |-  F/ j ( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) )
6867nfex 1599 . . . . . . . . . . . . 13  |-  F/ j E. k ( z  =  <. m ,  k
>.  /\  ( m  e. 
{ y }  /\  k  e.  [_ y  / 
j ]_ B ) )
69 nfv 1491 . . . . . . . . . . . . 13  |-  F/ m E. k ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )
70 opeq1 3673 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  <. m ,  k >.  =  <. j ,  k >. )
7170eqeq2d 2127 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  (
z  =  <. m ,  k >.  <->  z  =  <. j ,  k >.
) )
72 eqtr2 2134 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  =  j  /\  m  =  y )  ->  j  =  y )
7372, 22syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  =  j  /\  m  =  y )  ->  B  =  [_ y  /  j ]_ B
)
7473eleq2d 2185 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  =  j  /\  m  =  y )  ->  ( k  e.  B  <->  k  e.  [_ y  / 
j ]_ B ) )
7574pm5.32da 445 . . . . . . . . . . . . . . . . 17  |-  ( m  =  j  ->  (
( m  =  y  /\  k  e.  B
)  <->  ( m  =  y  /\  k  e. 
[_ y  /  j ]_ B ) ) )
76 velsn 3512 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  { y }  <-> 
m  =  y )
7776anbi1i 451 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B )  <->  ( m  =  y  /\  k  e.  [_ y  /  j ]_ B ) )
7875, 77syl6rbbr 198 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  (
( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )  <->  ( m  =  y  /\  k  e.  B ) ) )
79 equequ1 1671 . . . . . . . . . . . . . . . . 17  |-  ( m  =  j  ->  (
m  =  y  <->  j  =  y ) )
8079anbi1d 458 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  (
( m  =  y  /\  k  e.  B
)  <->  ( j  =  y  /\  k  e.  B ) ) )
8178, 80bitrd 187 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  (
( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )  <->  ( j  =  y  /\  k  e.  B ) ) )
8271, 81anbi12d 462 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  (
( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) )  <->  ( z  =  <. j ,  k
>.  /\  ( j  =  y  /\  k  e.  B ) ) ) )
8382exbidv 1779 . . . . . . . . . . . . 13  |-  ( 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 )
) ) )
8468, 69, 83cbvex 1712 . . . . . . . . . . . 12  |-  ( 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
) ) )
8562, 84bitri 183 . . . . . . . . . . 11  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  <->  E. j E. k
( z  =  <. j ,  k >.  /\  (
j  =  y  /\  k  e.  B )
) )
86 nfv 1491 . . . . . . . . . . . 12  |-  F/ j
ph
87 nfcv 2256 . . . . . . . . . . . . . 14  |-  F/_ j
( 2nd `  z
)
8887, 28nfcsb 3005 . . . . . . . . . . . . 13  |-  F/_ j [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C
8988nfeq2 2268 . . . . . . . . . . . 12  |-  F/ j  D  =  [_ ( 2nd `  z )  / 
k ]_ [_ y  / 
j ]_ C
90 nfv 1491 . . . . . . . . . . . . 13  |-  F/ k
ph
91 nfcsb1v 3003 . . . . . . . . . . . . . 14  |-  F/_ k [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C
9291nfeq2 2268 . . . . . . . . . . . . 13  |-  F/ k  D  =  [_ ( 2nd `  z )  / 
k ]_ [_ y  / 
j ]_ C
93 fsum2d.1 . . . . . . . . . . . . . . . 16  |-  ( z  =  <. j ,  k
>.  ->  D  =  C )
9493ad2antlr 478 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  C )
9531ad2antrl 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  C  =  [_ y  /  j ]_ C )
96 fveq2 5387 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  <. j ,  k
>.  ->  ( 2nd `  z
)  =  ( 2nd `  <. j ,  k
>. ) )
97 vex 2661 . . . . . . . . . . . . . . . . . . 19  |-  j  e. 
_V
98 vex 2661 . . . . . . . . . . . . . . . . . . 19  |-  k  e. 
_V
9997, 98op2nd 6011 . . . . . . . . . . . . . . . . . 18  |-  ( 2nd `  <. j ,  k
>. )  =  k
10096, 99syl6req 2165 . . . . . . . . . . . . . . . . 17  |-  ( z  =  <. j ,  k
>.  ->  k  =  ( 2nd `  z ) )
101100ad2antlr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  k  =  ( 2nd `  z ) )
102 csbeq1a 2981 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( 2nd `  z
)  ->  [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
103101, 102syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
10494, 95, 1033eqtrd 2152 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C )
105104expl 373 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10690, 92, 105exlimd 1559 . . . . . . . . . . . 12  |-  ( ph  ->  ( E. k ( z  =  <. j ,  k >.  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10786, 89, 106exlimd 1559 . . . . . . . . . . 11  |-  ( ph  ->  ( E. j E. k ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10885, 107syl5bi 151 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
109108imp 123 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( { y }  X.  [_ y  /  j ]_ B ) )  ->  D  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C )
110109sumeq2dv 11088 . . . . . . . 8  |-  ( ph  -> 
sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B ) D  = 
sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B ) [_ ( 2nd `  z )  / 
k ]_ [_ y  / 
j ]_ C )
11161, 110eqtr4d 2151 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  [_  y  /  j ]_ B [_ m  /  k ]_ [_ y  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11247, 111syl5eq 2160 . . . . . 6  |-  ( ph  -> 
sum_ k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11343, 112eqtrd 2148 . . . . 5  |-  ( ph  -> 
sum_ m  e.  { y } sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11412, 113syl5eq 2160 . . . 4  |-  ( ph  -> 
sum_ j  e.  {
y } sum_ k  e.  B  C  =  sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B
) D )
115114adantr 272 . . 3  |-  ( (
ph  /\  ps )  -> 
sum_ j  e.  {
y } sum_ k  e.  B  C  =  sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B
) D )
1163, 115oveq12d 5758 . 2  |-  ( (
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 fsum2d.5 . . . . 5  |-  ( ph  ->  -.  y  e.  x
)
118 disjsn 3553 . . . . 5  |-  ( ( x  i^i  { y } )  =  (/)  <->  -.  y  e.  x )
119117, 118sylibr 133 . . . 4  |-  ( ph  ->  ( x  i^i  {
y } )  =  (/) )
120 eqidd 2116 . . . 4  |-  ( ph  ->  ( x  u.  {
y } )  =  ( x  u.  {
y } ) )
121 fsum2dlemstep.x . . . . 5  |-  ( ph  ->  x  e.  Fin )
12250a1i 9 . . . . 5  |-  ( ph  ->  { y }  e.  Fin )
123 unfidisj 6776 . . . . 5  |-  ( ( x  e.  Fin  /\  { y }  e.  Fin  /\  ( x  i^i  {
y } )  =  (/) )  ->  ( x  u.  { y } )  e.  Fin )
124121, 122, 119, 123syl3anc 1199 . . . 4  |-  ( ph  ->  ( x  u.  {
y } )  e. 
Fin )
12513sselda 3065 . . . . 5  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
j  e.  A )
12626anassrs 395 . . . . . 6  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  B )  ->  C  e.  CC )
12718, 126fsumcl 11120 . . . . 5  |-  ( (
ph  /\  j  e.  A )  ->  sum_ k  e.  B  C  e.  CC )
128125, 127syldan 278 . . . 4  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  ->  sum_ k  e.  B  C  e.  CC )
129119, 120, 124, 128fsumsplit 11127 . . 3  |-  ( 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 )
)
130129adantr 272 . 2  |-  ( (
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 )
)
131 eliun 3785 . . . . . . . . . 10  |-  ( z  e.  U_ j  e.  x  ( { j }  X.  B )  <->  E. j  e.  x  z  e.  ( {
j }  X.  B
) )
132 xp1st 6029 . . . . . . . . . . . . . 14  |-  ( z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  { j } )
133 elsni 3513 . . . . . . . . . . . . . 14  |-  ( ( 1st `  z )  e.  { j }  ->  ( 1st `  z
)  =  j )
134132, 133syl 14 . . . . . . . . . . . . 13  |-  ( z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  =  j )
135134adantl 273 . . . . . . . . . . . 12  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  ( 1st `  z )  =  j )
136 simpl 108 . . . . . . . . . . . 12  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  j  e.  x )
137135, 136eqeltrd 2192 . . . . . . . . . . 11  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  ( 1st `  z )  e.  x )
138137rexlimiva 2519 . . . . . . . . . 10  |-  ( E. j  e.  x  z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  x )
139131, 138sylbi 120 . . . . . . . . 9  |-  ( z  e.  U_ j  e.  x  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  x )
140 xp1st 6029 . . . . . . . . 9  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  ->  ( 1st `  z )  e.  {
y } )
141139, 140anim12i 334 . . . . . . . 8  |-  ( ( z  e.  U_ j  e.  x  ( {
j }  X.  B
)  /\  z  e.  ( { y }  X.  [_ y  /  j ]_ B ) )  -> 
( ( 1st `  z
)  e.  x  /\  ( 1st `  z )  e.  { y } ) )
142 elin 3227 . . . . . . . 8  |-  ( 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 ) ) )
143 elin 3227 . . . . . . . 8  |-  ( ( 1st `  z )  e.  ( x  i^i 
{ y } )  <-> 
( ( 1st `  z
)  e.  x  /\  ( 1st `  z )  e.  { y } ) )
144141, 142, 1433imtr4i 200 . . . . . . 7  |-  ( z  e.  ( U_ j  e.  x  ( {
j }  X.  B
)  i^i  ( {
y }  X.  [_ y  /  j ]_ B
) )  ->  ( 1st `  z )  e.  ( x  i^i  {
y } ) )
145119eleq2d 2185 . . . . . . . 8  |-  ( ph  ->  ( ( 1st `  z
)  e.  ( x  i^i  { y } )  <->  ( 1st `  z
)  e.  (/) ) )
146 noel 3335 . . . . . . . . 9  |-  -.  ( 1st `  z )  e.  (/)
147146pm2.21i 618 . . . . . . . 8  |-  ( ( 1st `  z )  e.  (/)  ->  z  e.  (/) )
148145, 147syl6bi 162 . . . . . . 7  |-  ( ph  ->  ( ( 1st `  z
)  e.  ( x  i^i  { y } )  ->  z  e.  (/) ) )
149144, 148syl5 32 . . . . . 6  |-  ( ph  ->  ( z  e.  (
U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B ) )  -> 
z  e.  (/) ) )
150149ssrdv 3071 . . . . 5  |-  ( ph  ->  ( U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B
) )  C_  (/) )
151 ss0 3371 . . . . 5  |-  ( (
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
) )  =  (/) )
152150, 151syl 14 . . . 4  |-  ( ph  ->  ( U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B
) )  =  (/) )
153 iunxun 3860 . . . . . 6  |-  U_ j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  =  (
U_ j  e.  x  ( { j }  X.  B )  u.  U_ j  e.  { y }  ( { j }  X.  B ) )
154 nfcv 2256 . . . . . . . . 9  |-  F/_ m
( { j }  X.  B )
155 nfcv 2256 . . . . . . . . . 10  |-  F/_ j { m }
156155, 5nfxp 4534 . . . . . . . . 9  |-  F/_ j
( { m }  X.  [_ m  /  j ]_ B )
157 sneq 3506 . . . . . . . . . 10  |-  ( j  =  m  ->  { j }  =  { m } )
158157, 8xpeq12d 4532 . . . . . . . . 9  |-  ( j  =  m  ->  ( { j }  X.  B )  =  ( { m }  X.  [_ m  /  j ]_ B ) )
159154, 156, 158cbviun 3818 . . . . . . . 8  |-  U_ j  e.  { y }  ( { j }  X.  B )  =  U_ m  e.  { y }  ( { m }  X.  [_ m  / 
j ]_ B )
160 sneq 3506 . . . . . . . . . 10  |-  ( m  =  y  ->  { m }  =  { y } )
161160, 38xpeq12d 4532 . . . . . . . . 9  |-  ( m  =  y  ->  ( { m }  X.  [_ m  /  j ]_ B )  =  ( { y }  X.  [_ y  /  j ]_ B ) )
16215, 161iunxsn 3857 . . . . . . . 8  |-  U_ m  e.  { y }  ( { m }  X.  [_ m  /  j ]_ B )  =  ( { y }  X.  [_ y  /  j ]_ B )
163159, 162eqtri 2136 . . . . . . 7  |-  U_ j  e.  { y }  ( { j }  X.  B )  =  ( { y }  X.  [_ y  /  j ]_ B )
164163uneq2i 3195 . . . . . 6  |-  ( 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 ) )
165153, 164eqtri 2136 . . . . 5  |-  U_ j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  =  (
U_ j  e.  x  ( { j }  X.  B )  u.  ( { y }  X.  [_ y  /  j ]_ B ) )
166165a1i 9 . . . 4  |-  ( ph  ->  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  =  ( U_ j  e.  x  ( { j }  X.  B )  u.  ( { y }  X.  [_ y  /  j ]_ B ) ) )
167 snfig 6674 . . . . . . . 8  |-  ( j  e.  _V  ->  { j }  e.  Fin )
168167elv 2662 . . . . . . 7  |-  { j }  e.  Fin
169125, 18syldan 278 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  ->  B  e.  Fin )
170 xpfi 6784 . . . . . . 7  |-  ( ( { j }  e.  Fin  /\  B  e.  Fin )  ->  ( { j }  X.  B )  e.  Fin )
171168, 169, 170sylancr 408 . . . . . 6  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( { j }  X.  B )  e. 
Fin )
172171ralrimiva 2480 . . . . 5  |-  ( ph  ->  A. j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  e.  Fin )
173 disjsnxp 6100 . . . . . 6  |- Disj  j  e.  ( x  u.  {
y } ) ( { j }  X.  B )
174173a1i 9 . . . . 5  |-  ( ph  -> Disj  j  e.  ( x  u.  { y } ) ( { j }  X.  B ) )
175 iunfidisj 6800 . . . . 5  |-  ( ( ( x  u.  {
y } )  e. 
Fin  /\  A. j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  e.  Fin  /\ Disj  j  e.  ( x  u.  { y } ) ( { j }  X.  B ) )  ->  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  e.  Fin )
176124, 172, 174, 175syl3anc 1199 . . . 4  |-  ( ph  ->  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  e.  Fin )
177 eliun 3785 . . . . . 6  |-  ( z  e.  U_ j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  <->  E. j  e.  ( x  u.  {
y } ) z  e.  ( { j }  X.  B ) )
178 elxp 4524 . . . . . . . 8  |-  ( z  e.  ( { j }  X.  B )  <->  E. m E. k ( z  =  <. m ,  k >.  /\  (
m  e.  { j }  /\  k  e.  B ) ) )
179 simprl 503 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  z  =  <. m ,  k >. )
180 simprrl 511 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  m  e.  {
j } )
181 elsni 3513 . . . . . . . . . . . . . . 15  |-  ( m  e.  { j }  ->  m  =  j )
182180, 181syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  m  =  j )
183182opeq1d 3679 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  <. m ,  k
>.  =  <. j ,  k >. )
184179, 183eqtrd 2148 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  z  =  <. j ,  k >. )
185184, 93syl 14 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  D  =  C )
186 simpll 501 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  ph )
187125adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  j  e.  A
)
188 simprrr 512 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  k  e.  B
)
189186, 187, 188, 26syl12anc 1197 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  C  e.  CC )
190185, 189eqeltrd 2192 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  D  e.  CC )
191190ex 114 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) )  ->  D  e.  CC )
)
192191exlimdvv 1851 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( E. m E. k ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) )  ->  D  e.  CC )
)
193178, 192syl5bi 151 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( z  e.  ( { j }  X.  B )  ->  D  e.  CC ) )
194193rexlimdva 2524 . . . . . 6  |-  ( ph  ->  ( E. j  e.  ( x  u.  {
y } ) z  e.  ( { j }  X.  B )  ->  D  e.  CC ) )
195177, 194syl5bi 151 . . . . 5  |-  ( ph  ->  ( z  e.  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B )  ->  D  e.  CC )
)
196195imp 123 . . . 4  |-  ( (
ph  /\  z  e.  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B ) )  ->  D  e.  CC )
197152, 166, 176, 196fsumsplit 11127 . . 3  |-  ( 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 ) )
198197adantr 272 . 2  |-  ( (
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 ) )
199116, 130, 1983eqtr4d 2158 1  |-  ( (
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 )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1314   E.wex 1451    e. wcel 1463   A.wral 2391   E.wrex 2392   _Vcvv 2658   [_csb 2973    u. cun 3037    i^i cin 3038    C_ wss 3039   (/)c0 3331   {csn 3495   <.cop 3498   U_ciun 3781  Disj wdisj 3874    X. cxp 4505    |` cres 4509   -1-1-onto->wf1o 5090   ` cfv 5091  (class class class)co 5740   1stc1st 6002   2ndc2nd 6003   Fincfn 6600   CCcc 7582    + caddc 7587   sum_csu 11073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-disj 3875  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-oadd 6283  df-er 6395  df-en 6601  df-dom 6602  df-fin 6603  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8396  df-inn 8681  df-2 8739  df-3 8740  df-4 8741  df-n0 8932  df-z 9009  df-uz 9279  df-q 9364  df-rp 9394  df-fz 9742  df-fzo 9871  df-seqfrec 10170  df-exp 10244  df-ihash 10473  df-cj 10565  df-re 10566  df-im 10567  df-rsqrt 10721  df-abs 10722  df-clim 10999  df-sumdc 11074
This theorem is referenced by:  fsum2d  11155
  Copyright terms: Public domain W3C validator