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

Definition df-lno 21322
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 ( .s
OLD `  u )
y ) ( +v
`  u ) z ) )  =  ( ( x ( .s
OLD `  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 21318 . 2  class  LnOp
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21140 . . 3  class  NrmCVec
5 vx . . . . . . . . . . . 12  set  x
65cv 1622 . . . . . . . . . . 11  class  x
7 vy . . . . . . . . . . . 12  set  y
87cv 1622 . . . . . . . . . . 11  class  y
92cv 1622 . . . . . . . . . . . 12  class  u
10 cns 21143 . . . . . . . . . . . 12  class  .s OLD
119, 10cfv 5255 . . . . . . . . . . 11  class  ( .s
OLD `  u )
126, 8, 11co 5858 . . . . . . . . . 10  class  ( x ( .s OLD `  u
) y )
13 vz . . . . . . . . . . 11  set  z
1413cv 1622 . . . . . . . . . 10  class  z
15 cpv 21141 . . . . . . . . . . 11  class  +v
169, 15cfv 5255 . . . . . . . . . 10  class  ( +v
`  u )
1712, 14, 16co 5858 . . . . . . . . 9  class  ( ( x ( .s OLD `  u ) y ) ( +v `  u
) z )
18 vt . . . . . . . . . 10  set  t
1918cv 1622 . . . . . . . . 9  class  t
2017, 19cfv 5255 . . . . . . . 8  class  ( t `
 ( ( x ( .s OLD `  u
) y ) ( +v `  u ) z ) )
218, 19cfv 5255 . . . . . . . . . 10  class  ( t `
 y )
223cv 1622 . . . . . . . . . . 11  class  w
2322, 10cfv 5255 . . . . . . . . . 10  class  ( .s
OLD `  w )
246, 21, 23co 5858 . . . . . . . . 9  class  ( x ( .s OLD `  w
) ( t `  y ) )
2514, 19cfv 5255 . . . . . . . . 9  class  ( t `
 z )
2622, 15cfv 5255 . . . . . . . . 9  class  ( +v
`  w )
2724, 25, 26co 5858 . . . . . . . 8  class  ( ( x ( .s OLD `  w ) ( t `
 y ) ) ( +v `  w
) ( t `  z ) )
2820, 27wceq 1623 . . . . . . 7  wff  ( t `
 ( ( x ( .s OLD `  u
) y ) ( +v `  u ) z ) )  =  ( ( x ( .s OLD `  w
) ( t `  y ) ) ( +v `  w ) ( t `  z
) )
29 cba 21142 . . . . . . . 8  class  BaseSet
309, 29cfv 5255 . . . . . . 7  class  ( BaseSet `  u )
3128, 13, 30wral 2543 . . . . . 6  wff  A. z  e.  ( BaseSet `  u )
( t `  (
( x ( .s
OLD `  u )
y ) ( +v
`  u ) z ) )  =  ( ( x ( .s
OLD `  w )
( t `  y
) ) ( +v
`  w ) ( t `  z ) )
3231, 7, 30wral 2543 . . . . 5  wff  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .s OLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .s OLD `  w
) ( t `  y ) ) ( +v `  w ) ( t `  z
) )
33 cc 8735 . . . . 5  class  CC
3432, 5, 33wral 2543 . . . 4  wff  A. x  e.  CC  A. y  e.  ( BaseSet `  u ) A. z  e.  ( BaseSet
`  u ) ( t `  ( ( x ( .s OLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .s OLD `  w
) ( t `  y ) ) ( +v `  w ) ( t `  z
) )
3522, 29cfv 5255 . . . . 5  class  ( BaseSet `  w )
36 cmap 6772 . . . . 5  class  ^m
3735, 30, 36co 5858 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
3834, 18, 37crab 2547 . . 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 ( .s OLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .s OLD `  w
) ( t `  y ) ) ( +v `  w ) ( t `  z
) ) }
392, 3, 4, 4, 38cmpt2 5860 . 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 ( .s OLD `  u ) y ) ( +v `  u
) z ) )  =  ( ( x ( .s OLD `  w
) ( t `  y ) ) ( +v `  w ) ( t `  z
) ) } )
401, 39wceq 1623 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 ( .s
OLD `  u )
y ) ( +v
`  u ) z ) )  =  ( ( x ( .s
OLD `  w )
( t `  y
) ) ( +v
`  w ) ( t `  z ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lnoval  21330
  Copyright terms: Public domain W3C validator