Metamath Proof Explorer

Theorem dochsnshp

Description: The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015)

Ref Expression
Hypotheses dochsnshp.h ⊢ H = LHyp ⁡ K
dochsnshp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsnshp.u ⊢ U = DVecH ⁡ K ⁡ W
dochsnshp.v ⊢ V = Base U
dochsnshp.z ⊢ 0 ˙ = 0 U
dochsnshp.y ⊢ Y = LSHyp ⁡ U
dochsnshp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsnshp.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion dochsnshp ⊢ φ → ⊥ ˙ ⁡ X ∈ Y

Proof

Step Hyp Ref Expression
1 dochsnshp.h ⊢ H = LHyp ⁡ K
2 dochsnshp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochsnshp.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochsnshp.v ⊢ V = Base U
5 dochsnshp.z ⊢ 0 ˙ = 0 U
6 dochsnshp.y ⊢ Y = LSHyp ⁡ U
7 dochsnshp.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dochsnshp.x ⊢ φ → X ∈ V ∖ 0 ˙
9 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
10 8 eldifad ⊢ φ → X ∈ V
11 10 snssd ⊢ φ → X ⊆ V
12 1 3 2 4 9 7 11 dochocsp ⊢ φ → ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X = ⊥ ˙ ⁡ X
13 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
14 1 3 7 dvhlmod ⊢ φ → U ∈ LMod
15 4 9 5 13 14 8 lsatlspsn ⊢ φ → LSpan ⁡ U ⁡ X ∈ LSAtoms ⁡ U
16 1 3 2 13 6 7 15 dochsatshp ⊢ φ → ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X ∈ Y
17 12 16 eqeltrrd ⊢ φ → ⊥ ˙ ⁡ X ∈ Y