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=BaseK
lhpmcvr.l ⊢≤˙=≤K
lhpmcvr.m ⊢∧˙=meet⁡K
lhpmcvr.c ⊢C=⋖K
lhpmcvr.h ⊢H=LHyp⁡K
Assertion lhpmcvr ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→X∧˙WCX

Proof

Step Hyp Ref Expression
1 lhpmcvr.b ⊢B=BaseK
2 lhpmcvr.l ⊢≤˙=≤K
3 lhpmcvr.m ⊢∧˙=meet⁡K
4 lhpmcvr.c ⊢C=⋖K
5 lhpmcvr.h ⊢H=LHyp⁡K
6 hllat ⊢K∈HL→K∈Lat
7 6 ad2antrr ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→K∈Lat
8 simprl ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→X∈B
9 1 5 lhpbase ⊢W∈H→W∈B
10 9 ad2antlr ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→W∈B
11 1 3 latmcom ⊢K∈Lat∧X∈B∧W∈B→X∧˙W=W∧˙X
12 7 8 10 11 syl3anc ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→X∧˙W=W∧˙X
13 eqid ⊢1.⁡K=1.⁡K
14 13 4 5 lhp1cvr ⊢K∈HL∧W∈H→WC1.⁡K
15 14 adantr ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→WC1.⁡K
16 eqid ⊢join⁡K=join⁡K
17 1 2 16 13 5 lhpj1 ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→Wjoin⁡KX=1.⁡K
18 15 17 breqtrrd ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→WCWjoin⁡KX
19 simpll ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→K∈HL
20 1 16 3 4 cvrexch ⊢K∈HL∧W∈B∧X∈B→W∧˙XCX↔WCWjoin⁡KX
21 19 10 8 20 syl3anc ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→W∧˙XCX↔WCWjoin⁡KX
22 18 21 mpbird ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→W∧˙XCX
23 12 22 eqbrtrd ⊢K∈HL∧W∈H∧X∈B∧¬X≤˙W→X∧˙WCX