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 𝐻 = ( LHyp ‘ 𝐾 )
dochsnshp.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsnshp.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsnshp.v 𝑉 = ( Base ‘ 𝑈 )
dochsnshp.z 0 = ( 0g𝑈 )
dochsnshp.y 𝑌 = ( LSHyp ‘ 𝑈 )
dochsnshp.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochsnshp.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion dochsnshp ( 𝜑 → ( ‘ { 𝑋 } ) ∈ 𝑌 )

Proof

Step Hyp Ref Expression
1 dochsnshp.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsnshp.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsnshp.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsnshp.v 𝑉 = ( Base ‘ 𝑈 )
5 dochsnshp.z 0 = ( 0g𝑈 )
6 dochsnshp.y 𝑌 = ( LSHyp ‘ 𝑈 )
7 dochsnshp.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 dochsnshp.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
9 eqid ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
10 8 eldifad ( 𝜑𝑋𝑉 )
11 10 snssd ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
12 1 3 2 4 9 7 11 dochocsp ( 𝜑 → ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ‘ { 𝑋 } ) )
13 eqid ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
14 1 3 7 dvhlmod ( 𝜑𝑈 ∈ LMod )
15 4 9 5 13 14 8 lsatlspsn ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
16 1 3 2 13 6 7 15 dochsatshp ( 𝜑 → ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ∈ 𝑌 )
17 12 16 eqeltrrd ( 𝜑 → ( ‘ { 𝑋 } ) ∈ 𝑌 )