dochss

Description: Subset law for orthocomplement. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	dochss.h	$⊢ H = LHyp (K)$
	dochss.u	$⊢ U = DVecH (K) (W)$
	dochss.v	$⊢ V = {Base}_{U}$
	dochss.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
Assertion	dochss	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$

Proof

Step	Hyp	Ref	Expression
1		dochss.h	$⊢ H = LHyp (K)$
2		dochss.u	$⊢ U = DVecH (K) (W)$
3		dochss.v	$⊢ V = {Base}_{U}$
4		dochss.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		simp1l	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to K \in HL$
6		hlclat	$⊢ K \in HL \to K \in CLat$
7	5 6	syl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to K \in CLat$
8		ssrab2	$⊢ \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K}$
9	8	a1i	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K}$
10		simpll3	$⊢ ((((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \land z \in {Base}_{K}) \land Y \subseteq DIsoH (K) (W) (z)) \to X \subseteq Y$
11		simpr	$⊢ ((((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \land z \in {Base}_{K}) \land Y \subseteq DIsoH (K) (W) (z)) \to Y \subseteq DIsoH (K) (W) (z)$
12	10 11	sstrd	$⊢ ((((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \land z \in {Base}_{K}) \land Y \subseteq DIsoH (K) (W) (z)) \to X \subseteq DIsoH (K) (W) (z)$
13	12	ex	$⊢ (((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \land z \in {Base}_{K}) \to (Y \subseteq DIsoH (K) (W) (z) \to X \subseteq DIsoH (K) (W) (z))$
14	13	ss2rabdv	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\} \subseteq \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16		eqid	$⊢ \leq_{K} = \leq_{K}$
17		eqid	$⊢ glb (K) = glb (K)$
18	15 16 17	clatglbss	$⊢ (K \in CLat \land \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K} \land \{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\} \subseteq \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \to glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \leq_{K} glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})$
19	7 9 14 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \leq_{K} glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})$
20		hlop	$⊢ K \in HL \to K \in OP$
21	5 20	syl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to K \in OP$
22	15 17	clatglbcl	$⊢ (K \in CLat \land \{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K}) \to glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}$
23	7 8 22	sylancl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}$
24		ssrab2	$⊢ \{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K}$
25	15 17	clatglbcl	$⊢ (K \in CLat \land \{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\} \subseteq {Base}_{K}) \to glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}$
26	7 24 25	sylancl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}$
27		eqid	$⊢ oc (K) = oc (K)$
28	15 16 27	oplecon3b	$⊢ (K \in OP \land glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K} \land glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}) \to (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \leq_{K} glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \leftrightarrow oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \leq_{K} oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
29	21 23 26 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \leq_{K} glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \leftrightarrow oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \leq_{K} oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
30	19 29	mpbid	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \leq_{K} oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}))$
31		simp1	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to (K \in HL \land W \in H)$
32	15 27	opoccl	$⊢ (K \in OP \land glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}) \to oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K}$
33	21 26 32	syl2anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K}$
34	15 27	opoccl	$⊢ (K \in OP \land glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}) \in {Base}_{K}) \to oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K}$
35	21 23 34	syl2anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K}$
36		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
37	15 16 1 36	dihord	$⊢ ((K \in HL \land W \in H) \land oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K} \land oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})) \in {Base}_{K}) \to (DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}))) \subseteq DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}))) \leftrightarrow oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \leq_{K} oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
38	31 33 35 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to (DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}))) \subseteq DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\}))) \leftrightarrow oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})) \leq_{K} oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
39	30 38	mpbird	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\}))) \subseteq DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
40	15 17 27 1 36 2 3 4	dochval	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V) \to \underset{˙}{⊥} (Y) = DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})))$
41	40	3adant3	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) = DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| Y \subseteq DIsoH (K) (W) (z)\})))$
42		simp3	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to X \subseteq Y$
43		simp2	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to Y \subseteq V$
44	42 43	sstrd	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to X \subseteq V$
45	15 17 27 1 36 2 3 4	dochval	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) = DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
46	31 44 45	syl2anc	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (X) = DIsoH (K) (W) (oc (K) (glb (K) (\{z \in {Base}_{K} \| X \subseteq DIsoH (K) (W) (z)\})))$
47	39 41 46	3sstr4d	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$

Metamath Proof Explorer

Theorem dochss

Proof