Theorem dochnel

Description: A nonzero vector doesn't belong to the orthocomplement of its singleton. (Contributed by NM, 27-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dochnel.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochnel.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochnel.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochnel.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochnel.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochnel.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dochnel.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
8		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
9	1 3 6	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
10	7	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
12	4 8 11	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
13	9 10 12	syl2anc	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
14	4 11	lspsnid	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
15	9 10 14	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
16		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
17	7 16	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
18		eldifsn	⊢ ( 𝑋 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∧ 𝑋 ≠ 0 ) )
19	15 17 18	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∖ { 0 } ) )
20	1 3 8 5 2 6 13 19	dochnel2	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
21	10	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
22	1 3 2 4 11 6 21	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
23	20 22	neleqtrd	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) )