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=BaseU
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=BaseU
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