# 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}={\mathrm{Base}}_{{K}}$
2lnat.m
2lnat.z
2lnat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2lnat.n ${⊢}{N}=\mathrm{Lines}\left({K}\right)$
2lnat.f ${⊢}{F}=\mathrm{pmap}\left({K}\right)$
Assertion 2lnat

### Proof

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