Theorem dochlss

Description: A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014)

	Ref	Expression
Hypotheses	dochlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochlss.v	$$⊢V={\mathrm{Base}}_U$$
	dochlss.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dochlss.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
Assertion	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		dochlss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochlss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dochlss.v	$$⊢V={\mathrm{Base}}_U$$
4		dochlss.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		dochlss.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7	1 6 2 3 5	dochcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8	1 2 6 4	dihrnlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\right)\to \underset{\dot{}}{\perp }\left(X\right)\in S$$
9	7 8	syldan	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\in S$$