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

Definition df-sh 21711
Description: Define the set of subspaces of a Hilbert space. See issh 21712 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-sh  |-  SH  =  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
) }

Detailed syntax breakdown of Definition df-sh
StepHypRef Expression
1 csh 21433 . 2  class  SH
2 c0v 21429 . . . . 5  class  0h
3 vh . . . . . 6  set  h
43cv 1618 . . . . 5  class  h
52, 4wcel 1621 . . . 4  wff  0h  e.  h
6 cva 21425 . . . . . 6  class  +h
74, 4cxp 4624 . . . . . 6  class  ( h  X.  h )
86, 7cima 4629 . . . . 5  class  (  +h  " ( h  X.  h ) )
98, 4wss 3094 . . . 4  wff  (  +h  " ( h  X.  h ) )  C_  h
10 csm 21426 . . . . . 6  class  .h
11 cc 8668 . . . . . . 7  class  CC
1211, 4cxp 4624 . . . . . 6  class  ( CC 
X.  h )
1310, 12cima 4629 . . . . 5  class  (  .h  " ( CC  X.  h ) )
1413, 4wss 3094 . . . 4  wff  (  .h  " ( CC  X.  h ) )  C_  h
155, 9, 14w3a 939 . . 3  wff  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
)
16 chil 21424 . . . 4  class  ~H
1716cpw 3566 . . 3  class  ~P ~H
1815, 3, 17crab 2519 . 2  class  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) ) 
C_  h  /\  (  .h  " ( CC  X.  h ) )  C_  h ) }
191, 18wceq 1619 1  wff  SH  =  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
) }
Colors of variables: wff set class
This definition is referenced by:  issh  21712
  Copyright terms: Public domain W3C validator