Metamath Proof Explorer

Theorem dochsncom

Description: Swap vectors in an orthocomplement of a singleton. (Contributed by NM, 17-Jun-2015)

Ref Expression
Hypotheses dochsncom.h ⊢ H = LHyp ⁡ K
dochsncom.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsncom.u ⊢ U = DVecH ⁡ K ⁡ W
dochsncom.v ⊢ V = Base U
dochsncom.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsncom.x ⊢ φ → X ∈ V
dochsncom.y ⊢ φ → Y ∈ V
Assertion dochsncom ⊢ φ → X ∈ ⊥ ˙ ⁡ Y ↔ Y ∈ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 dochsncom.h ⊢ H = LHyp ⁡ K
2 dochsncom.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochsncom.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochsncom.v ⊢ V = Base U
5 dochsncom.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 dochsncom.x ⊢ φ → X ∈ V
7 dochsncom.y ⊢ φ → Y ∈ V
8 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
9 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
10 1 3 4 9 8 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V → LSpan ⁡ U ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
11 5 6 10 syl2anc ⊢ φ → LSpan ⁡ U ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
12 1 3 4 9 8 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ V → LSpan ⁡ U ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
13 5 7 12 syl2anc ⊢ φ → LSpan ⁡ U ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
14 1 8 2 5 11 13 dochord3 ⊢ φ → LSpan ⁡ U ⁡ X ⊆ ⊥ ˙ ⁡ LSpan ⁡ U ⁡ Y ↔ LSpan ⁡ U ⁡ Y ⊆ ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X
15 7 snssd ⊢ φ → Y ⊆ V
16 1 3 2 4 9 5 15 dochocsp ⊢ φ → ⊥ ˙ ⁡ LSpan ⁡ U ⁡ Y = ⊥ ˙ ⁡ Y
17 16 sseq2d ⊢ φ → LSpan ⁡ U ⁡ X ⊆ ⊥ ˙ ⁡ LSpan ⁡ U ⁡ Y ↔ LSpan ⁡ U ⁡ X ⊆ ⊥ ˙ ⁡ Y
18 6 snssd ⊢ φ → X ⊆ V
19 1 3 2 4 9 5 18 dochocsp ⊢ φ → ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X = ⊥ ˙ ⁡ X
20 19 sseq2d ⊢ φ → LSpan ⁡ U ⁡ Y ⊆ ⊥ ˙ ⁡ LSpan ⁡ U ⁡ X ↔ LSpan ⁡ U ⁡ Y ⊆ ⊥ ˙ ⁡ X
21 14 17 20 3bitr3d ⊢ φ → LSpan ⁡ U ⁡ X ⊆ ⊥ ˙ ⁡ Y ↔ LSpan ⁡ U ⁡ Y ⊆ ⊥ ˙ ⁡ X
22 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
23 1 3 5 dvhlmod ⊢ φ → U ∈ LMod
24 1 3 4 22 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V → ⊥ ˙ ⁡ Y ∈ LSubSp ⁡ U
25 5 15 24 syl2anc ⊢ φ → ⊥ ˙ ⁡ Y ∈ LSubSp ⁡ U
26 4 22 9 23 25 6 lspsnel5 ⊢ φ → X ∈ ⊥ ˙ ⁡ Y ↔ LSpan ⁡ U ⁡ X ⊆ ⊥ ˙ ⁡ Y
27 1 3 4 22 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
28 5 18 27 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
29 4 22 9 23 28 7 lspsnel5 ⊢ φ → Y ∈ ⊥ ˙ ⁡ X ↔ LSpan ⁡ U ⁡ Y ⊆ ⊥ ˙ ⁡ X
30 21 26 29 3bitr4d ⊢ φ → X ∈ ⊥ ˙ ⁡ Y ↔ Y ∈ ⊥ ˙ ⁡ X