# Metamath Proof Explorer

## Theorem atcvrlln

Description: An element covering an atom is a lattice line and vice-versa. (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses atcvrlln.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
atcvrlln.c ${⊢}{C}={⋖}_{{K}}$
atcvrlln.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
atcvrlln.n ${⊢}{N}=\mathrm{LLines}\left({K}\right)$
Assertion atcvrlln ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\to \left({X}\in {A}↔{Y}\in {N}\right)$

### Proof

Step Hyp Ref Expression
1 atcvrlln.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 atcvrlln.c ${⊢}{C}={⋖}_{{K}}$
3 atcvrlln.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 atcvrlln.n ${⊢}{N}=\mathrm{LLines}\left({K}\right)$
5 simpll1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {X}\in {A}\right)\to {K}\in \mathrm{HL}$
6 simpll3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {X}\in {A}\right)\to {Y}\in {B}$
7 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {X}\in {A}\right)\to {X}\in {A}$
8 simplr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {X}\in {A}\right)\to {X}{C}{Y}$
9 1 2 3 4 llni ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {Y}\in {B}\wedge {X}\in {A}\right)\wedge {X}{C}{Y}\right)\to {Y}\in {N}$
10 5 6 7 8 9 syl31anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {X}\in {A}\right)\to {Y}\in {N}$
11 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to {Y}\in {N}$
12 simpll1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to {K}\in \mathrm{HL}$
13 simpll3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to {Y}\in {B}$
14 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
15 1 14 3 4 islln3 ${⊢}\left({K}\in \mathrm{HL}\wedge {Y}\in {B}\right)\to \left({Y}\in {N}↔\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)$
16 12 13 15 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to \left({Y}\in {N}↔\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)$
17 11 16 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to \exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)$
18 simp1l1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {K}\in \mathrm{HL}$
19 simp1l2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {X}\in {B}$
20 simp2l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {p}\in {A}$
21 simp2r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {q}\in {A}$
22 simp3l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {p}\ne {q}$
23 simp1r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {X}{C}{Y}$
24 simp3r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {Y}={p}\mathrm{join}\left({K}\right){q}$
25 23 24 breqtrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {X}{C}\left({p}\mathrm{join}\left({K}\right){q}\right)$
26 1 14 2 3 cvrat2 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {X}{C}\left({p}\mathrm{join}\left({K}\right){q}\right)\right)\right)\to {X}\in {A}$
27 18 19 20 21 22 25 26 syl132anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge \left({p}\in {A}\wedge {q}\in {A}\right)\wedge \left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\right)\to {X}\in {A}$
28 27 3exp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\to \left(\left({p}\in {A}\wedge {q}\in {A}\right)\to \left(\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\to {X}\in {A}\right)\right)$
29 28 rexlimdvv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\to \left(\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\to {X}\in {A}\right)$
30 29 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to \left(\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({p}\ne {q}\wedge {Y}={p}\mathrm{join}\left({K}\right){q}\right)\to {X}\in {A}\right)$
31 17 30 mpd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\wedge {Y}\in {N}\right)\to {X}\in {A}$
32 10 31 impbida ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}{C}{Y}\right)\to \left({X}\in {A}↔{Y}\in {N}\right)$