Metamath Proof Explorer


Theorem dochord3

Description: Ordering law for orthocomplement. (Contributed by NM, 9-Mar-2015)

Ref Expression
Hypotheses doch11.h H = LHyp K
doch11.i I = DIsoH K W
doch11.o ˙ = ocH K W
doch11.k φ K HL W H
doch11.x φ X ran I
doch11.y φ Y ran I
Assertion dochord3 φ X ˙ Y Y ˙ X

Proof

Step Hyp Ref Expression
1 doch11.h H = LHyp K
2 doch11.i I = DIsoH K W
3 doch11.o ˙ = ocH K W
4 doch11.k φ K HL W H
5 doch11.x φ X ran I
6 doch11.y φ Y ran I
7 eqid DVecH K W = DVecH K W
8 eqid LSubSp DVecH K W = LSubSp DVecH K W
9 1 7 2 8 dihrnlss K HL W H Y ran I Y LSubSp DVecH K W
10 4 6 9 syl2anc φ Y LSubSp DVecH K W
11 eqid Base DVecH K W = Base DVecH K W
12 11 8 lssss Y LSubSp DVecH K W Y Base DVecH K W
13 10 12 syl φ Y Base DVecH K W
14 1 2 7 11 3 dochcl K HL W H Y Base DVecH K W ˙ Y ran I
15 4 13 14 syl2anc φ ˙ Y ran I
16 1 2 3 4 5 15 dochord φ X ˙ Y ˙ ˙ Y ˙ X
17 1 2 3 dochoc K HL W H Y ran I ˙ ˙ Y = Y
18 4 6 17 syl2anc φ ˙ ˙ Y = Y
19 18 sseq1d φ ˙ ˙ Y ˙ X Y ˙ X
20 16 19 bitrd φ X ˙ Y Y ˙ X