Metamath Proof Explorer


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=LHypK
dochlss.u U=DVecHKW
dochlss.v V=BaseU
dochlss.s S=LSubSpU
dochlss.o ˙=ocHKW
Assertion dochlss KHLWHXV˙XS

Proof

Step Hyp Ref Expression
1 dochlss.h H=LHypK
2 dochlss.u U=DVecHKW
3 dochlss.v V=BaseU
4 dochlss.s S=LSubSpU
5 dochlss.o ˙=ocHKW
6 eqid DIsoHKW=DIsoHKW
7 1 6 2 3 5 dochcl KHLWHXV˙XranDIsoHKW
8 1 2 6 4 dihrnlss KHLWH˙XranDIsoHKW˙XS
9 7 8 syldan KHLWHXV˙XS