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

Theorem fprodcom2fi 11589
Description: Interchange order of multiplication. Note that  B ( j ) and  D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
Hypotheses
Ref Expression
fprodcom2.1  |-  ( ph  ->  A  e.  Fin )
fprodcom2.2  |-  ( ph  ->  C  e.  Fin )
fprodcom2.3  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  Fin )
fprodcom2fi.d  |-  ( (
ph  /\  k  e.  C )  ->  D  e.  Fin )
fprodcom2.4  |-  ( ph  ->  ( ( j  e.  A  /\  k  e.  B )  <->  ( k  e.  C  /\  j  e.  D ) ) )
fprodcom2.5  |-  ( (
ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  E  e.  CC )
Assertion
Ref Expression
fprodcom2fi  |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  E  =  prod_ k  e.  C  prod_ j  e.  D  E
)
Distinct variable groups:    A, j, k    B, k    C, j, k    D, j    ph, j, k
Allowed substitution hints:    B( j)    D( k)    E( j, k)

Proof of Theorem fprodcom2fi
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 4720 . . . . . . . . 9  |-  Rel  ( { j }  X.  B )
21rgenw 2525 . . . . . . . 8  |-  A. j  e.  A  Rel  ( { j }  X.  B
)
3 reliun 4732 . . . . . . . 8  |-  ( Rel  U_ j  e.  A  ( { j }  X.  B )  <->  A. j  e.  A  Rel  ( { j }  X.  B
) )
42, 3mpbir 145 . . . . . . 7  |-  Rel  U_ j  e.  A  ( {
j }  X.  B
)
5 relcnv 4989 . . . . . . 7  |-  Rel  `' U_ k  e.  C  ( { k }  X.  D )
6 ancom 264 . . . . . . . . . . . 12  |-  ( ( x  =  j  /\  y  =  k )  <->  ( y  =  k  /\  x  =  j )
)
7 vex 2733 . . . . . . . . . . . . 13  |-  x  e. 
_V
8 vex 2733 . . . . . . . . . . . . 13  |-  y  e. 
_V
97, 8opth 4222 . . . . . . . . . . . 12  |-  ( <.
x ,  y >.  =  <. j ,  k
>. 
<->  ( x  =  j  /\  y  =  k ) )
108, 7opth 4222 . . . . . . . . . . . 12  |-  ( <.
y ,  x >.  = 
<. k ,  j >.  <->  ( y  =  k  /\  x  =  j )
)
116, 9, 103bitr4i 211 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  <. j ,  k
>. 
<-> 
<. y ,  x >.  = 
<. k ,  j >.
)
1211a1i 9 . . . . . . . . . 10  |-  ( ph  ->  ( <. x ,  y
>.  =  <. j ,  k >.  <->  <. y ,  x >.  =  <. k ,  j
>. ) )
13 fprodcom2.4 . . . . . . . . . 10  |-  ( ph  ->  ( ( j  e.  A  /\  k  e.  B )  <->  ( k  e.  C  /\  j  e.  D ) ) )
1412, 13anbi12d 470 . . . . . . . . 9  |-  ( ph  ->  ( ( <. x ,  y >.  =  <. j ,  k >.  /\  (
j  e.  A  /\  k  e.  B )
)  <->  ( <. y ,  x >.  =  <. k ,  j >.  /\  (
k  e.  C  /\  j  e.  D )
) ) )
15142exbidv 1861 . . . . . . . 8  |-  ( ph  ->  ( E. j E. k ( <. x ,  y >.  =  <. j ,  k >.  /\  (
j  e.  A  /\  k  e.  B )
)  <->  E. j E. k
( <. y ,  x >.  =  <. k ,  j
>.  /\  ( k  e.  C  /\  j  e.  D ) ) ) )
16 eliunxp 4750 . . . . . . . 8  |-  ( <.
x ,  y >.  e.  U_ j  e.  A  ( { j }  X.  B )  <->  E. j E. k ( <. x ,  y >.  =  <. j ,  k >.  /\  (
j  e.  A  /\  k  e.  B )
) )
177, 8opelcnv 4793 . . . . . . . . 9  |-  ( <.
x ,  y >.  e.  `' U_ k  e.  C  ( { k }  X.  D )  <->  <. y ,  x >.  e.  U_ k  e.  C  ( {
k }  X.  D
) )
18 eliunxp 4750 . . . . . . . . 9  |-  ( <.
y ,  x >.  e. 
U_ k  e.  C  ( { k }  X.  D )  <->  E. k E. j ( <. y ,  x >.  =  <. k ,  j >.  /\  (
k  e.  C  /\  j  e.  D )
) )
19 excom 1657 . . . . . . . . 9  |-  ( E. k E. j (
<. y ,  x >.  = 
<. k ,  j >.  /\  ( k  e.  C  /\  j  e.  D
) )  <->  E. j E. k ( <. y ,  x >.  =  <. k ,  j >.  /\  (
k  e.  C  /\  j  e.  D )
) )
2017, 18, 193bitri 205 . . . . . . . 8  |-  ( <.
x ,  y >.  e.  `' U_ k  e.  C  ( { k }  X.  D )  <->  E. j E. k ( <. y ,  x >.  =  <. k ,  j >.  /\  (
k  e.  C  /\  j  e.  D )
) )
2115, 16, 203bitr4g 222 . . . . . . 7  |-  ( ph  ->  ( <. x ,  y
>.  e.  U_ j  e.  A  ( { j }  X.  B )  <->  <. x ,  y >.  e.  `' U_ k  e.  C  ( { k }  X.  D ) ) )
224, 5, 21eqrelrdv 4707 . . . . . 6  |-  ( ph  ->  U_ j  e.  A  ( { j }  X.  B )  =  `' U_ k  e.  C  ( { k }  X.  D ) )
23 nfcv 2312 . . . . . . 7  |-  F/_ x
( { j }  X.  B )
24 nfcv 2312 . . . . . . . 8  |-  F/_ j { x }
25 nfcsb1v 3082 . . . . . . . 8  |-  F/_ j [_ x  /  j ]_ B
2624, 25nfxp 4638 . . . . . . 7  |-  F/_ j
( { x }  X.  [_ x  /  j ]_ B )
27 sneq 3594 . . . . . . . 8  |-  ( j  =  x  ->  { j }  =  { x } )
28 csbeq1a 3058 . . . . . . . 8  |-  ( j  =  x  ->  B  =  [_ x  /  j ]_ B )
2927, 28xpeq12d 4636 . . . . . . 7  |-  ( j  =  x  ->  ( { j }  X.  B )  =  ( { x }  X.  [_ x  /  j ]_ B ) )
3023, 26, 29cbviun 3910 . . . . . 6  |-  U_ j  e.  A  ( {
j }  X.  B
)  =  U_ x  e.  A  ( {
x }  X.  [_ x  /  j ]_ B
)
31 nfcv 2312 . . . . . . . 8  |-  F/_ y
( { k }  X.  D )
32 nfcv 2312 . . . . . . . . 9  |-  F/_ k { y }
33 nfcsb1v 3082 . . . . . . . . 9  |-  F/_ k [_ y  /  k ]_ D
3432, 33nfxp 4638 . . . . . . . 8  |-  F/_ k
( { y }  X.  [_ y  / 
k ]_ D )
35 sneq 3594 . . . . . . . . 9  |-  ( k  =  y  ->  { k }  =  { y } )
36 csbeq1a 3058 . . . . . . . . 9  |-  ( k  =  y  ->  D  =  [_ y  /  k ]_ D )
3735, 36xpeq12d 4636 . . . . . . . 8  |-  ( k  =  y  ->  ( { k }  X.  D )  =  ( { y }  X.  [_ y  /  k ]_ D ) )
3831, 34, 37cbviun 3910 . . . . . . 7  |-  U_ k  e.  C  ( {
k }  X.  D
)  =  U_ y  e.  C  ( {
y }  X.  [_ y  /  k ]_ D
)
3938cnveqi 4786 . . . . . 6  |-  `' U_ k  e.  C  ( { k }  X.  D )  =  `' U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )
4022, 30, 393eqtr3g 2226 . . . . 5  |-  ( ph  ->  U_ x  e.  A  ( { x }  X.  [_ x  /  j ]_ B )  =  `' U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )
4140prodeq1d 11527 . . . 4  |-  ( ph  ->  prod_ z  e.  U_  x  e.  A  ( { x }  X.  [_ x  /  j ]_ B ) [_ ( 2nd `  z )  / 
k ]_ [_ ( 1st `  z )  /  j ]_ E  =  prod_ z  e.  `'  U_ y  e.  C  ( {
y }  X.  [_ y  /  k ]_ D
) [_ ( 2nd `  z
)  /  k ]_ [_ ( 1st `  z
)  /  j ]_ E )
428, 7op1std 6127 . . . . . . 7  |-  ( w  =  <. y ,  x >.  ->  ( 1st `  w
)  =  y )
4342csbeq1d 3056 . . . . . 6  |-  ( w  =  <. y ,  x >.  ->  [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ ( 2nd `  w )  /  j ]_ E )
448, 7op2ndd 6128 . . . . . . . 8  |-  ( w  =  <. y ,  x >.  ->  ( 2nd `  w
)  =  x )
4544csbeq1d 3056 . . . . . . 7  |-  ( w  =  <. y ,  x >.  ->  [_ ( 2nd `  w
)  /  j ]_ E  =  [_ x  / 
j ]_ E )
4645csbeq2dv 3075 . . . . . 6  |-  ( w  =  <. y ,  x >.  ->  [_ y  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ x  / 
j ]_ E )
4743, 46eqtrd 2203 . . . . 5  |-  ( w  =  <. y ,  x >.  ->  [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ x  / 
j ]_ E )
487, 8op2ndd 6128 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( 2nd `  z
)  =  y )
4948csbeq1d 3056 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  [_ ( 2nd `  z
)  /  k ]_ [_ ( 1st `  z
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ ( 1st `  z )  /  j ]_ E )
507, 8op1std 6127 . . . . . . . 8  |-  ( z  =  <. x ,  y
>.  ->  ( 1st `  z
)  =  x )
5150csbeq1d 3056 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  [_ ( 1st `  z
)  /  j ]_ E  =  [_ x  / 
j ]_ E )
5251csbeq2dv 3075 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  [_ y  /  k ]_ [_ ( 1st `  z
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ x  / 
j ]_ E )
5349, 52eqtrd 2203 . . . . 5  |-  ( z  =  <. x ,  y
>.  ->  [_ ( 2nd `  z
)  /  k ]_ [_ ( 1st `  z
)  /  j ]_ E  =  [_ y  / 
k ]_ [_ x  / 
j ]_ E )
54 fprodcom2.2 . . . . . 6  |-  ( ph  ->  C  e.  Fin )
55 snfig 6792 . . . . . . . . 9  |-  ( y  e.  _V  ->  { y }  e.  Fin )
5655elv 2734 . . . . . . . 8  |-  { y }  e.  Fin
57 fprodcom2fi.d . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  C )  ->  D  e.  Fin )
5857ralrimiva 2543 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  C  D  e.  Fin )
5933nfel1 2323 . . . . . . . . . 10  |-  F/ k
[_ y  /  k ]_ D  e.  Fin
6036eleq1d 2239 . . . . . . . . . 10  |-  ( k  =  y  ->  ( D  e.  Fin  <->  [_ y  / 
k ]_ D  e.  Fin ) )
6159, 60rspc 2828 . . . . . . . . 9  |-  ( y  e.  C  ->  ( A. k  e.  C  D  e.  Fin  ->  [_ y  /  k ]_ D  e.  Fin ) )
6258, 61mpan9 279 . . . . . . . 8  |-  ( (
ph  /\  y  e.  C )  ->  [_ y  /  k ]_ D  e.  Fin )
63 xpfi 6907 . . . . . . . 8  |-  ( ( { y }  e.  Fin  /\  [_ y  / 
k ]_ D  e.  Fin )  ->  ( { y }  X.  [_ y  /  k ]_ D
)  e.  Fin )
6456, 62, 63sylancr 412 . . . . . . 7  |-  ( (
ph  /\  y  e.  C )  ->  ( { y }  X.  [_ y  /  k ]_ D )  e.  Fin )
6564ralrimiva 2543 . . . . . 6  |-  ( ph  ->  A. y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )  e.  Fin )
66 disjsnxp 6216 . . . . . . 7  |- Disj  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D
)
6766a1i 9 . . . . . 6  |-  ( ph  -> Disj  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )
68 iunfidisj 6923 . . . . . 6  |-  ( ( C  e.  Fin  /\  A. y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )  e.  Fin  /\ Disj  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )  e.  Fin )
6954, 65, 67, 68syl3anc 1233 . . . . 5  |-  ( ph  ->  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )  e.  Fin )
70 reliun 4732 . . . . . . 7  |-  ( Rel  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D )  <->  A. y  e.  C  Rel  ( { y }  X.  [_ y  /  k ]_ D
) )
71 relxp 4720 . . . . . . . 8  |-  Rel  ( { y }  X.  [_ y  /  k ]_ D )
7271a1i 9 . . . . . . 7  |-  ( y  e.  C  ->  Rel  ( { y }  X.  [_ y  /  k ]_ D ) )
7370, 72mprgbir 2528 . . . . . 6  |-  Rel  U_ y  e.  C  ( {
y }  X.  [_ y  /  k ]_ D
)
7473a1i 9 . . . . 5  |-  ( ph  ->  Rel  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )
75 csbeq1 3052 . . . . . . . 8  |-  ( x  =  ( 2nd `  w
)  ->  [_ x  / 
j ]_ E  =  [_ ( 2nd `  w )  /  j ]_ E
)
7675csbeq2dv 3075 . . . . . . 7  |-  ( x  =  ( 2nd `  w
)  ->  [_ ( 1st `  w )  /  k ]_ [_ x  /  j ]_ E  =  [_ ( 1st `  w )  / 
k ]_ [_ ( 2nd `  w )  /  j ]_ E )
7776eleq1d 2239 . . . . . 6  |-  ( x  =  ( 2nd `  w
)  ->  ( [_ ( 1st `  w )  /  k ]_ [_ x  /  j ]_ E  e.  CC  <->  [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E  e.  CC )
)
78 csbeq1 3052 . . . . . . . 8  |-  ( y  =  ( 1st `  w
)  ->  [_ y  / 
k ]_ D  =  [_ ( 1st `  w )  /  k ]_ D
)
79 csbeq1 3052 . . . . . . . . 9  |-  ( y  =  ( 1st `  w
)  ->  [_ y  / 
k ]_ [_ x  / 
j ]_ E  =  [_ ( 1st `  w )  /  k ]_ [_ x  /  j ]_ E
)
8079eleq1d 2239 . . . . . . . 8  |-  ( y  =  ( 1st `  w
)  ->  ( [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC  <->  [_ ( 1st `  w
)  /  k ]_ [_ x  /  j ]_ E  e.  CC )
)
8178, 80raleqbidv 2677 . . . . . . 7  |-  ( y  =  ( 1st `  w
)  ->  ( A. x  e.  [_  y  / 
k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC  <->  A. x  e.  [_  ( 1st `  w )  /  k ]_ D [_ ( 1st `  w
)  /  k ]_ [_ x  /  j ]_ E  e.  CC )
)
82 simpl 108 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  ph )
8333, 36opeliunxp2f 6217 . . . . . . . . . . . . . . 15  |-  ( <.
y ,  x >.  e. 
U_ k  e.  C  ( { k }  X.  D )  <->  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )
8417, 83sylbbr 135 . . . . . . . . . . . . . 14  |-  ( ( y  e.  C  /\  x  e.  [_ y  / 
k ]_ D )  ->  <. x ,  y >.  e.  `' U_ k  e.  C  ( { k }  X.  D ) )
8584adantl 275 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  <. x ,  y >.  e.  `' U_ k  e.  C  ( { k }  X.  D ) )
8622adantr 274 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  U_ j  e.  A  ( { j }  X.  B )  =  `' U_ k  e.  C  ( { k }  X.  D ) )
8785, 86eleqtrrd 2250 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  <. x ,  y >.  e.  U_ j  e.  A  ( { j }  X.  B ) )
88 eliun 3877 . . . . . . . . . . . 12  |-  ( <.
x ,  y >.  e.  U_ j  e.  A  ( { j }  X.  B )  <->  E. j  e.  A  <. x ,  y >.  e.  ( { j }  X.  B ) )
8987, 88sylib 121 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  E. j  e.  A  <. x ,  y >.  e.  ( { j }  X.  B ) )
90 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  <. x ,  y
>.  e.  ( { j }  X.  B ) )
91 opelxp 4641 . . . . . . . . . . . . . . . 16  |-  ( <.
x ,  y >.  e.  ( { j }  X.  B )  <->  ( x  e.  { j }  /\  y  e.  B )
)
9290, 91sylib 121 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  ( x  e. 
{ j }  /\  y  e.  B )
)
9392simpld 111 . . . . . . . . . . . . . 14  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  x  e.  {
j } )
94 elsni 3601 . . . . . . . . . . . . . 14  |-  ( x  e.  { j }  ->  x  =  j )
9593, 94syl 14 . . . . . . . . . . . . 13  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  x  =  j )
96 simpl 108 . . . . . . . . . . . . 13  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  j  e.  A
)
9795, 96eqeltrd 2247 . . . . . . . . . . . 12  |-  ( ( j  e.  A  /\  <.
x ,  y >.  e.  ( { j }  X.  B ) )  ->  x  e.  A
)
9897rexlimiva 2582 . . . . . . . . . . 11  |-  ( E. j  e.  A  <. x ,  y >.  e.  ( { j }  X.  B )  ->  x  e.  A )
9989, 98syl 14 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  x  e.  A )
10025nfcri 2306 . . . . . . . . . . . 12  |-  F/ j  y  e.  [_ x  /  j ]_ B
10194equcomd 1700 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  { j }  ->  j  =  x )
102101, 28syl 14 . . . . . . . . . . . . . . . 16  |-  ( x  e.  { j }  ->  B  =  [_ x  /  j ]_ B
)
103102eleq2d 2240 . . . . . . . . . . . . . . 15  |-  ( x  e.  { j }  ->  ( y  e.  B  <->  y  e.  [_ x  /  j ]_ B
) )
104103biimpa 294 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { j }  /\  y  e.  B )  ->  y  e.  [_ x  /  j ]_ B )
10591, 104sylbi 120 . . . . . . . . . . . . 13  |-  ( <.
x ,  y >.  e.  ( { j }  X.  B )  -> 
y  e.  [_ x  /  j ]_ B
)
106105a1i 9 . . . . . . . . . . . 12  |-  ( j  e.  A  ->  ( <. x ,  y >.  e.  ( { j }  X.  B )  -> 
y  e.  [_ x  /  j ]_ B
) )
107100, 106rexlimi 2580 . . . . . . . . . . 11  |-  ( E. j  e.  A  <. x ,  y >.  e.  ( { j }  X.  B )  ->  y  e.  [_ x  /  j ]_ B )
10889, 107syl 14 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  -> 
y  e.  [_ x  /  j ]_ B
)
109 fprodcom2.5 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  E  e.  CC )
110109ralrimivva 2552 . . . . . . . . . . . . 13  |-  ( ph  ->  A. j  e.  A  A. k  e.  B  E  e.  CC )
111 nfcsb1v 3082 . . . . . . . . . . . . . . . 16  |-  F/_ j [_ x  /  j ]_ E
112111nfel1 2323 . . . . . . . . . . . . . . 15  |-  F/ j
[_ x  /  j ]_ E  e.  CC
11325, 112nfralw 2507 . . . . . . . . . . . . . 14  |-  F/ j A. k  e.  [_  x  /  j ]_ B [_ x  /  j ]_ E  e.  CC
114 csbeq1a 3058 . . . . . . . . . . . . . . . 16  |-  ( j  =  x  ->  E  =  [_ x  /  j ]_ E )
115114eleq1d 2239 . . . . . . . . . . . . . . 15  |-  ( j  =  x  ->  ( E  e.  CC  <->  [_ x  / 
j ]_ E  e.  CC ) )
11628, 115raleqbidv 2677 . . . . . . . . . . . . . 14  |-  ( j  =  x  ->  ( A. k  e.  B  E  e.  CC  <->  A. k  e.  [_  x  /  j ]_ B [_ x  / 
j ]_ E  e.  CC ) )
117113, 116rspc 2828 . . . . . . . . . . . . 13  |-  ( x  e.  A  ->  ( A. j  e.  A  A. k  e.  B  E  e.  CC  ->  A. k  e.  [_  x  /  j ]_ B [_ x  /  j ]_ E  e.  CC ) )
118110, 117mpan9 279 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  A. k  e.  [_  x  /  j ]_ B [_ x  / 
j ]_ E  e.  CC )
119 nfcsb1v 3082 . . . . . . . . . . . . . 14  |-  F/_ k [_ y  /  k ]_ [_ x  /  j ]_ E
120119nfel1 2323 . . . . . . . . . . . . 13  |-  F/ k
[_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC
121 csbeq1a 3058 . . . . . . . . . . . . . 14  |-  ( k  =  y  ->  [_ x  /  j ]_ E  =  [_ y  /  k ]_ [_ x  /  j ]_ E )
122121eleq1d 2239 . . . . . . . . . . . . 13  |-  ( k  =  y  ->  ( [_ x  /  j ]_ E  e.  CC  <->  [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC )
)
123120, 122rspc 2828 . . . . . . . . . . . 12  |-  ( y  e.  [_ x  / 
j ]_ B  ->  ( A. k  e.  [_  x  /  j ]_ B [_ x  /  j ]_ E  e.  CC  ->  [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC ) )
124118, 123syl5com 29 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  [_ x  /  j ]_ B  ->  [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC ) )
125124impr 377 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  [_ x  /  j ]_ B ) )  ->  [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC )
12682, 99, 108, 125syl12anc 1231 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  C  /\  x  e.  [_ y  /  k ]_ D ) )  ->  [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC )
127126ralrimivva 2552 . . . . . . . 8  |-  ( ph  ->  A. y  e.  C  A. x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC )
128127adantr 274 . . . . . . 7  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  A. y  e.  C  A. x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E  e.  CC )
129 simpr 109 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D
) )
130 eliun 3877 . . . . . . . . 9  |-  ( w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D
)  <->  E. y  e.  C  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )
131129, 130sylib 121 . . . . . . . 8  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  E. y  e.  C  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )
132 xp1st 6144 . . . . . . . . . . . 12  |-  ( w  e.  ( { y }  X.  [_ y  /  k ]_ D
)  ->  ( 1st `  w )  e.  {
y } )
133132adantl 275 . . . . . . . . . . 11  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  ( 1st `  w )  e. 
{ y } )
134 elsni 3601 . . . . . . . . . . 11  |-  ( ( 1st `  w )  e.  { y }  ->  ( 1st `  w
)  =  y )
135133, 134syl 14 . . . . . . . . . 10  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  ( 1st `  w )  =  y )
136 simpl 108 . . . . . . . . . 10  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  y  e.  C )
137135, 136eqeltrd 2247 . . . . . . . . 9  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  ( 1st `  w )  e.  C )
138137rexlimiva 2582 . . . . . . . 8  |-  ( E. y  e.  C  w  e.  ( { y }  X.  [_ y  /  k ]_ D
)  ->  ( 1st `  w )  e.  C
)
139131, 138syl 14 . . . . . . 7  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  -> 
( 1st `  w
)  e.  C )
14081, 128, 139rspcdva 2839 . . . . . 6  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  A. x  e.  [_  ( 1st `  w )  / 
k ]_ D [_ ( 1st `  w )  / 
k ]_ [_ x  / 
j ]_ E  e.  CC )
141 xp2nd 6145 . . . . . . . . . 10  |-  ( w  e.  ( { y }  X.  [_ y  /  k ]_ D
)  ->  ( 2nd `  w )  e.  [_ y  /  k ]_ D
)
142141adantl 275 . . . . . . . . 9  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  ( 2nd `  w )  e. 
[_ y  /  k ]_ D )
143135csbeq1d 3056 . . . . . . . . 9  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  [_ ( 1st `  w )  / 
k ]_ D  =  [_ y  /  k ]_ D
)
144142, 143eleqtrrd 2250 . . . . . . . 8  |-  ( ( y  e.  C  /\  w  e.  ( {
y }  X.  [_ y  /  k ]_ D
) )  ->  ( 2nd `  w )  e. 
[_ ( 1st `  w
)  /  k ]_ D )
145144rexlimiva 2582 . . . . . . 7  |-  ( E. y  e.  C  w  e.  ( { y }  X.  [_ y  /  k ]_ D
)  ->  ( 2nd `  w )  e.  [_ ( 1st `  w )  /  k ]_ D
)
146131, 145syl 14 . . . . . 6  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  -> 
( 2nd `  w
)  e.  [_ ( 1st `  w )  / 
k ]_ D )
14777, 140, 146rspcdva 2839 . . . . 5  |-  ( (
ph  /\  w  e.  U_ y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) )  ->  [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E  e.  CC )
14847, 53, 69, 74, 147fprodcnv 11588 . . . 4  |-  ( ph  ->  prod_ w  e.  U_  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D ) [_ ( 1st `  w )  / 
k ]_ [_ ( 2nd `  w )  /  j ]_ E  =  prod_ z  e.  `'  U_ y  e.  C  ( {
y }  X.  [_ y  /  k ]_ D
) [_ ( 2nd `  z
)  /  k ]_ [_ ( 1st `  z
)  /  j ]_ E )
14941, 148eqtr4d 2206 . . 3  |-  ( ph  ->  prod_ z  e.  U_  x  e.  A  ( { x }  X.  [_ x  /  j ]_ B ) [_ ( 2nd `  z )  / 
k ]_ [_ ( 1st `  z )  /  j ]_ E  =  prod_ w  e.  U_  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D
) [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E )
150 fprodcom2.1 . . . 4  |-  ( ph  ->  A  e.  Fin )
151 fprodcom2.3 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  Fin )
152151ralrimiva 2543 . . . . 5  |-  ( ph  ->  A. j  e.  A  B  e.  Fin )
15325nfel1 2323 . . . . . 6  |-  F/ j
[_ x  /  j ]_ B  e.  Fin
15428eleq1d 2239 . . . . . 6  |-  ( j  =  x  ->  ( B  e.  Fin  <->  [_ x  / 
j ]_ B  e.  Fin ) )
155153, 154rspc 2828 . . . . 5  |-  ( x  e.  A  ->  ( A. j  e.  A  B  e.  Fin  ->  [_ x  /  j ]_ B  e.  Fin ) )
156152, 155mpan9 279 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  [_ x  /  j ]_ B  e.  Fin )
15753, 150, 156, 125fprod2d 11586 . . 3  |-  ( ph  ->  prod_ x  e.  A  prod_ y  e.  [_  x  /  j ]_ B [_ y  /  k ]_ [_ x  /  j ]_ E  =  prod_ z  e.  U_  x  e.  A  ( { x }  X.  [_ x  / 
j ]_ B ) [_ ( 2nd `  z )  /  k ]_ [_ ( 1st `  z )  / 
j ]_ E )
15847, 54, 62, 126fprod2d 11586 . . 3  |-  ( ph  ->  prod_ y  e.  C  prod_ x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E  =  prod_ w  e.  U_  y  e.  C  ( { y }  X.  [_ y  /  k ]_ D
) [_ ( 1st `  w
)  /  k ]_ [_ ( 2nd `  w
)  /  j ]_ E )
159149, 157, 1583eqtr4d 2213 . 2  |-  ( ph  ->  prod_ x  e.  A  prod_ y  e.  [_  x  /  j ]_ B [_ y  /  k ]_ [_ x  /  j ]_ E  =  prod_ y  e.  C  prod_ x  e.  [_  y  /  k ]_ D [_ y  / 
k ]_ [_ x  / 
j ]_ E )
160 nfcv 2312 . . 3  |-  F/_ x prod_ k  e.  B  E
161 nfcv 2312 . . . . 5  |-  F/_ j
y
162161, 111nfcsbw 3085 . . . 4  |-  F/_ j [_ y  /  k ]_ [_ x  /  j ]_ E
16325, 162nfcprod 11518 . . 3  |-  F/_ j prod_ y  e.  [_  x  /  j ]_ B [_ y  /  k ]_ [_ x  /  j ]_ E
164 nfcv 2312 . . . . 5  |-  F/_ y E
165 nfcsb1v 3082 . . . . 5  |-  F/_ k [_ y  /  k ]_ E
166 csbeq1a 3058 . . . . 5  |-  ( k  =  y  ->  E  =  [_ y  /  k ]_ E )
167164, 165, 166cbvprodi 11523 . . . 4  |-  prod_ k  e.  B  E  =  prod_ y  e.  B  [_ y  /  k ]_ E
168114csbeq2dv 3075 . . . . . 6  |-  ( j  =  x  ->  [_ y  /  k ]_ E  =  [_ y  /  k ]_ [_ x  /  j ]_ E )
169168adantr 274 . . . . 5  |-  ( ( j  =  x  /\  y  e.  B )  ->  [_ y  /  k ]_ E  =  [_ y  /  k ]_ [_ x  /  j ]_ E
)
17028, 169prodeq12dv 11532 . . . 4  |-  ( j  =  x  ->  prod_ y  e.  B  [_ y  /  k ]_ E  =  prod_ y  e.  [_  x  /  j ]_ B [_ y  /  k ]_ [_ x  /  j ]_ E )
171167, 170eqtrid 2215 . . 3  |-  ( j  =  x  ->  prod_ k  e.  B  E  = 
prod_ y  e.  [_  x  /  j ]_ B [_ y  /  k ]_ [_ x  /  j ]_ E )
172160, 163, 171cbvprodi 11523 . 2  |-  prod_ j  e.  A  prod_ k  e.  B  E  =  prod_ x  e.  A  prod_ y  e.  [_  x  /  j ]_ B [_ y  / 
k ]_ [_ x  / 
j ]_ E
173 nfcv 2312 . . 3  |-  F/_ y prod_ j  e.  D  E
17433, 119nfcprod 11518 . . 3  |-  F/_ k prod_ x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E
175 nfcv 2312 . . . . 5  |-  F/_ x E
176175, 111, 114cbvprodi 11523 . . . 4  |-  prod_ j  e.  D  E  =  prod_ x  e.  D  [_ x  /  j ]_ E
177121adantr 274 . . . . 5  |-  ( ( k  =  y  /\  x  e.  D )  ->  [_ x  /  j ]_ E  =  [_ y  /  k ]_ [_ x  /  j ]_ E
)
17836, 177prodeq12dv 11532 . . . 4  |-  ( k  =  y  ->  prod_ x  e.  D  [_ x  /  j ]_ E  =  prod_ x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E )
179176, 178eqtrid 2215 . . 3  |-  ( k  =  y  ->  prod_ j  e.  D  E  = 
prod_ x  e.  [_  y  /  k ]_ D [_ y  /  k ]_ [_ x  /  j ]_ E )
180173, 174, 179cbvprodi 11523 . 2  |-  prod_ k  e.  C  prod_ j  e.  D  E  =  prod_ y  e.  C  prod_ x  e.  [_  y  /  k ]_ D [_ y  / 
k ]_ [_ x  / 
j ]_ E
181159, 172, 1803eqtr4g 2228 1  |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  E  =  prod_ k  e.  C  prod_ j  e.  D  E
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1348   E.wex 1485    e. wcel 2141   A.wral 2448   E.wrex 2449   _Vcvv 2730   [_csb 3049   {csn 3583   <.cop 3586   U_ciun 3873  Disj wdisj 3966    X. cxp 4609   `'ccnv 4610   Rel wrel 4616   ` cfv 5198   1stc1st 6117   2ndc2nd 6118   Fincfn 6718   CCcc 7772   prod_cprod 11513
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-disj 3967  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-frec 6370  df-1o 6395  df-oadd 6399  df-er 6513  df-en 6719  df-dom 6720  df-fin 6721  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-q 9579  df-rp 9611  df-fz 9966  df-fzo 10099  df-seqfrec 10402  df-exp 10476  df-ihash 10710  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963  df-clim 11242  df-proddc 11514
This theorem is referenced by:  fprodcom  11590  fprod0diagfz  11591
  Copyright terms: Public domain W3C validator