Theorem cssval

Description: The set of closed subspaces of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssval.o	|- ._|_ = ( ocv ` W )
	cssval.c	|- C = ( ClSubSp ` W )
Assertion	cssval	|- ( W e. X -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )

Proof

Step	Hyp	Ref	Expression
1		cssval.o	|- ._|_ = ( ocv ` W )
2		cssval.c	|- C = ( ClSubSp ` W )
3		elex	|- ( W e. X -> W e. _V )
4		fveq2	|- ( w = W -> ( ocv ` w ) = ( ocv ` W ) )
5	4 1	eqtr4di	|- ( w = W -> ( ocv ` w ) = ._|_ )
6	5	fveq1d	|- ( w = W -> ( ( ocv ` w ) ` s ) = ( ._|_ ` s ) )
7	5 6	fveq12d	|- ( w = W -> ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) = ( ._|_ ` ( ._|_ ` s ) ) )
8	7	eqeq2d	|- ( w = W -> ( s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) <-> s = ( ._|_ ` ( ._|_ ` s ) ) ) )
9	8	abbidv	|- ( w = W -> { s | s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) } = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )
10		df-css	|- ClSubSp = ( w e. _V |-> { s | s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) } )
11		fvex	|- ( Base ` W ) e. _V
12	11	pwex	|- ~P ( Base ` W ) e. _V
13		id	|- ( s = ( ._|_ ` ( ._|_ ` s ) ) -> s = ( ._|_ ` ( ._|_ ` s ) ) )
14		eqid	|- ( Base ` W ) = ( Base ` W )
15	14 1	ocvss	|- ( ._|_ ` ( ._|_ ` s ) ) C_ ( Base ` W )
16		fvex	|- ( ._|_ ` ( ._|_ ` s ) ) e. _V
17	16	elpw	|- ( ( ._|_ ` ( ._|_ ` s ) ) e. ~P ( Base ` W ) <-> ( ._|_ ` ( ._|_ ` s ) ) C_ ( Base ` W ) )
18	15 17	mpbir	|- ( ._|_ ` ( ._|_ ` s ) ) e. ~P ( Base ` W )
19	13 18	eqeltrdi	|- ( s = ( ._|_ ` ( ._|_ ` s ) ) -> s e. ~P ( Base ` W ) )
20	19	abssi	|- { s | s = ( ._|_ ` ( ._|_ ` s ) ) } C_ ~P ( Base ` W )
21	12 20	ssexi	|- { s | s = ( ._|_ ` ( ._|_ ` s ) ) } e. _V
22	9 10 21	fvmpt	|- ( W e. _V -> ( ClSubSp ` W ) = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )
23	2 22	syl5eq	|- ( W e. _V -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )
24	3 23	syl	|- ( W e. X -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )