lhprelat3N

Description: The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 . (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lhprelat3.b	$⊢ B = {Base}_{K}$
	lhprelat3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhprelat3.s	$⊢ \underset{˙}{<} = <_{K}$
	lhprelat3.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhprelat3.c	$⊢ C = ⋖_{K}$
	lhprelat3.h	$⊢ H = LHyp (K)$
Assertion	lhprelat3N	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists w \in H (X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \land (Y \underset{˙}{\land} w) C Y)$

Proof

Step	Hyp	Ref	Expression
1		lhprelat3.b	$⊢ B = {Base}_{K}$
2		lhprelat3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lhprelat3.s	$⊢ \underset{˙}{<} = <_{K}$
4		lhprelat3.m	$⊢ \underset{˙}{\land} = meet (K)$
5		lhprelat3.c	$⊢ C = ⋖_{K}$
6		lhprelat3.h	$⊢ H = LHyp (K)$
7		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to p \in Atoms (K)$
8		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to K \in HL$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	1 9	atbase	$⊢ p \in Atoms (K) \to p \in B$
11	10	adantl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to p \in B$
12		eqid	$⊢ oc (K) = oc (K)$
13	1 12 9 6	lhpoc2N	$⊢ (K \in HL \land p \in B) \to (p \in Atoms (K) \leftrightarrow oc (K) (p) \in H)$
14	8 11 13	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to (p \in Atoms (K) \leftrightarrow oc (K) (p) \in H)$
15	7 14	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to oc (K) (p) \in H$
16	15	adantr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \land (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))) \to oc (K) (p) \in H$
17		hlop	$⊢ K \in HL \to K \in OP$
18	8 17	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to K \in OP$
19	8	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to K \in Lat$
20		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to Y \in B$
21	1 12	opoccl	$⊢ (K \in OP \land p \in B) \to oc (K) (p) \in B$
22	18 11 21	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to oc (K) (p) \in B$
23	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land oc (K) (p) \in B) \to Y \underset{˙}{\land} oc (K) (p) \in B$
24	19 20 22 23	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to Y \underset{˙}{\land} oc (K) (p) \in B$
25	1 12 5	cvrcon3b	$⊢ (K \in OP \land Y \underset{˙}{\land} oc (K) (p) \in B \land Y \in B) \to ((Y \underset{˙}{\land} oc (K) (p)) C Y \leftrightarrow oc (K) (Y) C oc (K) (Y \underset{˙}{\land} oc (K) (p)))$
26	18 24 20 25	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to ((Y \underset{˙}{\land} oc (K) (p)) C Y \leftrightarrow oc (K) (Y) C oc (K) (Y \underset{˙}{\land} oc (K) (p)))$
27		hlol	$⊢ K \in HL \to K \in OL$
28	8 27	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to K \in OL$
29		eqid	$⊢ join (K) = join (K)$
30	1 29 4 12	oldmm3N	$⊢ (K \in OL \land Y \in B \land p \in B) \to oc (K) (Y \underset{˙}{\land} oc (K) (p)) = oc (K) (Y) join (K) p$
31	28 20 11 30	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to oc (K) (Y \underset{˙}{\land} oc (K) (p)) = oc (K) (Y) join (K) p$
32	31	breq2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to (oc (K) (Y) C oc (K) (Y \underset{˙}{\land} oc (K) (p)) \leftrightarrow oc (K) (Y) C (oc (K) (Y) join (K) p))$
33	26 32	bitr2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to (oc (K) (Y) C (oc (K) (Y) join (K) p) \leftrightarrow (Y \underset{˙}{\land} oc (K) (p)) C Y)$
34		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to X \in B$
35	1 2 12	oplecon3b	$⊢ (K \in OP \land X \in B \land Y \underset{˙}{\land} oc (K) (p) \in B) \to (X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)) \leftrightarrow oc (K) (Y \underset{˙}{\land} oc (K) (p)) \underset{˙}{\leq} oc (K) (X))$
36	18 34 24 35	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to (X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)) \leftrightarrow oc (K) (Y \underset{˙}{\land} oc (K) (p)) \underset{˙}{\leq} oc (K) (X))$
37	31	breq1d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to (oc (K) (Y \underset{˙}{\land} oc (K) (p)) \underset{˙}{\leq} oc (K) (X) \leftrightarrow (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))$
38	36 37	bitr2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to ((oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X) \leftrightarrow X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)))$
39	33 38	anbi12d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \to ((oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X)) \leftrightarrow ((Y \underset{˙}{\land} oc (K) (p)) C Y \land X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p))))$
40	39	biimpa	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \land (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))) \to ((Y \underset{˙}{\land} oc (K) (p)) C Y \land X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)))$
41	40	ancomd	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \land (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))) \to (X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)) \land (Y \underset{˙}{\land} oc (K) (p)) C Y)$
42		oveq2	$⊢ w = oc (K) (p) \to Y \underset{˙}{\land} w = Y \underset{˙}{\land} oc (K) (p)$
43	42	breq2d	$⊢ w = oc (K) (p) \to (X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \leftrightarrow X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)))$
44	42	breq1d	$⊢ w = oc (K) (p) \to ((Y \underset{˙}{\land} w) C Y \leftrightarrow (Y \underset{˙}{\land} oc (K) (p)) C Y)$
45	43 44	anbi12d	$⊢ w = oc (K) (p) \to ((X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \land (Y \underset{˙}{\land} w) C Y) \leftrightarrow (X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)) \land (Y \underset{˙}{\land} oc (K) (p)) C Y))$
46	45	rspcev	$⊢ (oc (K) (p) \in H \land (X \underset{˙}{\leq} (Y \underset{˙}{\land} oc (K) (p)) \land (Y \underset{˙}{\land} oc (K) (p)) C Y)) \to \exists w \in H (X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \land (Y \underset{˙}{\land} w) C Y)$
47	16 41 46	syl2anc	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in Atoms (K)) \land (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))) \to \exists w \in H (X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \land (Y \underset{˙}{\land} w) C Y)$
48		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to K \in HL$
49	48 17	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to K \in OP$
50		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to Y \in B$
51	1 12	opoccl	$⊢ (K \in OP \land Y \in B) \to oc (K) (Y) \in B$
52	49 50 51	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to oc (K) (Y) \in B$
53		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \in B$
54	1 12	opoccl	$⊢ (K \in OP \land X \in B) \to oc (K) (X) \in B$
55	49 53 54	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to oc (K) (X) \in B$
56		simpr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{<} Y$
57	1 3 12	opltcon3b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow oc (K) (Y) \underset{˙}{<} oc (K) (X))$
58	49 53 50 57	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{<} Y \leftrightarrow oc (K) (Y) \underset{˙}{<} oc (K) (X))$
59	56 58	mpbid	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to oc (K) (Y) \underset{˙}{<} oc (K) (X)$
60	1 2 3 29 5 9	hlrelat3	$⊢ ((K \in HL \land oc (K) (Y) \in B \land oc (K) (X) \in B) \land oc (K) (Y) \underset{˙}{<} oc (K) (X)) \to \exists p \in Atoms (K) (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))$
61	48 52 55 59 60	syl31anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in Atoms (K) (oc (K) (Y) C (oc (K) (Y) join (K) p) \land (oc (K) (Y) join (K) p) \underset{˙}{\leq} oc (K) (X))$
62	47 61	r19.29a	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists w \in H (X \underset{˙}{\leq} (Y \underset{˙}{\land} w) \land (Y \underset{˙}{\land} w) C Y)$

Metamath Proof Explorer

Theorem lhprelat3N

Proof