2llnm4

Description: Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012)

	Ref	Expression
Hypotheses	2llnm4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnm4.m	$⊢ \underset{˙}{\land} = meet (K)$
	2llnm4.z	$⊢ \underset{˙}{0} = 0. (K)$
	2llnm4.a	$⊢ A = Atoms (K)$
	2llnm4.n	$⊢ N = LLines (K)$
Assertion	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 \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		2llnm4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnm4.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2llnm4.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2llnm4.a	$⊢ A = Atoms (K)$
5		2llnm4.n	$⊢ N = LLines (K)$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	3ad2ant1	$⊢ (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 K \in AtLat$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	8	3ad2ant1	$⊢ (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 K \in Lat$
10		simp22	$⊢ (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 \in N$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 5	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
13	10 12	syl	$⊢ (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 \in {Base}_{K}$
14		simp23	$⊢ (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 Y \in N$
15	11 5	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
16	14 15	syl	$⊢ (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 Y \in {Base}_{K}$
17	11 2	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
18	9 13 16 17	syl3anc	$⊢ (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 \in {Base}_{K}$
19		simp21	$⊢ (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 P \in A$
20		simp3	$⊢ (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 (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y)$
21	11 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
22	19 21	syl	$⊢ (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 P \in {Base}_{K}$
23	11 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))$
24	9 22 13 16 23	syl13anc	$⊢ (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 ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
25	20 24	mpbid	$⊢ (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 P \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
26	11 1 3 4	atlen0	$⊢ ((K \in AtLat \land X \underset{˙}{\land} Y \in {Base}_{K} \land P \in A) \land P \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
27	7 18 19 25 26	syl31anc	$⊢ (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 \underset{˙}{0}$

Metamath Proof Explorer

Theorem 2llnm4

Proof