# 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 𝐻 = ( LHyp ‘ 𝐾 )
dochn0nv.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochn0nv.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochn0nv.v 𝑉 = ( Base ‘ 𝑈 )
dochn0nv.z 0 = ( 0g𝑈 )
dochn0nv.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochn0nv.x ( 𝜑𝑋𝑉 )
Assertion dochn0nv ( 𝜑 → ( ( 𝑋 ) ≠ { 0 } ↔ ( ‘ ( 𝑋 ) ) ≠ 𝑉 ) )

### Proof

Step Hyp Ref Expression
1 dochn0nv.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochn0nv.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochn0nv.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochn0nv.v 𝑉 = ( Base ‘ 𝑈 )
5 dochn0nv.z 0 = ( 0g𝑈 )
6 dochn0nv.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 dochn0nv.x ( 𝜑𝑋𝑉 )
8 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 1 8 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
10 6 7 9 syl2anc ( 𝜑 → ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
11 1 8 2 dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( ‘ ( 𝑋 ) ) ) = ( 𝑋 ) )
12 6 10 11 syl2anc ( 𝜑 → ( ‘ ( ‘ ( 𝑋 ) ) ) = ( 𝑋 ) )
13 1 3 2 4 5 doch1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑉 ) = { 0 } )
14 6 13 syl ( 𝜑 → ( 𝑉 ) = { 0 } )
15 12 14 eqeq12d ( 𝜑 → ( ( ‘ ( ‘ ( 𝑋 ) ) ) = ( 𝑉 ) ↔ ( 𝑋 ) = { 0 } ) )
16 1 3 4 2 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ⊆ 𝑉 )
17 6 7 16 syl2anc ( 𝜑 → ( 𝑋 ) ⊆ 𝑉 )
18 1 8 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ⊆ 𝑉 ) → ( ‘ ( 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
19 6 17 18 syl2anc ( 𝜑 → ( ‘ ( 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
20 1 8 3 4 dih1rn ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 6 20 syl ( 𝜑𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
22 1 8 2 6 19 21 doch11 ( 𝜑 → ( ( ‘ ( ‘ ( 𝑋 ) ) ) = ( 𝑉 ) ↔ ( ‘ ( 𝑋 ) ) = 𝑉 ) )
23 15 22 bitr3d ( 𝜑 → ( ( 𝑋 ) = { 0 } ↔ ( ‘ ( 𝑋 ) ) = 𝑉 ) )
24 23 necon3bid ( 𝜑 → ( ( 𝑋 ) ≠ { 0 } ↔ ( ‘ ( 𝑋 ) ) ≠ 𝑉 ) )