2llnmat

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

	Ref	Expression
Hypotheses	2llnmat.m	$⊢ \underset{˙}{\land} = meet (K)$
	2llnmat.z	$⊢ \underset{˙}{0} = 0. (K)$
	2llnmat.a	$⊢ A = Atoms (K)$
	2llnmat.n	$⊢ N = LLines (K)$
Assertion	2llnmat	$⊢ ((K \in HL \land X \in N \land 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		2llnmat.m	$⊢ \underset{˙}{\land} = meet (K)$
2		2llnmat.z	$⊢ \underset{˙}{0} = 0. (K)$
3		2llnmat.a	$⊢ A = Atoms (K)$
4		2llnmat.n	$⊢ N = LLines (K)$
5		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in HL$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	5 6	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in AtLat$
8	5	hllatd	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to K \in Lat$
9		simpl2	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \in N$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 4	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
12	9 11	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \in {Base}_{K}$
13		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to Y \in N$
14	10 4	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to Y \in {Base}_{K}$
16	10 1	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
17	8 12 15 16	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in {Base}_{K}$
18		simprr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \neq Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	10 19 2 3	atlex	$⊢ (K \in AtLat \land X \underset{˙}{\land} Y \in {Base}_{K} \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \to \exists p \in A p \leq_{K} (X \underset{˙}{\land} Y)$
21	7 17 18 20	syl3anc	$⊢ ((K \in HL \land X \in N \land 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)$
22		simp1rl	$⊢ (((K \in HL \land X \in N \land 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$
23		simp1l	$⊢ (((K \in HL \land X \in N \land 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 N \land Y \in N)$
24	19 4	llncmp	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \leq_{K} Y \leftrightarrow X = Y)$
25	23 24	syl	$⊢ (((K \in HL \land X \in N \land 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)$
26		simp1l1	$⊢ (((K \in HL \land X \in N \land 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$
27	26	hllatd	$⊢ (((K \in HL \land X \in N \land 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$
28		simp1l2	$⊢ (((K \in HL \land X \in N \land 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 N$
29	28 11	syl	$⊢ (((K \in HL \land X \in N \land 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 {Base}_{K}$
30		simp1l3	$⊢ (((K \in HL \land X \in N \land 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 N$
31	30 14	syl	$⊢ (((K \in HL \land X \in N \land 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 {Base}_{K}$
32	10 19 1	latleeqm1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \leq_{K} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
33	27 29 31 32	syl3anc	$⊢ (((K \in HL \land X \in N \land 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)$
34	25 33	bitr3d	$⊢ (((K \in HL \land X \in N \land 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)$
35	34	necon3bid	$⊢ (((K \in HL \land X \in N \land 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)$
36	22 35	mpbid	$⊢ (((K \in HL \land X \in N \land 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$
37		simp3	$⊢ (((K \in HL \land X \in N \land 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)$
38	10 19 1	latmle1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\land} Y) \leq_{K} X$
39	27 29 31 38	syl3anc	$⊢ (((K \in HL \land X \in N \land 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$
40		hlpos	$⊢ K \in HL \to K \in Poset$
41	26 40	syl	$⊢ (((K \in HL \land X \in N \land 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$
42	10 3	atbase	$⊢ p \in A \to p \in {Base}_{K}$
43	42	3ad2ant2	$⊢ (((K \in HL \land X \in N \land 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 {Base}_{K}$
44	27 29 31 16	syl3anc	$⊢ (((K \in HL \land X \in N \land 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 {Base}_{K}$
45		simp2	$⊢ (((K \in HL \land X \in N \land 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$
46	10 19 27 43 44 29 37 39	lattrd	$⊢ (((K \in HL \land X \in N \land 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$
47		eqid	$⊢ ⋖_{K} = ⋖_{K}$
48	19 47 3 4	atcvrlln2	$⊢ ((K \in HL \land p \in A \land X \in N) \land p \leq_{K} X) \to p ⋖_{K} X$
49	26 45 28 46 48	syl31anc	$⊢ (((K \in HL \land X \in N \land 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$
50	10 19 47	cvrnbtwn4	$⊢ (K \in Poset \land (p \in {Base}_{K} \land X \in {Base}_{K} \land X \underset{˙}{\land} Y \in {Base}_{K}) \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))$
51	41 43 29 44 49 50	syl131anc	$⊢ (((K \in HL \land X \in N \land 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))$
52	37 39 51	mpbi2and	$⊢ (((K \in HL \land X \in N \land 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)$
53		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)$
54	52 53	sylib	$⊢ (((K \in HL \land X \in N \land 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)$
55	54	necon1d	$⊢ (((K \in HL \land X \in N \land 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)$
56	36 55	mpd	$⊢ (((K \in HL \land X \in N \land 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$
57	56	3exp	$⊢ ((K \in HL \land X \in N \land 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))$
58	57	reximdvai	$⊢ ((K \in HL \land X \in N \land 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)$
59	21 58	mpd	$⊢ ((K \in HL \land X \in N \land 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$
60		risset	$⊢ X \underset{˙}{\land} Y \in A \leftrightarrow \exists p \in A p = X \underset{˙}{\land} Y$
61	59 60	sylibr	$⊢ ((K \in HL \land X \in N \land 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 2llnmat

Proof