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 25497
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 25494 . 2  class  x 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
1514crn 4690 . . . . . . . 8  class  ran  dom  g
16 vm . . . . . . . . 9  set  m
1716cv 1622 . . . . . . . 8  class  m
1812, 15, 17wf 5251 . . . . . . 7  wff  m : ( ( 1 ... j )  X.  (
1 ... k ) ) --> ran  dom  g
19 va . . . . . . . . 9  set  a
2019cv 1622 . . . . . . . 8  class  a
2114cdm 4689 . . . . . . . 8  class  dom  dom  g
2220, 21wcel 1684 . . . . . . 7  wff  a  e. 
dom  dom  g
23 vo . . . . . . . . 9  set  o
2423cv 1622 . . . . . . . 8  class  o
25 vx . . . . . . . . 9  set  x
26 vy . . . . . . . . 9  set  y
2725cv 1622 . . . . . . . . . . . 12  class  x
2826cv 1622 . . . . . . . . . . . 12  class  y
2927, 28cop 3643 . . . . . . . . . . 11  class  <. x ,  y >.
3029, 17cfv 5255 . . . . . . . . . 10  class  ( m `
 <. x ,  y
>. )
3120, 30, 13co 5858 . . . . . . . . 9  class  ( a g ( m `  <. x ,  y >.
) )
3225, 26, 8, 11, 31cmpt2 5860 . . . . . . . 8  class  ( x  e.  ( 1 ... j ) ,  y  e.  ( 1 ... k )  |->  ( a g ( m `  <. x ,  y >.
) ) )
3324, 32wceq 1623 . . . . . . 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 9746 . . . . . 6  class  NN
3634, 9, 35wrex 2544 . . . . 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 2544 . . . 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 5859 . . 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 4077 . 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 1623 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