# Metamath Proof Explorer

## Theorem lhpmcvr

Description: The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses lhpmcvr.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lhpmcvr.l
lhpmcvr.m
lhpmcvr.c ${⊢}{C}={⋖}_{{K}}$
lhpmcvr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhpmcvr

### Proof

Step Hyp Ref Expression
1 lhpmcvr.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lhpmcvr.l
3 lhpmcvr.m
4 lhpmcvr.c ${⊢}{C}={⋖}_{{K}}$
5 lhpmcvr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
8 simprl
9 1 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
11 1 3 latmcom
12 7 8 10 11 syl3anc
13 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
14 13 4 5 lhp1cvr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {W}{C}\mathrm{1.}\left({K}\right)$
16 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
17 1 2 16 13 5 lhpj1
18 15 17 breqtrrd
19 simpll
20 1 16 3 4 cvrexch
21 19 10 8 20 syl3anc
22 18 21 mpbird
23 12 22 eqbrtrd