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 ( 𝜑 → ( ‘ ( ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )