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}}_{\mathscr{H}}=\left\{h\in 𝒫\mathscr{H}|\left(0_{ℎ}\in h\wedge {+}_{ℎ}\left[h\times h\right]\subseteq h\wedge {\cdot }_{ℎ}\left[ℂ\times h\right]\subseteq h\right)\right\}$$

Detailed syntax breakdown

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