hlrelat

Description: A Hilbert lattice is relatively atomic. Remark 2 of Kalmbach p. 149. ( chrelati analog.) (Contributed by NM, 4-Feb-2012)

	Ref	Expression
Hypotheses	hlrelat5.b	$⊢ B = {Base}_{K}$
	hlrelat5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	hlrelat5.s	$⊢ \underset{˙}{<} = <_{K}$
	hlrelat5.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlrelat5.a	$⊢ A = Atoms (K)$
Assertion	hlrelat	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (X \underset{˙}{<} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$

Proof

Step	Hyp	Ref	Expression
1		hlrelat5.b	$⊢ B = {Base}_{K}$
2		hlrelat5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		hlrelat5.s	$⊢ \underset{˙}{<} = <_{K}$
4		hlrelat5.j	$⊢ \underset{˙}{\lor} = join (K)$
5		hlrelat5.a	$⊢ A = Atoms (K)$
6	1 2 3 5	hlrelat1	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y))$
7	6	imp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
8		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to K \in HL$
9	8	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to K \in Lat$
10		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to X \in B$
11	1 5	atbase	$⊢ p \in A \to p \in B$
12	11	adantl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to p \in B$
13	1 2 3 4	latnle	$⊢ (K \in Lat \land X \in B \land p \in B) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{<} (X \underset{˙}{\lor} p))$
14	9 10 12 13	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{<} (X \underset{˙}{\lor} p))$
15	2 3	pltle	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \underset{˙}{\leq} Y)$
16	15	imp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{\leq} Y$
17	16	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to X \underset{˙}{\leq} Y$
18	17	biantrurd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to (p \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\leq} Y \land p \underset{˙}{\leq} Y))$
19		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to Y \in B$
20	1 2 4	latjle12	$⊢ (K \in Lat \land (X \in B \land p \in B \land Y \in B)) \to ((X \underset{˙}{\leq} Y \land p \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
21	9 10 12 19 20	syl13anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to ((X \underset{˙}{\leq} Y \land p \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
22	18 21	bitrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to (p \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
23	14 22	anbi12d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A) \to ((\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{<} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y))$
24	23	rexbidva	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (\exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \leftrightarrow \exists p \in A (X \underset{˙}{<} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y))$
25	7 24	mpbid	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (X \underset{˙}{<} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$

Metamath Proof Explorer

Theorem hlrelat

Proof