Description: A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dochlss.h | |
|
dochlss.u | |
||
dochlss.v | |
||
dochlss.s | |
||
dochlss.o | |
||
Assertion | dochlss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochlss.h | |
|
2 | dochlss.u | |
|
3 | dochlss.v | |
|
4 | dochlss.s | |
|
5 | dochlss.o | |
|
6 | eqid | |
|
7 | 1 6 2 3 5 | dochcl | |
8 | 1 2 6 4 | dihrnlss | |
9 | 7 8 | syldan | |