# Metamath Proof Explorer

## Definition df-sh

Description: Define the set of subspaces of a Hilbert space. See issh for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of Beran p. 95. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion df-sh ${⊢}{\mathbf{S}}_{ℋ}=\left\{{h}\in 𝒫ℋ|\left({0}_{ℎ}\in {h}\wedge {+}_{ℎ}\left[{h}×{h}\right]\subseteq {h}\wedge {\cdot }_{ℎ}\left[ℂ×{h}\right]\subseteq {h}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 csh ${class}{\mathbf{S}}_{ℋ}$
1 vh ${setvar}{h}$
2 chba ${class}ℋ$
3 2 cpw ${class}𝒫ℋ$
4 c0v ${class}{0}_{ℎ}$
5 1 cv ${setvar}{h}$
6 4 5 wcel ${wff}{0}_{ℎ}\in {h}$
7 cva ${class}{+}_{ℎ}$
8 5 5 cxp ${class}\left({h}×{h}\right)$
9 7 8 cima ${class}{+}_{ℎ}\left[{h}×{h}\right]$
10 9 5 wss ${wff}{+}_{ℎ}\left[{h}×{h}\right]\subseteq {h}$
11 csm ${class}{\cdot }_{ℎ}$
12 cc ${class}ℂ$
13 12 5 cxp ${class}\left(ℂ×{h}\right)$
14 11 13 cima ${class}{\cdot }_{ℎ}\left[ℂ×{h}\right]$
15 14 5 wss ${wff}{\cdot }_{ℎ}\left[ℂ×{h}\right]\subseteq {h}$
16 6 10 15 w3a ${wff}\left({0}_{ℎ}\in {h}\wedge {+}_{ℎ}\left[{h}×{h}\right]\subseteq {h}\wedge {\cdot }_{ℎ}\left[ℂ×{h}\right]\subseteq {h}\right)$
17 16 1 3 crab ${class}\left\{{h}\in 𝒫ℋ|\left({0}_{ℎ}\in {h}\wedge {+}_{ℎ}\left[{h}×{h}\right]\subseteq {h}\wedge {\cdot }_{ℎ}\left[ℂ×{h}\right]\subseteq {h}\right)\right\}$
18 0 17 wceq ${wff}{\mathbf{S}}_{ℋ}=\left\{{h}\in 𝒫ℋ|\left({0}_{ℎ}\in {h}\wedge {+}_{ℎ}\left[{h}×{h}\right]\subseteq {h}\wedge {\cdot }_{ℎ}\left[ℂ×{h}\right]\subseteq {h}\right)\right\}$