Theorem css0

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

	Ref	Expression
Hypotheses	css0.c	|- C = ( ClSubSp ` W )
	css0.z	|- .0. = ( 0g ` W )
Assertion	css0	|- ( W e. PreHil -> { .0. } e. C )

Proof

Step	Hyp	Ref	Expression
1		css0.c	|- C = ( ClSubSp ` W )
2		css0.z	|- .0. = ( 0g ` W )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4		eqid	|- ( ocv ` W ) = ( ocv ` W )
5	3 4 2	ocv1	|- ( W e. PreHil -> ( ( ocv ` W ) ` ( Base ` W ) ) = { .0. } )
6		ssid	|- ( Base ` W ) C_ ( Base ` W )
7	3 1 4	ocvcss	|- ( ( W e. PreHil /\ ( Base ` W ) C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( Base ` W ) ) e. C )
8	6 7	mpan2	|- ( W e. PreHil -> ( ( ocv ` W ) ` ( Base ` W ) ) e. C )
9	5 8	eqeltrrd	|- ( W e. PreHil -> { .0. } e. C )