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={\mathrm{Base}}_W$$
	ocvss.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
Assertion	ocvss	$$⊢\underset{\dot{}}{\perp }\left(S\right)\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		ocvss.v	$$⊢V={\mathrm{Base}}_W$$
2		ocvss.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
3		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
4		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
6	1 3 4 5 2	elocv	$$⊢x\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow \left(S\subseteq V\wedge x\in V\wedge \forall y\in Sx{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}\right)$$
7	6	simp2bi	$$⊢x\in \underset{\dot{}}{\perp }\left(S\right)\to x\in V$$
8	7	ssriv	$$⊢\underset{\dot{}}{\perp }\left(S\right)\subseteq V$$