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 = Base K
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 ∧ ˙ W C X

Proof

Step Hyp Ref Expression
1 lhpmcvr.b ⊢ B = Base K
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 → W C 1. ⁡ K
15 14 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W C 1. ⁡ K
16 eqid ⊢ join ⁡ K = join ⁡ K
17 1 2 16 13 5 lhpj1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W join ⁡ K X = 1. ⁡ K
18 15 17 breqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W C W join ⁡ K X
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 ∧ ˙ X C X ↔ W C W join ⁡ K X
21 19 10 8 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W ∧ ˙ X C X ↔ W C W join ⁡ K X
22 18 21 mpbird ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W ∧ ˙ X C X
23 12 22 eqbrtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → X ∧ ˙ W C X