Metamath Proof Explorer

Theorem lncvrelatN

Description: A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lncvrelat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lncvrelat.c ${⊢}{C}={⋖}_{{K}}$
lncvrelat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
lncvrelat.n ${⊢}{N}=\mathrm{Lines}\left({K}\right)$
lncvrelat.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
Assertion lncvrelatN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({M}\left({X}\right)\in {N}\wedge {P}{C}{X}\right)\right)\to {P}\in {A}$

Proof

Step Hyp Ref Expression
1 lncvrelat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lncvrelat.c ${⊢}{C}={⋖}_{{K}}$
3 lncvrelat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 lncvrelat.n ${⊢}{N}=\mathrm{Lines}\left({K}\right)$
5 lncvrelat.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
6 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
7 6 3ad2ant1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\to {K}\in \mathrm{Lat}$
8 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
9 8 3 4 5 isline2 ${⊢}{K}\in \mathrm{Lat}\to \left({M}\left({X}\right)\in {N}↔\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\exists {r}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}\ne {r}\wedge {M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)$
10 7 9 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\to \left({M}\left({X}\right)\in {N}↔\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\exists {r}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}\ne {r}\wedge {M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)$
11 simpll1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {K}\in \mathrm{HL}$
12 simpll2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {X}\in {B}$
13 11 6 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {K}\in \mathrm{Lat}$
14 simplrl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {q}\in {A}$
15 1 3 atbase ${⊢}{q}\in {A}\to {q}\in {B}$
16 14 15 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {q}\in {B}$
17 simplrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {r}\in {A}$
18 1 3 atbase ${⊢}{r}\in {A}\to {r}\in {B}$
19 17 18 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {r}\in {B}$
20 1 8 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge {q}\in {B}\wedge {r}\in {B}\right)\to {q}\mathrm{join}\left({K}\right){r}\in {B}$
21 13 16 19 20 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {q}\mathrm{join}\left({K}\right){r}\in {B}$
22 1 5 pmap11 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {q}\mathrm{join}\left({K}\right){r}\in {B}\right)\to \left({M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)↔{X}={q}\mathrm{join}\left({K}\right){r}\right)$
23 11 12 21 22 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to \left({M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)↔{X}={q}\mathrm{join}\left({K}\right){r}\right)$
24 breq2 ${⊢}{X}={q}\mathrm{join}\left({K}\right){r}\to \left({P}{C}{X}↔{P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)$
25 24 biimpd ${⊢}{X}={q}\mathrm{join}\left({K}\right){r}\to \left({P}{C}{X}\to {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)$
26 11 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to {K}\in \mathrm{HL}$
27 simpll3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to {P}\in {B}$
28 27 14 17 3jca ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to \left({P}\in {B}\wedge {q}\in {A}\wedge {r}\in {A}\right)$
29 28 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to \left({P}\in {B}\wedge {q}\in {A}\wedge {r}\in {A}\right)$
30 simplr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to {q}\ne {r}$
31 simpr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)$
32 1 8 2 3 cvrat2 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {B}\wedge {q}\in {A}\wedge {r}\in {A}\right)\wedge \left({q}\ne {r}\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\to {P}\in {A}$
33 26 29 30 31 32 syl112anc ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\wedge {P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to {P}\in {A}$
34 33 ex ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to \left({P}{C}\left({q}\mathrm{join}\left({K}\right){r}\right)\to {P}\in {A}\right)$
35 25 34 syl9r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to \left({X}={q}\mathrm{join}\left({K}\right){r}\to \left({P}{C}{X}\to {P}\in {A}\right)\right)$
36 23 35 sylbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\wedge {q}\ne {r}\right)\to \left({M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)\to \left({P}{C}{X}\to {P}\in {A}\right)\right)$
37 36 expimpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({q}\in {A}\wedge {r}\in {A}\right)\right)\to \left(\left({q}\ne {r}\wedge {M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to \left({P}{C}{X}\to {P}\in {A}\right)\right)$
38 37 rexlimdvva ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\to \left(\exists {q}\in {A}\phantom{\rule{.4em}{0ex}}\exists {r}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}\ne {r}\wedge {M}\left({X}\right)={M}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to \left({P}{C}{X}\to {P}\in {A}\right)\right)$
39 10 38 sylbid ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\to \left({M}\left({X}\right)\in {N}\to \left({P}{C}{X}\to {P}\in {A}\right)\right)$
40 39 imp32 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {P}\in {B}\right)\wedge \left({M}\left({X}\right)\in {N}\wedge {P}{C}{X}\right)\right)\to {P}\in {A}$