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

Theorem shss 31229
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 31227 . . 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 2108  wss 3951   × cxp 5683  cima 5688  cc 11153  chba 30938   + cva 30939   · csm 30940  0c0v 30943   S csh 30947
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-hilex 31018
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-sh 31226
This theorem is referenced by:  shel  31230  shex  31231  shssii  31232  shsubcl  31239  chss  31248  shsspwh  31265  hhsssh  31288  shocel  31301  shocsh  31303  ocss  31304  shocss  31305  shocorth  31311  shococss  31313  shorth  31314  shoccl  31324  shsel  31333  shintcli  31348  spanid  31366  shjval  31370  shjcl  31375  shlej1  31379  shlub  31433  chscllem2  31657  chscllem4  31659
  Copyright terms: Public domain W3C validator