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	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	doch11.k	$⊢ φ \to (K \in HL \land W \in H)$
	doch11.x	$⊢ φ \to X \in ran I$
	doch11.y	$⊢ φ \to Y \in ran I$
Assertion	doch11	$⊢ φ \to (\underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) \leftrightarrow X = Y)$

Step	Hyp	Ref	Expression
1		doch11.h	$⊢ H = LHyp (K)$
2		doch11.i	$⊢ I = DIsoH (K) (W)$
3		doch11.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		doch11.k	$⊢ φ \to (K \in HL \land W \in H)$
5		doch11.x	$⊢ φ \to X \in ran I$
6		doch11.y	$⊢ φ \to Y \in ran I$
7	1 2 3 4 6 5	dochord	$⊢ φ \to (Y \subseteq X \leftrightarrow \underset{˙}{⊥} (X) \subseteq \underset{˙}{⊥} (Y))$
8	1 2 3 4 5 6	dochord	$⊢ φ \to (X \subseteq Y \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
9	7 8	anbi12d	$⊢ φ \to ((Y \subseteq X \land X \subseteq Y) \leftrightarrow (\underset{˙}{⊥} (X) \subseteq \underset{˙}{⊥} (Y) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)))$
10		eqcom	$⊢ X = Y \leftrightarrow Y = X$
11		eqss	$⊢ Y = X \leftrightarrow (Y \subseteq X \land X \subseteq Y)$
12	10 11	bitri	$⊢ X = Y \leftrightarrow (Y \subseteq X \land X \subseteq Y)$
13		eqss	$⊢ \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) \leftrightarrow (\underset{˙}{⊥} (X) \subseteq \underset{˙}{⊥} (Y) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
14	9 12 13	3bitr4g	$⊢ φ \to (X = Y \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y))$
15	14	bicomd	$⊢ φ \to (\underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer