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	$⊢ \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	dochord3	$⊢ φ \to (X \subseteq \underset{˙}{⊥} (Y) \leftrightarrow Y \subseteq \underset{˙}{⊥} (X))$

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		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
8		eqid	$⊢ LSubSp (DVecH (K) (W)) = LSubSp (DVecH (K) (W))$
9	1 7 2 8	dihrnlss	$⊢ ((K \in HL \land W \in H) \land Y \in ran I) \to Y \in LSubSp (DVecH (K) (W))$
10	4 6 9	syl2anc	$⊢ φ \to Y \in LSubSp (DVecH (K) (W))$
11		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
12	11 8	lssss	$⊢ Y \in LSubSp (DVecH (K) (W)) \to Y \subseteq {Base}_{DVecH (K) (W)}$
13	10 12	syl	$⊢ φ \to Y \subseteq {Base}_{DVecH (K) (W)}$
14	1 2 7 11 3	dochcl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq {Base}_{DVecH (K) (W)}) \to \underset{˙}{⊥} (Y) \in ran I$
15	4 13 14	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Y) \in ran I$
16	1 2 3 4 5 15	dochord	$⊢ φ \to (X \subseteq \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (X))$
17	1 2 3	dochoc	$⊢ ((K \in HL \land W \in H) \land Y \in ran I) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
18	4 6 17	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
19	18	sseq1d	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (X) \leftrightarrow Y \subseteq \underset{˙}{⊥} (X))$
20	16 19	bitrd	$⊢ φ \to (X \subseteq \underset{˙}{⊥} (Y) \leftrightarrow Y \subseteq \underset{˙}{⊥} (X))$

Metamath Proof Explorer