Theorem ocvss

Description: The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	ocvss.v	|- V = ( Base ` W )
	ocvss.o	|- ._|_ = ( ocv ` W )
Assertion	ocvss	|- ( ._|_ ` S ) C_ V

Proof

Step	Hyp	Ref	Expression
1		ocvss.v	|- V = ( Base ` W )
2		ocvss.o	|- ._|_ = ( ocv ` W )
3		eqid	|- ( .i ` W ) = ( .i ` W )
4		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
5		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
6	1 3 4 5 2	elocv	|- ( x e. ( ._|_ ` S ) <-> ( S C_ V /\ x e. V /\ A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
7	6	simp2bi	|- ( x e. ( ._|_ ` S ) -> x e. V )
8	7	ssriv	|- ( ._|_ ` S ) C_ V