Theorem iscss

Description: The predicate "is a closed subspace" (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	iscss	|- ( W e. X -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cssval.o	|- ._|_ = ( ocv ` W )
2		cssval.c	|- C = ( ClSubSp ` W )
3	1 2	cssval	|- ( W e. X -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )
4	3	eleq2d	|- ( W e. X -> ( S e. C <-> S e. { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) )
5		id	|- ( S = ( ._|_ ` ( ._|_ ` S ) ) -> S = ( ._|_ ` ( ._|_ ` S ) ) )
6		fvex	|- ( ._|_ ` ( ._|_ ` S ) ) e. _V
7	5 6	eqeltrdi	|- ( S = ( ._|_ ` ( ._|_ ` S ) ) -> S e. _V )
8		id	|- ( s = S -> s = S )
9		2fveq3	|- ( s = S -> ( ._|_ ` ( ._|_ ` s ) ) = ( ._|_ ` ( ._|_ ` S ) ) )
10	8 9	eqeq12d	|- ( s = S -> ( s = ( ._|_ ` ( ._|_ ` s ) ) <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )
11	7 10	elab3	|- ( S e. { s | s = ( ._|_ ` ( ._|_ ` s ) ) } <-> S = ( ._|_ ` ( ._|_ ` S ) ) )
12	4 11	bitrdi	|- ( W e. X -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )