Metamath Proof Explorer


Theorem 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 ˙ = meet K
2lnat.z 0 ˙ = 0. K
2lnat.a A = Atoms K
2lnat.n N = Lines K
2lnat.f F = pmap K
Assertion 2lnat K HL X B Y B F X N F Y N X Y X ˙ Y 0 ˙ X ˙ Y A

Proof

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