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

Definition df-amat 25496
Description: Matrix addition. Meaningful if  g is a  Magma (a binary internal operation) at least. Experimental. (Contributed by FL, 29-Aug-2010.)
Assertion
Ref Expression
df-amat  |-  + m  =  ( g  e. 
_V  |->  { <. <. m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  (
m : ( ( 1 ... j )  X.  ( 1 ... k ) ) --> dom 
dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) ) } )
Distinct variable group:    g, m, n, o, j, k, x, y

Detailed syntax breakdown of Definition df-amat
StepHypRef Expression
1 cmmat 25493 . 2  class  + m
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
4 c1 8738 . . . . . . . . . 10  class  1
5 vj . . . . . . . . . . 11  set  j
65cv 1622 . . . . . . . . . 10  class  j
7 cfz 10782 . . . . . . . . . 10  class  ...
84, 6, 7co 5858 . . . . . . . . 9  class  ( 1 ... j )
9 vk . . . . . . . . . . 11  set  k
109cv 1622 . . . . . . . . . 10  class  k
114, 10, 7co 5858 . . . . . . . . 9  class  ( 1 ... k )
128, 11cxp 4687 . . . . . . . 8  class  ( ( 1 ... j )  X.  ( 1 ... k ) )
132cv 1622 . . . . . . . . . 10  class  g
1413cdm 4689 . . . . . . . . 9  class  dom  g
1514cdm 4689 . . . . . . . 8  class  dom  dom  g
16 vm . . . . . . . . 9  set  m
1716cv 1622 . . . . . . . 8  class  m
1812, 15, 17wf 5251 . . . . . . 7  wff  m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g
19 vn . . . . . . . . 9  set  n
2019cv 1622 . . . . . . . 8  class  n
2112, 15, 20wf 5251 . . . . . . 7  wff  n : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g
22 vo . . . . . . . . 9  set  o
2322cv 1622 . . . . . . . 8  class  o
24 vx . . . . . . . . 9  set  x
25 vy . . . . . . . . 9  set  y
2624cv 1622 . . . . . . . . . . . 12  class  x
2725cv 1622 . . . . . . . . . . . 12  class  y
2826, 27cop 3643 . . . . . . . . . . 11  class  <. x ,  y >.
2928, 17cfv 5255 . . . . . . . . . 10  class  ( m `
 <. x ,  y
>. )
3028, 20cfv 5255 . . . . . . . . . 10  class  ( n `
 <. x ,  y
>. )
3129, 30, 13co 5858 . . . . . . . . 9  class  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) )
3224, 25, 8, 11, 31cmpt2 5860 . . . . . . . 8  class  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) )
3323, 32wceq 1623 . . . . . . 7  wff  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k ) 
|->  ( ( m `  <. x ,  y >.
) g ( n `
 <. x ,  y
>. ) ) )
3418, 21, 33w3a 934 . . . . . 6  wff  ( m : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  n : ( ( 1 ... j
)  X.  ( 1 ... k ) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j
) ,  y  e.  ( 1 ... k
)  |->  ( ( m `
 <. x ,  y
>. ) g ( n `
 <. x ,  y
>. ) ) ) )
35 cn 9746 . . . . . 6  class  NN
3634, 9, 35wrex 2544 . . . . 5  wff  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) )
3736, 5, 35wrex 2544 . . . 4  wff  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) )
3837, 16, 19, 22coprab 5859 . . 3  class  { <. <.
m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) ) }
392, 3, 38cmpt 4077 . 2  class  ( g  e.  _V  |->  { <. <.
m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> dom  dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) ) } )
401, 39wceq 1623 1  wff  + m  =  ( g  e. 
_V  |->  { <. <. m ,  n >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  (
m : ( ( 1 ... j )  X.  ( 1 ... k ) ) --> dom 
dom  g  /\  n : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( ( m `  <. x ,  y >. )
g ( n `  <. x ,  y >.
) ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator