# Metamath Proof Explorer

## Theorem dochn0nv

Description: An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochn0nv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochn0nv.o
dochn0nv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochn0nv.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochn0nv.z
dochn0nv.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochn0nv.x ${⊢}{\phi }\to {X}\subseteq {V}$
Assertion dochn0nv

### Proof

Step Hyp Ref Expression
1 dochn0nv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochn0nv.o
3 dochn0nv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochn0nv.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochn0nv.z
6 dochn0nv.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 dochn0nv.x ${⊢}{\phi }\to {X}\subseteq {V}$
8 eqid ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right)=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
9 1 8 3 4 2 dochcl
10 6 7 9 syl2anc
11 1 8 2 dochoc
12 6 10 11 syl2anc
13 1 3 2 4 5 doch1
14 6 13 syl
15 12 14 eqeq12d
16 1 3 4 2 dochssv
17 6 7 16 syl2anc
18 1 8 3 4 2 dochcl
19 6 17 18 syl2anc
20 1 8 3 4 dih1rn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {V}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
21 6 20 syl ${⊢}{\phi }\to {V}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
22 1 8 2 6 19 21 doch11
23 15 22 bitr3d
24 23 necon3bid