MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lno Structured version   Unicode version

Definition df-lno 24144
Description: Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e. the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-lno  |-  LnOp  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { t  e.  ( ( BaseSet `  w
)  ^m  ( BaseSet `  u ) )  | 
A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet `  u )
( t `  (
( x ( .sOLD `  u ) y ) ( +v
`  u ) z ) )  =  ( ( x ( .sOLD `  w ) ( t `  y
) ) ( +v
`  w ) ( t `  z ) ) } )
Distinct variable group:    u, t, w, x, y, z

Detailed syntax breakdown of Definition df-lno
StepHypRef Expression
1 clno 24140 . 2  class  LnOp
2 vu . . 3  setvar  u
3 vw . . 3  setvar  w
4 cnv 23962 . . 3  class  NrmCVec
5 vx . . . . . . . . . . . 12  setvar  x
65cv 1368 . . . . . . . . . . 11  class  x
7 vy . . . . . . . . . . . 12  setvar  y
87cv 1368 . . . . . . . . . . 11  class  y
92cv 1368 . . . . . . . . . . . 12  class  u
10 cns 23965 . . . . . . . . . . . 12  class  .sOLD
119, 10cfv 5418 . . . . . . . . . . 11  class  ( .sOLD `  u )
126, 8, 11co 6091 . . . . . . . . . 10  class  ( x ( .sOLD `  u ) y )
13 vz . . . . . . . . . . 11  setvar  z
1413cv 1368 . . . . . . . . . 10  class  z
15 cpv 23963 . . . . . . . . . . 11  class  +v
169, 15cfv 5418 . . . . . . . . . 10  class  ( +v
`  u )
1712, 14, 16co 6091 . . . . . . . . 9  class  ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z )
18 vt . . . . . . . . . 10  setvar  t
1918cv 1368 . . . . . . . . 9  class  t
2017, 19cfv 5418 . . . . . . . 8  class  ( t `
 ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )
218, 19cfv 5418 . . . . . . . . . 10  class  ( t `
 y )
223cv 1368 . . . . . . . . . . 11  class  w
2322, 10cfv 5418 . . . . . . . . . 10  class  ( .sOLD `  w )
246, 21, 23co 6091 . . . . . . . . 9  class  ( x ( .sOLD `  w ) ( t `
 y ) )
2514, 19cfv 5418 . . . . . . . . 9  class  ( t `
 z )
2622, 15cfv 5418 . . . . . . . . 9  class  ( +v
`  w )
2724, 25, 26co 6091 . . . . . . . 8  class  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) )
2820, 27wceq 1369 . . . . . . 7  wff  ( t `
 ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) )
29 cba 23964 . . . . . . . 8  class  BaseSet
309, 29cfv 5418 . . . . . . 7  class  ( BaseSet `  u )
3128, 13, 30wral 2715 . . . . . 6  wff  A. z  e.  ( BaseSet `  u )
( t `  (
( x ( .sOLD `  u ) y ) ( +v
`  u ) z ) )  =  ( ( x ( .sOLD `  w ) ( t `  y
) ) ( +v
`  w ) ( t `  z ) )
3231, 7, 30wral 2715 . . . . 5  wff  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) )
33 cc 9280 . . . . 5  class  CC
3432, 5, 33wral 2715 . . . 4  wff  A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) )
3522, 29cfv 5418 . . . . 5  class  ( BaseSet `  w )
36 cmap 7214 . . . . 5  class  ^m
3735, 30, 36co 6091 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
3834, 18, 37crab 2719 . . 3  class  { t  e.  ( ( BaseSet `  w )  ^m  ( BaseSet
`  u ) )  |  A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) ) }
392, 3, 4, 4, 38cmpt2 6093 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  { t  e.  ( ( BaseSet `  w )  ^m  ( BaseSet `  u )
)  |  A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .sOLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .sOLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) ) } )
401, 39wceq 1369 1  wff  LnOp  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { t  e.  ( ( BaseSet `  w
)  ^m  ( BaseSet `  u ) )  | 
A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet `  u )
( t `  (
( x ( .sOLD `  u ) y ) ( +v
`  u ) z ) )  =  ( ( x ( .sOLD `  w ) ( t `  y
) ) ( +v
`  w ) ( t `  z ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  lnoval  24152
  Copyright terms: Public domain W3C validator