df-css

Description: Define the set of closed (linear) subspaces of a given pre-Hilbert space. (Contributed by NM, 7-Oct-2011)

		Ref	Expression
	Assertion	df-css	$⊢ ClSubSp = (h \in V ⟼ \{s \| s = ocv (h) (ocv (h) (s))\})$

Step	Hyp	Ref	Expression
0		ccss	$class ClSubSp$
1		vh	$setvar h$
2		cvv	$class V$
3		vs	$setvar s$
4	3	cv	$setvar s$
5		cocv	$class ocv$
6	1	cv	$setvar h$
7	6 5	cfv	$class ocv (h)$
8	4 7	cfv	$class ocv (h) (s)$
9	8 7	cfv	$class ocv (h) (ocv (h) (s))$
10	4 9	wceq	$wff s = ocv (h) (ocv (h) (s))$
11	10 3	cab	$class \{s \| s = ocv (h) (ocv (h) (s))\}$
12	1 2 11	cmpt	$class (h \in V ⟼ \{s \| s = ocv (h) (ocv (h) (s))\})$
13	0 12	wceq	$wff ClSubSp = (h \in V ⟼ \{s \| s = ocv (h) (ocv (h) (s))\})$

Metamath Proof Explorer