Metamath Proof Explorer

Theorem doch11

Description: Orthocomplement is one-to-one. (Contributed by NM, 12-Aug-2014)

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 doch11 ⊢ φ → ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ Y ↔ X = Y

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 1 2 3 4 6 5 dochord ⊢ φ → Y ⊆ X ↔ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ Y
8 1 2 3 4 5 6 dochord ⊢ φ → X ⊆ Y ↔ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
9 7 8 anbi12d ⊢ φ → Y ⊆ X ∧ X ⊆ Y ↔ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ Y ∧ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
10 eqcom ⊢ X = Y ↔ Y = X
11 eqss ⊢ Y = X ↔ Y ⊆ X ∧ X ⊆ Y
12 10 11 bitri ⊢ X = Y ↔ Y ⊆ X ∧ X ⊆ Y
13 eqss ⊢ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ Y ↔ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ Y ∧ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
14 9 12 13 3bitr4g ⊢ φ → X = Y ↔ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ Y
15 14 bicomd ⊢ φ → ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ Y ↔ X = Y