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 = Base U
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 = Base U
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