2llnmeqat

Description: An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013)

	Ref	Expression
Hypotheses	2llnmeqat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnmeqat.m	$⊢ \underset{˙}{\land} = meet (K)$
	2llnmeqat.a	$⊢ A = Atoms (K)$
	2llnmeqat.n	$⊢ N = LLines (K)$
Assertion	2llnmeqat	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to P = X \underset{˙}{\land} Y$

Proof

Step	Hyp	Ref	Expression
1		2llnmeqat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnmeqat.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2llnmeqat.a	$⊢ A = Atoms (K)$
4		2llnmeqat.n	$⊢ N = LLines (K)$
5		simp3r	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to P \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	3ad2ant1	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to K \in AtLat$
8		simp23	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to P \in A$
9		simp1	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to K \in HL$
10		simp21	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \in N$
11		simp22	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to Y \in N$
12		simp3l	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \neq Y$
13		hllat	$⊢ K \in HL \to K \in Lat$
14	13	3ad2ant1	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to K \in Lat$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	8 16	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to P \in {Base}_{K}$
18	15 4	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
19	10 18	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \in {Base}_{K}$
20	15 4	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
21	11 20	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to Y \in {Base}_{K}$
22	15 1 2	latlem12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land X \in {Base}_{K} \land Y \in {Base}_{K})) \to ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
23	14 17 19 21 22	syl13anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
24	5 23	mpbird	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y)$
25		eqid	$⊢ 0. (K) = 0. (K)$
26	1 2 25 3 4	2llnm4	$⊢ (K \in HL \land (P \in A \land X \in N \land Y \in N) \land (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y)) \to X \underset{˙}{\land} Y \neq 0. (K)$
27	9 8 10 11 24 26	syl131anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \underset{˙}{\land} Y \neq 0. (K)$
28	2 25 3 4	2llnmat	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq 0. (K))) \to X \underset{˙}{\land} Y \in A$
29	9 10 11 12 27 28	syl32anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \underset{˙}{\land} Y \in A$
30	1 3	atcmp	$⊢ (K \in AtLat \land P \in A \land X \underset{˙}{\land} Y \in A) \to (P \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow P = X \underset{˙}{\land} Y)$
31	7 8 29 30	syl3anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to (P \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow P = X \underset{˙}{\land} Y)$
32	5 31	mpbid	$⊢ (K \in HL \land (X \in N \land Y \in N \land P \in A) \land (X \neq Y \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to P = X \underset{˙}{\land} Y$

Metamath Proof Explorer

Theorem 2llnmeqat

Proof