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

Theorem shss 28592
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 28590 . . 3 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (( + “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( · “ (ℂ × 𝐻)) ⊆ 𝐻)))
21simplbi 492 . 2 (𝐻S → (𝐻 ⊆ ℋ ∧ 0𝐻))
32simpld 489 1 (𝐻S𝐻 ⊆ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  wss 3769   × cxp 5310  cima 5315  cc 10222  chba 28301   + cva 28302   · csm 28303  0c0v 28306   S csh 28310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-hilex 28381
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-xp 5318  df-cnv 5320  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-sh 28589
This theorem is referenced by:  shel  28593  shex  28594  shssii  28595  shsubcl  28602  chss  28611  shsspwh  28628  hhsssh  28651  shocel  28666  shocsh  28668  ocss  28669  shocss  28670  shocorth  28676  shococss  28678  shorth  28679  shoccl  28689  shsel  28698  shintcli  28713  spanid  28731  shjval  28735  shjcl  28740  shlej1  28744  shlub  28798  chscllem2  29022  chscllem4  29024
  Copyright terms: Public domain W3C validator