Definition 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 e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccss	|- ClSubSp
1		vh	|- h
2		cvv	|- _V
3		vs	|- s
4	3	cv	|- s
5		cocv	|- ocv
6	1	cv	|- h
7	6 5	cfv	|- ( ocv ` h )
8	4 7	cfv	|- ( ( ocv ` h ) ` s )
9	8 7	cfv	|- ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) )
10	4 9	wceq	|- s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) )
11	10 3	cab	|- { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) }
12	1 2 11	cmpt	|- ( h e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )
13	0 12	wceq	|- ClSubSp = ( h e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )