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