This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ 𝑌 )