atlelt

Description: Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012)

	Ref	Expression
Hypotheses	atlelt.b	$⊢ B = {Base}_{K}$
	atlelt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlelt.s	$⊢ \underset{˙}{<} = <_{K}$
	atlelt.a	$⊢ A = Atoms (K)$
Assertion	atlelt	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P \underset{˙}{<} X$

Proof

Step	Hyp	Ref	Expression
1		atlelt.b	$⊢ B = {Base}_{K}$
2		atlelt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlelt.s	$⊢ \underset{˙}{<} = <_{K}$
4		atlelt.a	$⊢ A = Atoms (K)$
5		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to Q \underset{˙}{<} X$
6		breq1	$⊢ P = Q \to (P \underset{˙}{<} X \leftrightarrow Q \underset{˙}{<} X)$
7	5 6	syl5ibrcom	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (P = Q \to P \underset{˙}{<} X)$
8		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to K \in HL$
9		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P \in A$
10		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to Q \in A$
11		eqid	$⊢ join (K) = join (K)$
12	3 11 4	atlt	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \underset{˙}{<} (P join (K) Q) \leftrightarrow P \neq Q)$
13	8 9 10 12	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (P \underset{˙}{<} (P join (K) Q) \leftrightarrow P \neq Q)$
14		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P \underset{˙}{\leq} X$
15		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to X \in B$
16	8 10 15	3jca	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (K \in HL \land Q \in A \land X \in B)$
17	2 3	pltle	$⊢ (K \in HL \land Q \in A \land X \in B) \to (Q \underset{˙}{<} X \to Q \underset{˙}{\leq} X)$
18	16 5 17	sylc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to Q \underset{˙}{\leq} X$
19		hllat	$⊢ K \in HL \to K \in Lat$
20	19	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to K \in Lat$
21	1 4	atbase	$⊢ P \in A \to P \in B$
22	9 21	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P \in B$
23	1 4	atbase	$⊢ Q \in A \to Q \in B$
24	10 23	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to Q \in B$
25	1 2 11	latjle12	$⊢ (K \in Lat \land (P \in B \land Q \in B \land X \in B)) \to ((P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} X) \leftrightarrow (P join (K) Q) \underset{˙}{\leq} X)$
26	20 22 24 15 25	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to ((P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} X) \leftrightarrow (P join (K) Q) \underset{˙}{\leq} X)$
27	14 18 26	mpbi2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (P join (K) Q) \underset{˙}{\leq} X$
28		hlpos	$⊢ K \in HL \to K \in Poset$
29	28	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to K \in Poset$
30	1 11	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P join (K) Q \in B$
31	20 22 24 30	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P join (K) Q \in B$
32	1 2 3	pltletr	$⊢ (K \in Poset \land (P \in B \land P join (K) Q \in B \land X \in B)) \to ((P \underset{˙}{<} (P join (K) Q) \land (P join (K) Q) \underset{˙}{\leq} X) \to P \underset{˙}{<} X)$
33	29 22 31 15 32	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to ((P \underset{˙}{<} (P join (K) Q) \land (P join (K) Q) \underset{˙}{\leq} X) \to P \underset{˙}{<} X)$
34	27 33	mpan2d	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (P \underset{˙}{<} (P join (K) Q) \to P \underset{˙}{<} X)$
35	13 34	sylbird	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to (P \neq Q \to P \underset{˙}{<} X)$
36	7 35	pm2.61dne	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{<} X)) \to P \underset{˙}{<} X$

Metamath Proof Explorer

Theorem atlelt

Proof