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 ⊢H=LHyp⁡K
dochocsn.u ⊢U=DVecH⁡K⁡W
dochocsn.o ⊢⊥˙=ocH⁡K⁡W
dochocsn.v ⊢V=BaseU
dochocsn.n ⊢N=LSpan⁡U
dochocsn.k ⊢φ→K∈HL∧W∈H
dochocsn.x ⊢φ→X∈V
Assertion dochocsn ⊢φ→⊥˙⁡⊥˙⁡X=N⁡X

Proof

Step Hyp Ref Expression
1 dochocsn.h ⊢H=LHyp⁡K
2 dochocsn.u ⊢U=DVecH⁡K⁡W
3 dochocsn.o ⊢⊥˙=ocH⁡K⁡W
4 dochocsn.v ⊢V=BaseU
5 dochocsn.n ⊢N=LSpan⁡U
6 dochocsn.k ⊢φ→K∈HL∧W∈H
7 dochocsn.x ⊢φ→X∈V
8 7 snssd ⊢φ→X⊆V
9 1 2 3 4 5 6 8 dochocsp ⊢φ→⊥˙⁡N⁡X=⊥˙⁡X
10 9 fveq2d ⊢φ→⊥˙⁡⊥˙⁡N⁡X=⊥˙⁡⊥˙⁡X
11 eqid ⊢DIsoH⁡K⁡W=DIsoH⁡K⁡W
12 1 2 4 5 11 dihlsprn ⊢K∈HL∧W∈H∧X∈V→N⁡X∈ran⁡DIsoH⁡K⁡W
13 6 7 12 syl2anc ⊢φ→N⁡X∈ran⁡DIsoH⁡K⁡W
14 1 11 3 dochoc ⊢K∈HL∧W∈H∧N⁡X∈ran⁡DIsoH⁡K⁡W→⊥˙⁡⊥˙⁡N⁡X=N⁡X
15 6 13 14 syl2anc ⊢φ→⊥˙⁡⊥˙⁡N⁡X=N⁡X
16 10 15 eqtr3d ⊢φ→⊥˙⁡⊥˙⁡X=N⁡X