This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) )