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

Metamath Proof Explorer

Theorem dochocsn

Description: The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015)

Ref Expression
Hypotheses dochocsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochocsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochocsn.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochocsn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochocsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dochocsn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochocsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion dochocsn ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 dochocsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochocsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochocsn.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 dochocsn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochocsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 dochocsn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochocsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 7 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
9 1 2 3 4 5 6 8 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
10 9 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) )
11 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
12 1 2 4 5 11 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
13 6 7 12 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
14 1 11 3 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
15 6 13 14 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
16 10 15 eqtr3d ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )