# Metamath Proof Explorer

## Theorem lnnat

Description: A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses lnnat.j
lnnat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion lnnat

### Proof

Step Hyp Ref Expression
1 lnnat.j
2 lnnat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 simpl1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {K}\in \mathrm{HL}$
4 simpl2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {P}\in {A}$
5 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
6 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
7 5 6 2 atcvr0 ${⊢}\left({K}\in \mathrm{HL}\wedge {P}\in {A}\right)\to \mathrm{0.}\left({K}\right){⋖}_{{K}}{P}$
8 3 4 7 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to \mathrm{0.}\left({K}\right){⋖}_{{K}}{P}$
9 1 6 2 atcvr1
10 9 biimpa
11 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
12 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
13 12 5 op0cl ${⊢}{K}\in \mathrm{OP}\to \mathrm{0.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
14 3 11 13 3syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to \mathrm{0.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
15 12 2 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
16 4 15 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {P}\in {\mathrm{Base}}_{{K}}$
17 3 hllatd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {K}\in \mathrm{Lat}$
18 simpl3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {Q}\in {A}$
19 12 2 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
20 18 19 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {Q}\in {\mathrm{Base}}_{{K}}$
21 12 1 latjcl
22 17 16 20 21 syl3anc
23 12 6 cvrntr
24 3 14 16 22 23 syl13anc
25 8 10 24 mp2and
26 simpll1
27 5 6 2 atcvr0
28 26 27 sylancom
29 25 28 mtand
30 29 ex
31 1 2 hlatjidm
33 simp2 ${⊢}\left({K}\in \mathrm{HL}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\to {P}\in {A}$