# Metamath Proof Explorer

## Theorem isline3

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012)

Ref Expression
Hypotheses isline3.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
isline3.j
isline3.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
isline3.n ${⊢}{N}=\mathrm{Lines}\left({K}\right)$
isline3.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
Assertion isline3

### Proof

Step Hyp Ref Expression
1 isline3.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 isline3.j
3 isline3.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 isline3.n ${⊢}{N}=\mathrm{Lines}\left({K}\right)$
5 isline3.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
6 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
7 6 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\to {K}\in \mathrm{Lat}$
8 2 3 4 5 isline2
9 7 8 syl
10 simpll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\right)\to {K}\in \mathrm{HL}$
11 simplr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\right)\to {X}\in {B}$
12 6 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\right)\to {K}\in \mathrm{Lat}$
13 1 3 atbase ${⊢}{p}\in {A}\to {p}\in {B}$
14 13 ad2antrl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\right)\to {p}\in {B}$
15 1 3 atbase ${⊢}{q}\in {A}\to {q}\in {B}$
16 15 ad2antll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\right)\to {q}\in {B}$
17 1 2 latjcl
18 12 14 16 17 syl3anc
19 1 5 pmap11
20 10 11 18 19 syl3anc
21 20 anbi2d
22 21 2rexbidva
23 9 22 bitrd