Metamath Proof Explorer

Theorem lhpmat

Description: An element covered by the lattice unity, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses lhpmat.l ⊢ ≤ ˙ = ≤ K
lhpmat.m ⊢ ∧ ˙ = meet ⁡ K
lhpmat.z ⊢ 0 ˙ = 0. ⁡ K
lhpmat.a ⊢ A = Atoms ⁡ K
lhpmat.h ⊢ H = LHyp ⁡ K
Assertion lhpmat ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∧ ˙ W = 0 ˙

Proof

Step Hyp Ref Expression
1 lhpmat.l ⊢ ≤ ˙ = ≤ K
2 lhpmat.m ⊢ ∧ ˙ = meet ⁡ K
3 lhpmat.z ⊢ 0 ˙ = 0. ⁡ K
4 lhpmat.a ⊢ A = Atoms ⁡ K
5 lhpmat.h ⊢ H = LHyp ⁡ K
6 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ¬ P ≤ ˙ W
7 hlatl ⊢ K ∈ HL → K ∈ AtLat
8 7 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ AtLat
9 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ A
10 eqid ⊢ Base K = Base K
11 10 5 lhpbase ⊢ W ∈ H → W ∈ Base K
12 11 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ Base K
13 10 1 2 3 4 atnle ⊢ K ∈ AtLat ∧ P ∈ A ∧ W ∈ Base K → ¬ P ≤ ˙ W ↔ P ∧ ˙ W = 0 ˙
14 8 9 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ¬ P ≤ ˙ W ↔ P ∧ ˙ W = 0 ˙
15 6 14 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∧ ˙ W = 0 ˙