dochord

Description: Ordering law for orthocomplement. (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	dochord	$⊢ φ \to (X \subseteq Y \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$

Proof

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	4	adantr	$⊢ (φ \land X \subseteq Y) \to (K \in HL \land W \in H)$
8		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
9		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
10	1 8 2 9	dihrnss	$⊢ ((K \in HL \land W \in H) \land Y \in ran I) \to Y \subseteq {Base}_{DVecH (K) (W)}$
11	4 6 10	syl2anc	$⊢ φ \to Y \subseteq {Base}_{DVecH (K) (W)}$
12	11	adantr	$⊢ (φ \land X \subseteq Y) \to Y \subseteq {Base}_{DVecH (K) (W)}$
13		simpr	$⊢ (φ \land X \subseteq Y) \to X \subseteq Y$
14	1 8 9 3	dochss	$⊢ ((K \in HL \land W \in H) \land Y \subseteq {Base}_{DVecH (K) (W)} \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
15	7 12 13 14	syl3anc	$⊢ (φ \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
16	4	adantr	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to (K \in HL \land W \in H)$
17	1 8 2 9	dihrnss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \subseteq {Base}_{DVecH (K) (W)}$
18	4 5 17	syl2anc	$⊢ φ \to X \subseteq {Base}_{DVecH (K) (W)}$
19	1 2 8 9 3	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{DVecH (K) (W)}) \to \underset{˙}{⊥} (X) \in ran I$
20	4 18 19	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran I$
21	1 8 2 9	dihrnss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran I) \to \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)}$
22	4 20 21	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)}$
23	22	adantr	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)}$
24		simpr	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
25	1 8 9 3	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)} \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
26	16 23 24 25	syl3anc	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
27	1 2 3	dochoc	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
28	4 5 27	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
29	28	adantr	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
30	1 2 3	dochoc	$⊢ ((K \in HL \land W \in H) \land Y \in ran I) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
31	4 6 30	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
32	31	adantr	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
33	26 29 32	3sstr3d	$⊢ (φ \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to X \subseteq Y$
34	15 33	impbida	$⊢ φ \to (X \subseteq Y \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem dochord

Proof