2lnat

Description: Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012)

	Ref	Expression
Hypotheses	2lnat.b	$⊢ B = {Base}_{K}$
	2lnat.m	$⊢ \underset{˙}{\land} = meet (K)$
	2lnat.z	$⊢ \underset{˙}{0} = 0. (K)$
	2lnat.a	$⊢ A = Atoms (K)$
	2lnat.n	$⊢ N = Lines (K)$
	2lnat.f	$⊢ F = pmap (K)$
Assertion	2lnat	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in A$

Proof

Step	Hyp	Ref	Expression
1		2lnat.b	$⊢ B = {Base}_{K}$
2		2lnat.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2lnat.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2lnat.a	$⊢ A = Atoms (K)$
5		2lnat.n	$⊢ N = Lines (K)$
6		2lnat.f	$⊢ F = pmap (K)$
7		simp11	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in HL$
8		hlatl	$⊢ K \in HL \to K \in AtLat$
9	7 8	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in AtLat$
10	7	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in Lat$
11		simp12	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \in B$
12		simp13	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to Y \in B$
13	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in B$
15		simp3r	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
16		eqid	$⊢ \leq_{K} = \leq_{K}$
17	1 16 3 4	atlex	$⊢ (K \in AtLat \land X \underset{˙}{\land} Y \in B \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \to \exists p \in A p \leq_{K} (X \underset{˙}{\land} Y)$
18	9 14 15 17	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to \exists p \in A p \leq_{K} (X \underset{˙}{\land} Y)$
19		simp13l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to X \neq Y$
20		simp11	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (K \in HL \land X \in B \land Y \in B)$
21		simp12l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to F (X) \in N$
22		simp12r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to F (Y) \in N$
23	1 16 5 6	lncmp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N)) \to (X \leq_{K} Y \leftrightarrow X = Y)$
24	20 21 22 23	syl12anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X \leq_{K} Y \leftrightarrow X = Y)$
25		simp111	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to K \in HL$
26	25	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to K \in Lat$
27		simp112	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to X \in B$
28		simp113	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to Y \in B$
29	1 16 2	latleeqm1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
30	26 27 28 29	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X \leq_{K} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
31	24 30	bitr3d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X = Y \leftrightarrow X \underset{˙}{\land} Y = X)$
32	31	necon3bid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X \neq Y \leftrightarrow X \underset{˙}{\land} Y \neq X)$
33	19 32	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to X \underset{˙}{\land} Y \neq X$
34		simp3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p \leq_{K} (X \underset{˙}{\land} Y)$
35	1 16 2	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} X$
36	26 27 28 35	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X \underset{˙}{\land} Y) \leq_{K} X$
37		hlpos	$⊢ K \in HL \to K \in Poset$
38	25 37	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to K \in Poset$
39	1 4	atbase	$⊢ p \in A \to p \in B$
40	39	3ad2ant2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p \in B$
41	26 27 28 13	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to X \underset{˙}{\land} Y \in B$
42		simp2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p \in A$
43	1 16 26 40 41 27 34 36	lattrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p \leq_{K} X$
44		eqid	$⊢ ⋖_{K} = ⋖_{K}$
45	1 16 44 4 5 6	lncvrat	$⊢ ((K \in HL \land X \in B \land p \in A) \land (F (X) \in N \land p \leq_{K} X)) \to p ⋖_{K} X$
46	25 27 42 21 43 45	syl32anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p ⋖_{K} X$
47	1 16 44	cvrnbtwn4	$⊢ (K \in Poset \land (p \in B \land X \in B \land X \underset{˙}{\land} Y \in B) \land p ⋖_{K} X) \to ((p \leq_{K} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \leq_{K} X) \leftrightarrow (p = X \underset{˙}{\land} Y \lor X \underset{˙}{\land} Y = X))$
48	38 40 27 41 46 47	syl131anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to ((p \leq_{K} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \leq_{K} X) \leftrightarrow (p = X \underset{˙}{\land} Y \lor X \underset{˙}{\land} Y = X))$
49	34 36 48	mpbi2and	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (p = X \underset{˙}{\land} Y \lor X \underset{˙}{\land} Y = X)$
50		neor	$⊢ (p = X \underset{˙}{\land} Y \lor X \underset{˙}{\land} Y = X) \leftrightarrow (p \neq X \underset{˙}{\land} Y \to X \underset{˙}{\land} Y = X)$
51	49 50	sylib	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (p \neq X \underset{˙}{\land} Y \to X \underset{˙}{\land} Y = X)$
52	51	necon1d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to (X \underset{˙}{\land} Y \neq X \to p = X \underset{˙}{\land} Y)$
53	33 52	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \land p \in A \land p \leq_{K} (X \underset{˙}{\land} Y)) \to p = X \underset{˙}{\land} Y$
54	53	3exp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to (p \in A \to (p \leq_{K} (X \underset{˙}{\land} Y) \to p = X \underset{˙}{\land} Y))$
55	54	reximdvai	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to (\exists p \in A p \leq_{K} (X \underset{˙}{\land} Y) \to \exists p \in A p = X \underset{˙}{\land} Y)$
56	18 55	mpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to \exists p \in A p = X \underset{˙}{\land} Y$
57		risset	$⊢ X \underset{˙}{\land} Y \in A \leftrightarrow \exists p \in A p = X \underset{˙}{\land} Y$
58	56 57	sylibr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (F (X) \in N \land F (Y) \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in A$

Metamath Proof Explorer

Theorem 2lnat

Proof