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

Definition df-smat 25600
Description: Matrix left scalar multiplication. Meaningful if  g is a binary external operation. Experimental. (Contributed by FL, 29-Aug-2010.)
Assertion
Ref Expression
df-smat  |-  x m  =  ( g  e. 
_V  |->  { <. <. m ,  a >. ,  o
>.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) ) } )
Distinct variable group:    g, m, a, o, j, k, x, y

Detailed syntax breakdown of Definition df-smat
StepHypRef Expression
1 csmat 25597 . 2  class  x m
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
4 c1 8754 . . . . . . . . . 10  class  1
5 vj . . . . . . . . . . 11  set  j
65cv 1631 . . . . . . . . . 10  class  j
7 cfz 10798 . . . . . . . . . 10  class  ...
84, 6, 7co 5874 . . . . . . . . 9  class  ( 1 ... j )
9 vk . . . . . . . . . . 11  set  k
109cv 1631 . . . . . . . . . 10  class  k
114, 10, 7co 5874 . . . . . . . . 9  class  ( 1 ... k )
128, 11cxp 4703 . . . . . . . 8  class  ( ( 1 ... j )  X.  ( 1 ... k ) )
132cv 1631 . . . . . . . . . 10  class  g
1413cdm 4705 . . . . . . . . 9  class  dom  g
1514crn 4706 . . . . . . . 8  class  ran  dom  g
16 vm . . . . . . . . 9  set  m
1716cv 1631 . . . . . . . 8  class  m
1812, 15, 17wf 5267 . . . . . . 7  wff  m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g
19 va . . . . . . . . 9  set  a
2019cv 1631 . . . . . . . 8  class  a
2114cdm 4705 . . . . . . . 8  class  dom  dom  g
2220, 21wcel 1696 . . . . . . 7  wff  a  e. 
dom  dom  g
23 vo . . . . . . . . 9  set  o
2423cv 1631 . . . . . . . 8  class  o
25 vx . . . . . . . . 9  set  x
26 vy . . . . . . . . 9  set  y
2725cv 1631 . . . . . . . . . . . 12  class  x
2826cv 1631 . . . . . . . . . . . 12  class  y
2927, 28cop 3656 . . . . . . . . . . 11  class  <. x ,  y >.
3029, 17cfv 5271 . . . . . . . . . 10  class  ( m `
 <. x ,  y
>. )
3120, 30, 13co 5874 . . . . . . . . 9  class  ( a g ( m `  <. x ,  y >.
) )
3225, 26, 8, 11, 31cmpt2 5876 . . . . . . . 8  class  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `  <. x ,  y >.
) ) )
3324, 32wceq 1632 . . . . . . 7  wff  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k ) 
|->  ( a g ( m `  <. x ,  y >. )
) )
3418, 22, 33w3a 934 . . . . . 6  wff  ( m : ( ( 1 ... j )  X.  ( 1 ... k
) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k ) 
|->  ( a g ( m `  <. x ,  y >. )
) ) )
35 cn 9762 . . . . . 6  class  NN
3634, 9, 35wrex 2557 . . . . 5  wff  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) )
3736, 5, 35wrex 2557 . . . 4  wff  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) )
3837, 16, 19, 23coprab 5875 . . 3  class  { <. <.
m ,  a >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) ) }
392, 3, 38cmpt 4093 . 2  class  ( g  e.  _V  |->  { <. <.
m ,  a >. ,  o >.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) ) } )
401, 39wceq 1632 1  wff  x m  =  ( g  e. 
_V  |->  { <. <. m ,  a >. ,  o
>.  |  E. j  e.  NN  E. k  e.  NN  ( m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g  /\  a  e.  dom  dom  g  /\  o  =  (
x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `
 <. x ,  y
>. ) ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator