HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-lnfn Unicode version

Definition df-lnfn 22258
Description: Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-lnfn  |-  LinFn  =  {
t  e.  ( CC 
^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  x.  (
t `  y )
)  +  ( t `
 z ) ) }
Distinct variable group:    x, t, y, z

Detailed syntax breakdown of Definition df-lnfn
StepHypRef Expression
1 clf 21364 . 2  class  LinFn
2 vx . . . . . . . . . . 11  set  x
32cv 1618 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  set  y
54cv 1618 . . . . . . . . . 10  class  y
6 csm 21331 . . . . . . . . . 10  class  .h
73, 5, 6co 5710 . . . . . . . . 9  class  ( x  .h  y )
8 vz . . . . . . . . . 10  set  z
98cv 1618 . . . . . . . . 9  class  z
10 cva 21330 . . . . . . . . 9  class  +h
117, 9, 10co 5710 . . . . . . . 8  class  ( ( x  .h  y )  +h  z )
12 vt . . . . . . . . 9  set  t
1312cv 1618 . . . . . . . 8  class  t
1411, 13cfv 4592 . . . . . . 7  class  ( t `
 ( ( x  .h  y )  +h  z ) )
155, 13cfv 4592 . . . . . . . . 9  class  ( t `
 y )
16 cmul 8622 . . . . . . . . 9  class  x.
173, 15, 16co 5710 . . . . . . . 8  class  ( x  x.  ( t `  y ) )
189, 13cfv 4592 . . . . . . . 8  class  ( t `
 z )
19 caddc 8620 . . . . . . . 8  class  +
2017, 18, 19co 5710 . . . . . . 7  class  ( ( x  x.  ( t `
 y ) )  +  ( t `  z ) )
2114, 20wceq 1619 . . . . . 6  wff  ( t `
 ( ( x  .h  y )  +h  z ) )  =  ( ( x  x.  ( t `  y
) )  +  ( t `  z ) )
22 chil 21329 . . . . . 6  class  ~H
2321, 8, 22wral 2509 . . . . 5  wff  A. z  e.  ~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  x.  (
t `  y )
)  +  ( t `
 z ) )
2423, 4, 22wral 2509 . . . 4  wff  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  x.  (
t `  y )
)  +  ( t `
 z ) )
25 cc 8615 . . . 4  class  CC
2624, 2, 25wral 2509 . . 3  wff  A. x  e.  CC  A. y  e. 
~H  A. z  e.  ~H  ( t `  (
( x  .h  y
)  +h  z ) )  =  ( ( x  x.  ( t `
 y ) )  +  ( t `  z ) )
27 cmap 6658 . . . 4  class  ^m
2825, 22, 27co 5710 . . 3  class  ( CC 
^m  ~H )
2926, 12, 28crab 2512 . 2  class  { t  e.  ( CC  ^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  x.  (
t `  y )
)  +  ( t `
 z ) ) }
301, 29wceq 1619 1  wff  LinFn  =  {
t  e.  ( CC 
^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  x.  (
t `  y )
)  +  ( t `
 z ) ) }
Colors of variables: wff set class
This definition is referenced by:  ellnfn  22293
  Copyright terms: Public domain W3C validator