# Metamath Proof Explorer

## Theorem lhpj1

Description: The join of a co-atom (hyperplane) and an element not under it is the lattice unit. (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses lhpj1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lhpj1.l
lhpj1.j
lhpj1.u
lhpj1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhpj1

### Proof

Step Hyp Ref Expression
1 lhpj1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lhpj1.l
3 lhpj1.j
4 lhpj1.u
5 lhpj1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 simpll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {K}\in \mathrm{HL}$
7 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {X}\in {B}$
8 1 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
9 8 ad2antlr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {W}\in {B}$
10 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
11 1 2 10 hlrelat2
12 6 7 9 11 syl3anc
13 simp1l
14 simp2
15 simp3r
16 2 3 4 10 5 lhpjat1
17 13 14 15 16 syl12anc
18 simp3l
19 simp1ll
20 19 hllatd
21 1 10 atbase ${⊢}{p}\in \mathrm{Atoms}\left({K}\right)\to {p}\in {B}$
23 simp1r
25 1 2 3 latjlej2
26 20 22 23 24 25 syl13anc
27 18 26 mpd
28 17 27 eqbrtrrd
29 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
30 19 29 syl
31 1 3 latjcl
32 20 24 23 31 syl3anc
33 1 2 4 op1le
34 30 32 33 syl2anc
35 28 34 mpbid
36 35 rexlimdv3a
37 12 36 sylbid
38 37 impr