Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  shss Structured version   Visualization version   GIF version

Theorem shss 28990
 Description: A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
shss (𝐻S𝐻 ⊆ ℋ)

Proof of Theorem shss
StepHypRef Expression
1 issh 28988 . . 3 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (( + “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( · “ (ℂ × 𝐻)) ⊆ 𝐻)))
21simplbi 500 . 2 (𝐻S → (𝐻 ⊆ ℋ ∧ 0𝐻))
32simpld 497 1 (𝐻S𝐻 ⊆ ℋ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113   ⊆ wss 3939   × cxp 5556   “ cima 5561  ℂcc 10538   ℋchba 28699   +ℎ cva 28700   ·ℎ csm 28701  0ℎc0v 28704   Sℋ csh 28708 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-hilex 28779 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-xp 5564  df-cnv 5566  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-sh 28987 This theorem is referenced by:  shel  28991  shex  28992  shssii  28993  shsubcl  29000  chss  29009  shsspwh  29026  hhsssh  29049  shocel  29062  shocsh  29064  ocss  29065  shocss  29066  shocorth  29072  shococss  29074  shorth  29075  shoccl  29085  shsel  29094  shintcli  29109  spanid  29127  shjval  29131  shjcl  29136  shlej1  29140  shlub  29194  chscllem2  29418  chscllem4  29420
 Copyright terms: Public domain W3C validator