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

Theorem shss 28297
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 28295 . . 3 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (( + “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( · “ (ℂ × 𝐻)) ⊆ 𝐻)))
21simplbi 478 . 2 (𝐻S → (𝐻 ⊆ ℋ ∧ 0𝐻))
32simpld 477 1 (𝐻S𝐻 ⊆ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2103  wss 3680   × cxp 5216  cima 5221  cc 10047  chil 28006   + cva 28007   · csm 28008  0c0v 28011   S csh 28015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-hilex 28086
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-opab 4821  df-xp 5224  df-cnv 5226  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-sh 28294
This theorem is referenced by:  shel  28298  shex  28299  shssii  28300  shsubcl  28307  chss  28316  shsspwh  28333  hhsssh  28356  shocel  28371  shocsh  28373  ocss  28374  shocss  28375  shocorth  28381  shococss  28383  shorth  28384  shoccl  28394  shsel  28403  shintcli  28418  spanid  28436  shjval  28440  shjcl  28445  shlej1  28449  shlub  28503  chscllem2  28727  chscllem4  28729
  Copyright terms: Public domain W3C validator