Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mmat Unicode version

Definition df-mmat 25498
Description: Matrix multiplication. Meaningful if  <. g ,  h >. is a ring at least.  prod_ here should be 
sum_ (to be traditional). But in set.mm  sum_ is  CC oriented and has a limit definition embedded and thus doesn't fit the needs of this generic definition. Experimental. (Contributed by FL, 29-Aug-2010.)
Assertion
Ref Expression
df-mmat  |-  x m  =  ( g  e. 
_V ,  h  e. 
_V  |->  { <. <. m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  E. l  e.  NN  (
m : ( ( 1 ... j )  X.  ( 1 ... k ) ) --> dom 
dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) ) } )
Distinct variable group:    g, h, m, n, o, j, k, l, x, y, z

Detailed syntax breakdown of Definition df-mmat
StepHypRef Expression
1 cxmat 25495 . 2  class  x m
2 vg . . 3  set  g
3 vh . . 3  set  h
4 cvv 2788 . . 3  class  _V
5 c1 8738 . . . . . . . . . . 11  class  1
6 vj . . . . . . . . . . . 12  set  j
76cv 1622 . . . . . . . . . . 11  class  j
8 cfz 10782 . . . . . . . . . . 11  class  ...
95, 7, 8co 5858 . . . . . . . . . 10  class  ( 1 ... j )
10 vk . . . . . . . . . . . 12  set  k
1110cv 1622 . . . . . . . . . . 11  class  k
125, 11, 8co 5858 . . . . . . . . . 10  class  ( 1 ... k )
139, 12cxp 4687 . . . . . . . . 9  class  ( ( 1 ... j )  X.  ( 1 ... k ) )
142cv 1622 . . . . . . . . . . 11  class  g
1514cdm 4689 . . . . . . . . . 10  class  dom  g
1615cdm 4689 . . . . . . . . 9  class  dom  dom  g
17 vm . . . . . . . . . 10  set  m
1817cv 1622 . . . . . . . . 9  class  m
1913, 16, 18wf 5251 . . . . . . . 8  wff  m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g
20 vl . . . . . . . . . . . 12  set  l
2120cv 1622 . . . . . . . . . . 11  class  l
225, 21, 8co 5858 . . . . . . . . . 10  class  ( 1 ... l )
2312, 22cxp 4687 . . . . . . . . 9  class  ( ( 1 ... k )  X.  ( 1 ... l ) )
24 vn . . . . . . . . . 10  set  n
2524cv 1622 . . . . . . . . 9  class  n
2623, 16, 25wf 5251 . . . . . . . 8  wff  n : ( ( 1 ... k )  X.  (
1 ... l ) ) --> dom  dom  g
27 vo . . . . . . . . . 10  set  o
2827cv 1622 . . . . . . . . 9  class  o
29 vx . . . . . . . . . 10  set  x
30 vy . . . . . . . . . 10  set  y
3129cv 1622 . . . . . . . . . . . . . 14  class  x
32 vz . . . . . . . . . . . . . . 15  set  z
3332cv 1622 . . . . . . . . . . . . . 14  class  z
3431, 33cop 3643 . . . . . . . . . . . . 13  class  <. x ,  z >.
3534, 18cfv 5255 . . . . . . . . . . . 12  class  ( m `
 <. x ,  z
>. )
3630cv 1622 . . . . . . . . . . . . . 14  class  y
3733, 36cop 3643 . . . . . . . . . . . . 13  class  <. z ,  y >.
3837, 25cfv 5255 . . . . . . . . . . . 12  class  ( n `
 <. z ,  y
>. )
393cv 1622 . . . . . . . . . . . 12  class  h
4035, 38, 39co 5858 . . . . . . . . . . 11  class  ( ( m `  <. x ,  z >. )
h ( n `  <. z ,  y >.
) )
4112, 40, 32, 14cprd 25298 . . . . . . . . . 10  class  prod_ z  e.  ( 1 ... k
) g ( ( m `  <. x ,  z >. )
h ( n `  <. z ,  y >.
) )
4229, 30, 9, 22, 41cmpt2 5860 . . . . . . . . 9  class  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_ z  e.  ( 1 ... k
) g ( ( m `  <. x ,  z >. )
h ( n `  <. z ,  y >.
) ) )
4328, 42wceq 1623 . . . . . . . 8  wff  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l ) 
|->  prod_ z  e.  ( 1 ... k ) g ( ( m `
 <. x ,  z
>. ) h ( n `
 <. z ,  y
>. ) ) )
4419, 26, 43w3a 934 . . . . . . 7  wff  ( m : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  n : ( ( 1 ... k
)  X.  ( 1 ... l ) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j
) ,  y  e.  ( 1 ... l
)  |->  prod_ z  e.  ( 1 ... k ) g ( ( m `
 <. x ,  z
>. ) h ( n `
 <. z ,  y
>. ) ) ) )
45 cn 9746 . . . . . . 7  class  NN
4644, 20, 45wrex 2544 . . . . . 6  wff  E. l  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) )
4746, 10, 45wrex 2544 . . . . 5  wff  E. k  e.  NN  E. l  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) )
4847, 6, 45wrex 2544 . . . 4  wff  E. j  e.  NN  E. k  e.  NN  E. l  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) )
4948, 17, 24, 27coprab 5859 . . 3  class  { <. <.
m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  E. l  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) ) }
502, 3, 4, 4, 49cmpt2 5860 . 2  class  ( g  e.  _V ,  h  e.  _V  |->  { <. <. m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  E. l  e.  NN  (
m : ( ( 1 ... j )  X.  ( 1 ... k ) ) --> dom 
dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) ) } )
511, 50wceq 1623 1  wff  x m  =  ( g  e. 
_V ,  h  e. 
_V  |->  { <. <. m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  E. l  e.  NN  (
m : ( ( 1 ... j )  X.  ( 1 ... k ) ) --> dom 
dom  g  /\  n : ( ( 1 ... k )  X.  ( 1 ... l
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... l )  |->  prod_
z  e.  ( 1 ... k ) g ( ( m `  <. x ,  z >.
) h ( n `
 <. z ,  y
>. ) ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator