Theorem shss 31812

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

Step	Hyp	Ref	Expression
1		issh 31810	. . 3 ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻)))
2	1	simplbi 502	. 2 ⊢ (𝐻 ∈ Sℋ → (𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻))
3	2	simpld 500	1 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   × cxp 5648   “ cima 5653  ℂcc 11198   ℋchba 31521   +_ℎ cva 31522   ·_ℎ csm 31523  0_ℎc0v 31526   S_ℋ csh 31530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-hilex 31601

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-sh 31809

This theorem is used by:  shel  31813  shex  31814  shssii  31815  shsubcl  31822  chss  31831  shsspwh  31848  hhsssh  31871  shocel  31884  shocsh  31886  ocss  31887  shocss  31888  shocorth  31894  shococss  31896  shorth  31897  shoccl  31907  shsel  31916  shintcli  31931  spanid  31949  shjval  31953  shjcl  31958  shlej1  31962  shlub  32016  chscllem2  32240  chscllem4  32242