Theorem cssi

Description: Property of a closed subspace (of a pre-Hilbert space). (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssval.o	|- ._|_ = ( ocv ` W )
	cssval.c	|- C = ( ClSubSp ` W )
Assertion	cssi	|- ( S e. C -> S = ( ._|_ ` ( ._|_ ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		cssval.o	|- ._|_ = ( ocv ` W )
2		cssval.c	|- C = ( ClSubSp ` W )
3		elfvdm	|- ( S e. ( ClSubSp ` W ) -> W e. dom ClSubSp )
4	3 2	eleq2s	|- ( S e. C -> W e. dom ClSubSp )
5	1 2	iscss	|- ( W e. dom ClSubSp -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )
6	4 5	syl	|- ( S e. C -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )
7	6	ibi	|- ( S e. C -> S = ( ._|_ ` ( ._|_ ` S ) ) )