Theorem csslss

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

	Ref	Expression
Hypotheses	csslss.c	|- C = ( ClSubSp ` W )
	csslss.l	|- L = ( LSubSp ` W )
Assertion	csslss	|- ( ( W e. PreHil /\ S e. C ) -> S e. L )

Proof

Step	Hyp	Ref	Expression
1		csslss.c	|- C = ( ClSubSp ` W )
2		csslss.l	|- L = ( LSubSp ` W )
3		eqid	|- ( ocv ` W ) = ( ocv ` W )
4	3 1	cssi	|- ( S e. C -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
5	4	adantl	|- ( ( W e. PreHil /\ S e. C ) -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
6		eqid	|- ( Base ` W ) = ( Base ` W )
7	6 3	ocvss	|- ( ( ocv ` W ) ` S ) C_ ( Base ` W )
8	7	a1i	|- ( S e. C -> ( ( ocv ` W ) ` S ) C_ ( Base ` W ) )
9	6 3 2	ocvlss	|- ( ( W e. PreHil /\ ( ( ocv ` W ) ` S ) C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) e. L )
10	8 9	sylan2	|- ( ( W e. PreHil /\ S e. C ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) e. L )
11	5 10	eqeltrd	|- ( ( W e. PreHil /\ S e. C ) -> S e. L )