Theorem css1

Description: The whole space is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	css1.v	|- V = ( Base ` W )
	css1.c	|- C = ( ClSubSp ` W )
Assertion	css1	|- ( W e. PreHil -> V e. C )

Proof

Step	Hyp	Ref	Expression
1		css1.v	|- V = ( Base ` W )
2		css1.c	|- C = ( ClSubSp ` W )
3		eqid	|- ( ocv ` W ) = ( ocv ` W )
4	1 3	ocv0	|- ( ( ocv ` W ) ` (/) ) = V
5		0ss	|- (/) C_ V
6	1 2 3	ocvcss	|- ( ( W e. PreHil /\ (/) C_ V ) -> ( ( ocv ` W ) ` (/) ) e. C )
7	5 6	mpan2	|- ( W e. PreHil -> ( ( ocv ` W ) ` (/) ) e. C )
8	4 7	eqeltrrid	|- ( W e. PreHil -> V e. C )