MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsum2dlem Unicode version

Theorem fsum2dlem 12483
Description: Lemma for fsum2d 12484- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.)
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 )
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
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 )
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 fsum2dlem
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 simpr 448 . . . 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 189 . . 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 2525 . . . . . 6  |-  F/_ m sum_ k  e.  B  C
5 nfcsb1v 3228 . . . . . . 7  |-  F/_ j [_ m  /  j ]_ B
6 nfcsb1v 3228 . . . . . . 7  |-  F/_ j [_ m  /  j ]_ C
75, 6nfsum 12414 . . . . . 6  |-  F/_ j sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C
8 csbeq1a 3204 . . . . . . 7  |-  ( j  =  m  ->  B  =  [_ m  /  j ]_ B )
9 csbeq1a 3204 . . . . . . . 8  |-  ( j  =  m  ->  C  =  [_ m  /  j ]_ C )
109adantr 452 . . . . . . 7  |-  ( ( j  =  m  /\  k  e.  B )  ->  C  =  [_ m  /  j ]_ C
)
118, 10sumeq12dv 12429 . . . . . 6  |-  ( j  =  m  ->  sum_ k  e.  B  C  =  sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C )
124, 7, 11cbvsumi 12420 . . . . 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 3470 . . . . . . . 8  |-  ( ph  ->  { y }  C_  A )
15 vex 2904 . . . . . . . . 9  |-  y  e. 
_V
1615snss 3871 . . . . . . . 8  |-  ( y  e.  A  <->  { y }  C_  A )
1714, 16sylibr 204 . . . . . . 7  |-  ( ph  ->  y  e.  A )
18 fsum2d.3 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  Fin )
1918ralrimiva 2734 . . . . . . . . 9  |-  ( ph  ->  A. j  e.  A  B  e.  Fin )
20 nfcsb1v 3228 . . . . . . . . . . 11  |-  F/_ j [_ y  /  j ]_ B
2120nfel1 2535 . . . . . . . . . 10  |-  F/ j
[_ y  /  j ]_ B  e.  Fin
22 csbeq1a 3204 . . . . . . . . . . 11  |-  ( j  =  y  ->  B  =  [_ y  /  j ]_ B )
2322eleq1d 2455 . . . . . . . . . 10  |-  ( j  =  y  ->  ( B  e.  Fin  <->  [_ y  / 
j ]_ B  e.  Fin ) )
2421, 23rspc 2991 . . . . . . . . 9  |-  ( y  e.  A  ->  ( A. j  e.  A  B  e.  Fin  ->  [_ y  /  j ]_ B  e.  Fin ) )
2517, 19, 24sylc 58 . . . . . . . 8  |-  ( ph  ->  [_ y  /  j ]_ B  e.  Fin )
26 fsum2d.4 . . . . . . . . . . 11  |-  ( (
ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )
2726ralrimivva 2743 . . . . . . . . . 10  |-  ( ph  ->  A. j  e.  A  A. k  e.  B  C  e.  CC )
28 nfcsb1v 3228 . . . . . . . . . . . . 13  |-  F/_ j [_ y  /  j ]_ C
2928nfel1 2535 . . . . . . . . . . . 12  |-  F/ j
[_ y  /  j ]_ C  e.  CC
3020, 29nfral 2704 . . . . . . . . . . 11  |-  F/ j A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC
31 csbeq1a 3204 . . . . . . . . . . . . 13  |-  ( j  =  y  ->  C  =  [_ y  /  j ]_ C )
3231eleq1d 2455 . . . . . . . . . . . 12  |-  ( j  =  y  ->  ( C  e.  CC  <->  [_ y  / 
j ]_ C  e.  CC ) )
3322, 32raleqbidv 2861 . . . . . . . . . . 11  |-  ( j  =  y  ->  ( A. k  e.  B  C  e.  CC  <->  A. k  e.  [_  y  /  j ]_ B [_ y  / 
j ]_ C  e.  CC ) )
3430, 33rspc 2991 . . . . . . . . . 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 58 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC )
3635r19.21bi 2749 . . . . . . . 8  |-  ( (
ph  /\  k  e.  [_ y  /  j ]_ B )  ->  [_ y  /  j ]_ C  e.  CC )
3725, 36fsumcl 12456 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC )
38 csbeq1 3199 . . . . . . . . 9  |-  ( m  =  y  ->  [_ m  /  j ]_ B  =  [_ y  /  j ]_ B )
39 csbeq1 3199 . . . . . . . . . 10  |-  ( m  =  y  ->  [_ m  /  j ]_ C  =  [_ y  /  j ]_ C )
4039adantr 452 . . . . . . . . 9  |-  ( ( m  =  y  /\  k  e.  [_ m  / 
j ]_ B )  ->  [_ m  /  j ]_ C  =  [_ y  /  j ]_ C
)
4138, 40sumeq12dv 12429 . . . . . . . 8  |-  ( m  =  y  ->  sum_ k  e.  [_  m  /  j ]_ B [_ m  / 
j ]_ C  =  sum_ k  e.  [_  y  / 
j ]_ B [_ y  /  j ]_ C
)
4241sumsn 12463 . . . . . . 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 643 . . . . . 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 2525 . . . . . . . 8  |-  F/_ m [_ y  /  j ]_ C
45 nfcsb1v 3228 . . . . . . . 8  |-  F/_ k [_ m  /  k ]_ [_ y  /  j ]_ C
46 csbeq1a 3204 . . . . . . . 8  |-  ( k  =  m  ->  [_ y  /  j ]_ C  =  [_ m  /  k ]_ [_ y  /  j ]_ C )
4744, 45, 46cbvsumi 12420 . . . . . . 7  |-  sum_ k  e.  [_  y  /  j ]_ B [_ y  / 
j ]_ C  =  sum_ m  e.  [_  y  / 
j ]_ B [_ m  /  k ]_ [_ y  /  j ]_ C
48 csbeq1 3199 . . . . . . . . 9  |-  ( m  =  ( 2nd `  z
)  ->  [_ m  / 
k ]_ [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
49 snfi 7125 . . . . . . . . . 10  |-  { y }  e.  Fin
50 xpfi 7316 . . . . . . . . . 10  |-  ( ( { y }  e.  Fin  /\  [_ y  / 
j ]_ B  e.  Fin )  ->  ( { y }  X.  [_ y  /  j ]_ B
)  e.  Fin )
5149, 25, 50sylancr 645 . . . . . . . . 9  |-  ( ph  ->  ( { y }  X.  [_ y  / 
j ]_ B )  e. 
Fin )
52 2ndconst 6377 . . . . . . . . . 10  |-  ( y  e.  A  ->  ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B
) ) : ( { y }  X.  [_ y  /  j ]_ B ) -1-1-onto-> [_ y  /  j ]_ B )
5317, 52syl 16 . . . . . . . . 9  |-  ( ph  ->  ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B ) ) : ( { y }  X.  [_ y  / 
j ]_ B ) -1-1-onto-> [_ y  /  j ]_ B
)
54 fvres 5687 . . . . . . . . . 10  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  ->  ( ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B
) ) `  z
)  =  ( 2nd `  z ) )
5554adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( { y }  X.  [_ y  /  j ]_ B ) )  -> 
( ( 2nd  |`  ( { y }  X.  [_ y  /  j ]_ B ) ) `  z )  =  ( 2nd `  z ) )
5645nfel1 2535 . . . . . . . . . . 11  |-  F/ k
[_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC
5746eleq1d 2455 . . . . . . . . . . 11  |-  ( k  =  m  ->  ( [_ y  /  j ]_ C  e.  CC  <->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC )
)
5856, 57rspc 2991 . . . . . . . . . 10  |-  ( m  e.  [_ y  / 
j ]_ B  ->  ( A. k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  e.  CC  ->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC ) )
5935, 58mpan9 456 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  [_ y  /  j ]_ B )  ->  [_ m  /  k ]_ [_ y  /  j ]_ C  e.  CC )
6048, 51, 53, 55, 59fsumf1o 12446 . . . . . . . 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 )
61 elxp 4837 . . . . . . . . . . . 12  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  <->  E. m E. k
( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) ) )
62 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ j  z  =  <. m ,  k >.
63 nfv 1626 . . . . . . . . . . . . . . . 16  |-  F/ j  m  e.  { y }
6420nfcri 2519 . . . . . . . . . . . . . . . 16  |-  F/ j  k  e.  [_ y  /  j ]_ B
6563, 64nfan 1836 . . . . . . . . . . . . . . 15  |-  F/ j ( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )
6662, 65nfan 1836 . . . . . . . . . . . . . 14  |-  F/ j ( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) )
6766nfex 1855 . . . . . . . . . . . . 13  |-  F/ j E. k ( z  =  <. m ,  k
>.  /\  ( m  e. 
{ y }  /\  k  e.  [_ y  / 
j ]_ B ) )
68 nfv 1626 . . . . . . . . . . . . 13  |-  F/ m E. k ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )
69 opeq1 3928 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  <. m ,  k >.  =  <. j ,  k >. )
7069eqeq2d 2400 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  (
z  =  <. m ,  k >.  <->  z  =  <. j ,  k >.
) )
71 eqtr2 2407 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  =  j  /\  m  =  y )  ->  j  =  y )
7271, 22syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  =  j  /\  m  =  y )  ->  B  =  [_ y  /  j ]_ B
)
7372eleq2d 2456 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  =  j  /\  m  =  y )  ->  ( k  e.  B  <->  k  e.  [_ y  / 
j ]_ B ) )
7473pm5.32da 623 . . . . . . . . . . . . . . . . 17  |-  ( m  =  j  ->  (
( m  =  y  /\  k  e.  B
)  <->  ( m  =  y  /\  k  e. 
[_ y  /  j ]_ B ) ) )
75 elsn 3774 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  { y }  <-> 
m  =  y )
7675anbi1i 677 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B )  <->  ( m  =  y  /\  k  e.  [_ y  /  j ]_ B ) )
7774, 76syl6rbbr 256 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  (
( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )  <->  ( m  =  y  /\  k  e.  B ) ) )
78 equequ1 1691 . . . . . . . . . . . . . . . . 17  |-  ( m  =  j  ->  (
m  =  y  <->  j  =  y ) )
7978anbi1d 686 . . . . . . . . . . . . . . . 16  |-  ( m  =  j  ->  (
( m  =  y  /\  k  e.  B
)  <->  ( j  =  y  /\  k  e.  B ) ) )
8077, 79bitrd 245 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  (
( m  e.  {
y }  /\  k  e.  [_ y  /  j ]_ B )  <->  ( j  =  y  /\  k  e.  B ) ) )
8170, 80anbi12d 692 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  (
( z  =  <. m ,  k >.  /\  (
m  e.  { y }  /\  k  e. 
[_ y  /  j ]_ B ) )  <->  ( z  =  <. j ,  k
>.  /\  ( j  =  y  /\  k  e.  B ) ) ) )
8281exbidv 1633 . . . . . . . . . . . . 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 )
) ) )
8367, 68, 82cbvex 2025 . . . . . . . . . . . 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
) ) )
8461, 83bitri 241 . . . . . . . . . . 11  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  <->  E. j E. k
( z  =  <. j ,  k >.  /\  (
j  =  y  /\  k  e.  B )
) )
85 nfv 1626 . . . . . . . . . . . 12  |-  F/ j
ph
86 nfcv 2525 . . . . . . . . . . . . . 14  |-  F/_ j
( 2nd `  z
)
8786, 28nfcsb 3230 . . . . . . . . . . . . 13  |-  F/_ j [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C
8887nfeq2 2536 . . . . . . . . . . . 12  |-  F/ j  D  =  [_ ( 2nd `  z )  / 
k ]_ [_ y  / 
j ]_ C
89 nfv 1626 . . . . . . . . . . . . 13  |-  F/ k
ph
90 nfcsb1v 3228 . . . . . . . . . . . . . 14  |-  F/_ k [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C
9190nfeq2 2536 . . . . . . . . . . . . 13  |-  F/ k  D  =  [_ ( 2nd `  z )  / 
k ]_ [_ y  / 
j ]_ C
92 fsum2d.1 . . . . . . . . . . . . . . . 16  |-  ( z  =  <. j ,  k
>.  ->  D  =  C )
9392ad2antlr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  C )
9431ad2antrl 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  C  =  [_ y  /  j ]_ C )
95 fveq2 5670 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  <. j ,  k
>.  ->  ( 2nd `  z
)  =  ( 2nd `  <. j ,  k
>. ) )
96 vex 2904 . . . . . . . . . . . . . . . . . . 19  |-  j  e. 
_V
97 vex 2904 . . . . . . . . . . . . . . . . . . 19  |-  k  e. 
_V
9896, 97op2nd 6297 . . . . . . . . . . . . . . . . . 18  |-  ( 2nd `  <. j ,  k
>. )  =  k
9995, 98syl6req 2438 . . . . . . . . . . . . . . . . 17  |-  ( z  =  <. j ,  k
>.  ->  k  =  ( 2nd `  z ) )
10099ad2antlr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  k  =  ( 2nd `  z ) )
101 csbeq1a 3204 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( 2nd `  z
)  ->  [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
102100, 101syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  [_ y  / 
j ]_ C  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C
)
10393, 94, 1023eqtrd 2425 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  =  <. j ,  k
>. )  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C )
104103expl 602 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10589, 91, 104exlimd 1814 . . . . . . . . . . . 12  |-  ( ph  ->  ( E. k ( z  =  <. j ,  k >.  /\  (
j  =  y  /\  k  e.  B )
)  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10685, 88, 105exlimd 1814 . . . . . . . . . . 11  |-  ( ph  ->  ( E. j E. k ( z  = 
<. j ,  k >.  /\  ( j  =  y  /\  k  e.  B
) )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
10784, 106syl5bi 209 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B )  ->  D  =  [_ ( 2nd `  z
)  /  k ]_ [_ y  /  j ]_ C ) )
108107imp 419 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( { y }  X.  [_ y  /  j ]_ B ) )  ->  D  =  [_ ( 2nd `  z )  /  k ]_ [_ y  /  j ]_ C )
109108sumeq2dv 12426 . . . . . . . 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 )
11060, 109eqtr4d 2424 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  [_  y  /  j ]_ B [_ m  /  k ]_ [_ y  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11147, 110syl5eq 2433 . . . . . 6  |-  ( ph  -> 
sum_ k  e.  [_  y  /  j ]_ B [_ y  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11243, 111eqtrd 2421 . . . . 5  |-  ( ph  -> 
sum_ m  e.  { y } sum_ k  e.  [_  m  /  j ]_ B [_ m  /  j ]_ C  =  sum_ z  e.  ( {
y }  X.  [_ y  /  j ]_ B
) D )
11312, 112syl5eq 2433 . . . 4  |-  ( ph  -> 
sum_ j  e.  {
y } sum_ k  e.  B  C  =  sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B
) D )
114113adantr 452 . . 3  |-  ( (
ph  /\  ps )  -> 
sum_ j  e.  {
y } sum_ k  e.  B  C  =  sum_ z  e.  ( { y }  X.  [_ y  /  j ]_ B
) D )
1153, 114oveq12d 6040 . 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 ) )
116 fsum2d.5 . . . . 5  |-  ( ph  ->  -.  y  e.  x
)
117 disjsn 3813 . . . . 5  |-  ( ( x  i^i  { y } )  =  (/)  <->  -.  y  e.  x )
118116, 117sylibr 204 . . . 4  |-  ( ph  ->  ( x  i^i  {
y } )  =  (/) )
119 eqidd 2390 . . . 4  |-  ( ph  ->  ( x  u.  {
y } )  =  ( x  u.  {
y } ) )
120 fsum2d.2 . . . . 5  |-  ( ph  ->  A  e.  Fin )
121 ssfi 7267 . . . . 5  |-  ( ( A  e.  Fin  /\  ( x  u.  { y } )  C_  A
)  ->  ( x  u.  { y } )  e.  Fin )
122120, 13, 121syl2anc 643 . . . 4  |-  ( ph  ->  ( x  u.  {
y } )  e. 
Fin )
12313sselda 3293 . . . . 5  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
j  e.  A )
12426anassrs 630 . . . . . 6  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  B )  ->  C  e.  CC )
12518, 124fsumcl 12456 . . . . 5  |-  ( (
ph  /\  j  e.  A )  ->  sum_ k  e.  B  C  e.  CC )
126123, 125syldan 457 . . . 4  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  ->  sum_ k  e.  B  C  e.  CC )
127118, 119, 122, 126fsumsplit 12462 . . 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 )
)
128127adantr 452 . 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 )
)
129 eliun 4041 . . . . . . . . . 10  |-  ( z  e.  U_ j  e.  x  ( { j }  X.  B )  <->  E. j  e.  x  z  e.  ( {
j }  X.  B
) )
130 xp1st 6317 . . . . . . . . . . . . . 14  |-  ( z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  { j } )
131 elsni 3783 . . . . . . . . . . . . . 14  |-  ( ( 1st `  z )  e.  { j }  ->  ( 1st `  z
)  =  j )
132130, 131syl 16 . . . . . . . . . . . . 13  |-  ( z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  =  j )
133132adantl 453 . . . . . . . . . . . 12  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  ( 1st `  z )  =  j )
134 simpl 444 . . . . . . . . . . . 12  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  j  e.  x )
135133, 134eqeltrd 2463 . . . . . . . . . . 11  |-  ( ( j  e.  x  /\  z  e.  ( {
j }  X.  B
) )  ->  ( 1st `  z )  e.  x )
136135rexlimiva 2770 . . . . . . . . . 10  |-  ( E. j  e.  x  z  e.  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  x )
137129, 136sylbi 188 . . . . . . . . 9  |-  ( z  e.  U_ j  e.  x  ( { j }  X.  B )  ->  ( 1st `  z
)  e.  x )
138 xp1st 6317 . . . . . . . . 9  |-  ( z  e.  ( { y }  X.  [_ y  /  j ]_ B
)  ->  ( 1st `  z )  e.  {
y } )
139137, 138anim12i 550 . . . . . . . 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 } ) )
140 elin 3475 . . . . . . . 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 ) ) )
141 elin 3475 . . . . . . . 8  |-  ( ( 1st `  z )  e.  ( x  i^i 
{ y } )  <-> 
( ( 1st `  z
)  e.  x  /\  ( 1st `  z )  e.  { y } ) )
142139, 140, 1413imtr4i 258 . . . . . . 7  |-  ( z  e.  ( U_ j  e.  x  ( {
j }  X.  B
)  i^i  ( {
y }  X.  [_ y  /  j ]_ B
) )  ->  ( 1st `  z )  e.  ( x  i^i  {
y } ) )
143118eleq2d 2456 . . . . . . . 8  |-  ( ph  ->  ( ( 1st `  z
)  e.  ( x  i^i  { y } )  <->  ( 1st `  z
)  e.  (/) ) )
144 noel 3577 . . . . . . . . 9  |-  -.  ( 1st `  z )  e.  (/)
145144pm2.21i 125 . . . . . . . 8  |-  ( ( 1st `  z )  e.  (/)  ->  z  e.  (/) )
146143, 145syl6bi 220 . . . . . . 7  |-  ( ph  ->  ( ( 1st `  z
)  e.  ( x  i^i  { y } )  ->  z  e.  (/) ) )
147142, 146syl5 30 . . . . . 6  |-  ( ph  ->  ( z  e.  (
U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B ) )  -> 
z  e.  (/) ) )
148147ssrdv 3299 . . . . 5  |-  ( ph  ->  ( U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B
) )  C_  (/) )
149 ss0 3603 . . . . 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
) )  =  (/) )
150148, 149syl 16 . . . 4  |-  ( ph  ->  ( U_ j  e.  x  ( { j }  X.  B )  i^i  ( { y }  X.  [_ y  /  j ]_ B
) )  =  (/) )
151 iunxun 4115 . . . . . 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 ) )
152 nfcv 2525 . . . . . . . . 9  |-  F/_ m
( { j }  X.  B )
153 nfcv 2525 . . . . . . . . . 10  |-  F/_ j { m }
154153, 5nfxp 4846 . . . . . . . . 9  |-  F/_ j
( { m }  X.  [_ m  /  j ]_ B )
155 sneq 3770 . . . . . . . . . 10  |-  ( j  =  m  ->  { j }  =  { m } )
156155, 8xpeq12d 4845 . . . . . . . . 9  |-  ( j  =  m  ->  ( { j }  X.  B )  =  ( { m }  X.  [_ m  /  j ]_ B ) )
157152, 154, 156cbviun 4071 . . . . . . . 8  |-  U_ j  e.  { y }  ( { j }  X.  B )  =  U_ m  e.  { y }  ( { m }  X.  [_ m  / 
j ]_ B )
158 sneq 3770 . . . . . . . . . 10  |-  ( m  =  y  ->  { m }  =  { y } )
159158, 38xpeq12d 4845 . . . . . . . . 9  |-  ( m  =  y  ->  ( { m }  X.  [_ m  /  j ]_ B )  =  ( { y }  X.  [_ y  /  j ]_ B ) )
16015, 159iunxsn 4113 . . . . . . . 8  |-  U_ m  e.  { y }  ( { m }  X.  [_ m  /  j ]_ B )  =  ( { y }  X.  [_ y  /  j ]_ B )
161157, 160eqtri 2409 . . . . . . 7  |-  U_ j  e.  { y }  ( { j }  X.  B )  =  ( { y }  X.  [_ y  /  j ]_ B )
162161uneq2i 3443 . . . . . 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 ) )
163151, 162eqtri 2409 . . . . 5  |-  U_ j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  =  (
U_ j  e.  x  ( { j }  X.  B )  u.  ( { y }  X.  [_ y  /  j ]_ B ) )
164163a1i 11 . . . 4  |-  ( ph  ->  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  =  ( U_ j  e.  x  ( { j }  X.  B )  u.  ( { y }  X.  [_ y  /  j ]_ B ) ) )
165 snfi 7125 . . . . . . 7  |-  { j }  e.  Fin
166123, 18syldan 457 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  ->  B  e.  Fin )
167 xpfi 7316 . . . . . . 7  |-  ( ( { j }  e.  Fin  /\  B  e.  Fin )  ->  ( { j }  X.  B )  e.  Fin )
168165, 166, 167sylancr 645 . . . . . 6  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( { j }  X.  B )  e. 
Fin )
169168ralrimiva 2734 . . . . 5  |-  ( ph  ->  A. j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  e.  Fin )
170 iunfi 7332 . . . . 5  |-  ( ( ( 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 )
171122, 169, 170syl2anc 643 . . . 4  |-  ( ph  ->  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B
)  e.  Fin )
172 eliun 4041 . . . . . 6  |-  ( z  e.  U_ j  e.  ( x  u.  {
y } ) ( { j }  X.  B )  <->  E. j  e.  ( x  u.  {
y } ) z  e.  ( { j }  X.  B ) )
173 elxp 4837 . . . . . . . 8  |-  ( z  e.  ( { j }  X.  B )  <->  E. m E. k ( z  =  <. m ,  k >.  /\  (
m  e.  { j }  /\  k  e.  B ) ) )
174 simprl 733 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  z  =  <. m ,  k >. )
175 simprrl 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  m  e.  {
j } )
176 elsni 3783 . . . . . . . . . . . . . . 15  |-  ( m  e.  { j }  ->  m  =  j )
177175, 176syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  m  =  j )
178177opeq1d 3934 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  <. m ,  k
>.  =  <. j ,  k >. )
179174, 178eqtrd 2421 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  z  =  <. j ,  k >. )
180179, 92syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  D  =  C )
181 simpll 731 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  ph )
182123adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  j  e.  A
)
183 simprrr 742 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  k  e.  B
)
184181, 182, 183, 26syl12anc 1182 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  C  e.  CC )
185180, 184eqeltrd 2463 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( x  u.  {
y } ) )  /\  ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) ) )  ->  D  e.  CC )
186185ex 424 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) )  ->  D  e.  CC )
)
187186exlimdvv 1644 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( E. m E. k ( z  = 
<. m ,  k >.  /\  ( m  e.  {
j }  /\  k  e.  B ) )  ->  D  e.  CC )
)
188173, 187syl5bi 209 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( x  u.  { y } ) )  -> 
( z  e.  ( { j }  X.  B )  ->  D  e.  CC ) )
189188rexlimdva 2775 . . . . . 6  |-  ( ph  ->  ( E. j  e.  ( x  u.  {
y } ) z  e.  ( { j }  X.  B )  ->  D  e.  CC ) )
190172, 189syl5bi 209 . . . . 5  |-  ( ph  ->  ( z  e.  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B )  ->  D  e.  CC )
)
191190imp 419 . . . 4  |-  ( (
ph  /\  z  e.  U_ j  e.  ( x  u.  { y } ) ( { j }  X.  B ) )  ->  D  e.  CC )
192150, 164, 171, 191fsumsplit 12462 . . 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 ) )
193192adantr 452 . 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 ) )
194115, 128, 1933eqtr4d 2431 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    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1717   A.wral 2651   E.wrex 2652   [_csb 3196    u. cun 3263    i^i cin 3264    C_ wss 3265   (/)c0 3573   {csn 3759   <.cop 3762   U_ciun 4037    X. cxp 4818    |` cres 4822   -1-1-onto->wf1o 5395   ` cfv 5396  (class class class)co 6022   1stc1st 6288   2ndc2nd 6289   Fincfn 7047   CCcc 8923    + caddc 8928   sum_csu 12408
This theorem is referenced by:  fsum2d  12484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-inf2 7531  ax-cnex 8981  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002  ax-pre-sup 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-se 4485  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-isom 5405  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-1st 6290  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-1o 6662  df-oadd 6666  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-sup 7383  df-oi 7414  df-card 7761  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612  df-nn 9935  df-2 9992  df-3 9993  df-n0 10156  df-z 10217  df-uz 10423  df-rp 10547  df-fz 10978  df-fzo 11068  df-seq 11253  df-exp 11312  df-hash 11548  df-cj 11833  df-re 11834  df-im 11835  df-sqr 11969  df-abs 11970  df-clim 12211  df-sum 12409
  Copyright terms: Public domain W3C validator