Metamath Proof Explorer

Theorem dochord2N

Description: Ordering law for orthocomplement. (Contributed by NM, 29-Oct-2014) (New usage is discouraged.)

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 dochord2N ⊢ φ → ⊥ ˙ ⁡ 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 ∧ X ∈ ran ⁡ I → X ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W
10 4 5 9 syl2anc ⊢ φ → X ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W
11 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
12 11 8 lssss ⊢ X ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W → X ⊆ Base DVecH ⁡ K ⁡ W
13 10 12 syl ⊢ φ → X ⊆ Base DVecH ⁡ K ⁡ W
14 1 2 7 11 3 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ Base DVecH ⁡ K ⁡ W → ⊥ ˙ ⁡ X ∈ ran ⁡ I
15 4 13 14 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ I
16 1 2 3 4 15 6 dochord ⊢ φ → ⊥ ˙ ⁡ X ⊆ Y ↔ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
17 1 2 3 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
18 4 5 17 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
19 18 sseq2d ⊢ φ → ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ↔ ⊥ ˙ ⁡ Y ⊆ X
20 16 19 bitrd ⊢ φ → ⊥ ˙ ⁡ X ⊆ Y ↔ ⊥ ˙ ⁡ Y ⊆ X