HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-sh Structured version   Visualization version   GIF version
Definition df-sh 30438
Description: Define the set of subspaces of a Hilbert space. See issh 30439 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 Sโ„‹ = {โ„Ž โˆˆ ๐’ซ โ„‹ โˆฃ (0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž)) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž)) โŠ† โ„Ž)}
Detailed syntax breakdown of Definition df-sh
StepHypRef Expression
1 csh 30159 . 2 class Sโ„‹
2 c0v 30155 . . . . 5 class 0โ„Ž
3 vh . . . . . 6 setvar โ„Ž
43cv 1541 . . . . 5 class โ„Ž
52, 4wcel 2107 . . . 4 wff 0โ„Ž โˆˆ โ„Ž
6 cva 30151 . . . . . 6 class +โ„Ž
74, 4cxp 5673 . . . . . 6 class (โ„Ž ร— โ„Ž)
86, 7cima 5678 . . . . 5 class ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž))
98, 4wss 3947 . . . 4 wff ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž)) โŠ† โ„Ž
10 csm 30152 . . . . . 6 class ยทโ„Ž
11 cc 11104 . . . . . . 7 class โ„‚
1211, 4cxp 5673 . . . . . 6 class (โ„‚ ร— โ„Ž)
1310, 12cima 5678 . . . . 5 class ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž))
1413, 4wss 3947 . . . 4 wff ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž)) โŠ† โ„Ž
155, 9, 14w3a 1088 . . 3 wff (0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž)) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž)) โŠ† โ„Ž)
16 chba 30150 . . . 4 class โ„‹
1716cpw 4601 . . 3 class ๐’ซ โ„‹
1815, 3, 17crab 3433 . 2 class {โ„Ž โˆˆ ๐’ซ โ„‹ โˆฃ (0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž)) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž)) โŠ† โ„Ž)}
191, 18wceq 1542 1 wff Sโ„‹ = {โ„Ž โˆˆ ๐’ซ โ„‹ โˆฃ (0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ (โ„Ž ร— โ„Ž)) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— โ„Ž)) โŠ† โ„Ž)}
Colors of variables: wff setvar class
This definition is referenced by:  issh  30439
  Copyright terms: Public domain W3C validator