This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhpmcvr2

Description: Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses lhpmcvr2.b ⊢ B = Base K
lhpmcvr2.l ⊢ ≤ ˙ = ≤ K
lhpmcvr2.j ⊢ ∨ ˙ = join ⁡ K
lhpmcvr2.m ⊢ ∧ ˙ = meet ⁡ K
lhpmcvr2.a ⊢ A = Atoms ⁡ K
lhpmcvr2.h ⊢ H = LHyp ⁡ K
Assertion lhpmcvr2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → ∃ p ∈ A ¬ p ≤ ˙ W ∧ p ∨ ˙ X ∧ ˙ W = X

Proof

Step Hyp Ref Expression
1 lhpmcvr2.b ⊢ B = Base K
2 lhpmcvr2.l ⊢ ≤ ˙ = ≤ K
3 lhpmcvr2.j ⊢ ∨ ˙ = join ⁡ K
4 lhpmcvr2.m ⊢ ∧ ˙ = meet ⁡ K
5 lhpmcvr2.a ⊢ A = Atoms ⁡ K
6 lhpmcvr2.h ⊢ H = LHyp ⁡ K
7 eqid ⊢ ⋖ K = ⋖ K
8 1 2 4 7 6 lhpmcvr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → X ∧ ˙ W ⋖ K X
9 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → K ∈ HL
10 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → X ∈ B
11 1 6 lhpbase ⊢ W ∈ H → W ∈ B
12 11 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W ∈ B
13 1 2 3 4 7 5 cvrval5 ⊢ K ∈ HL ∧ X ∈ B ∧ W ∈ B → X ∧ ˙ W ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ W ∧ p ∨ ˙ X ∧ ˙ W = X
14 9 10 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → X ∧ ˙ W ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ W ∧ p ∨ ˙ X ∧ ˙ W = X
15 8 14 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → ∃ p ∈ A ¬ p ≤ ˙ W ∧ p ∨ ˙ X ∧ ˙ W = X