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

Theorem shss 31239
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 31237 . . 3 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (( + “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( · “ (ℂ × 𝐻)) ⊆ 𝐻)))
21simplbi 497 . 2 (𝐻S → (𝐻 ⊆ ℋ ∧ 0𝐻))
32simpld 494 1 (𝐻S𝐻 ⊆ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2106  wss 3963   × cxp 5687  cima 5692  cc 11151  chba 30948   + cva 30949   · csm 30950  0c0v 30953   S csh 30957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-hilex 31028
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-sh 31236
This theorem is referenced by:  shel  31240  shex  31241  shssii  31242  shsubcl  31249  chss  31258  shsspwh  31275  hhsssh  31298  shocel  31311  shocsh  31313  ocss  31314  shocss  31315  shocorth  31321  shococss  31323  shorth  31324  shoccl  31334  shsel  31343  shintcli  31358  spanid  31376  shjval  31380  shjcl  31385  shlej1  31389  shlub  31443  chscllem2  31667  chscllem4  31669
  Copyright terms: Public domain W3C validator