Metamath Proof Explorer

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 ⊢ H = LHyp ⁡ K
dochnel.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochnel.u ⊢ U = DVecH ⁡ K ⁡ W
dochnel.v ⊢ V = Base U
dochnel.z ⊢ 0 ˙ = 0 U
dochnel.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochnel.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion dochnel ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 dochnel.h ⊢ H = LHyp ⁡ K
2 dochnel.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochnel.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochnel.v ⊢ V = Base U
5 dochnel.z ⊢ 0 ˙ = 0 U
6 dochnel.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochnel.x ⊢ φ → X ∈ V ∖ 0 ˙
8 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
9 1 3 6 dvhlmod ⊢ φ → U ∈ LMod
10 7 eldifad ⊢ φ → X ∈ V
11 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
12 4 8 11 lspsncl ⊢ U ∈ LMod ∧ X ∈ V → LSpan ⁡ U ⁡ X ∈ LSubSp ⁡ U
13 9 10 12 syl2anc ⊢ φ → LSpan ⁡ U ⁡ X ∈ LSubSp ⁡ U
14 4 11 lspsnid ⊢ U ∈ LMod ∧ X ∈ V → X ∈ LSpan ⁡ U ⁡ X
15 9 10 14 syl2anc ⊢ φ → X ∈ LSpan ⁡ U ⁡ X
16 eldifsni ⊢ X ∈ V ∖ 0 ˙ → X ≠ 0 ˙
17 7 16 syl ⊢ φ → X ≠ 0 ˙
18 eldifsn ⊢ X ∈ LSpan ⁡ U ⁡ X ∖ 0 ˙ ↔ X ∈ LSpan ⁡ U ⁡ X ∧ X ≠ 0 ˙
19 15 17 18 sylanbrc ⊢ φ → X ∈ LSpan ⁡ U ⁡ X ∖ 0 ˙
20 1 3 8 5 2 6 13 19 dochnel2 ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X
21 10 snssd ⊢ φ → X ⊆ V
22 1 3 2 4 11 6 21 dochocsp ⊢ φ → ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X = ⊥ ˙ ⁡ X
23 20 22 neleqtrd ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ X