Theorem dochsnnz

Description: The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015)

	Ref	Expression
Hypotheses	dochsnnz.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochsnnz.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochsnnz.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochsnnz.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochsnnz.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochsnnz.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochsnnz.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	dochsnnz	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		dochsnnz.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochsnnz.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochsnnz.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochsnnz.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochsnnz.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochsnnz.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dochsnnz.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
9	1 3 2 4 8 6 7	dochocsn	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
10	1 3 4 8 6 7	dvh2dim	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑉 ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
11		eleq2	⊢ ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = 𝑉 → ( 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ↔ 𝑦 ∈ 𝑉 ) )
12	11	biimprcd	⊢ ( 𝑦 ∈ 𝑉 → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = 𝑉 → 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
13	12	necon3bd	⊢ ( 𝑦 ∈ 𝑉 → ( ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 ) )
14	13	rexlimiv	⊢ ( ∃ 𝑦 ∈ 𝑉 ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 )
15	10 14	syl	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 )
16	9 15	eqnetrd	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ≠ 𝑉 )
17	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
18	1 2 3 4 5 6 17	dochn0nv	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ≠ 𝑉 ) )
19	16 18	mpbird	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } )