Metamath Proof Explorer

Theorem meetat

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012)

Ref Expression
Hypotheses m.b ⊢ B = Base K
m.m ⊢ ∧ ˙ = meet ⁡ K
m.z ⊢ 0 ˙ = 0. ⁡ K
m.a ⊢ A = Atoms ⁡ K
Assertion meetat ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∧ ˙ P = P ∨ X ∧ ˙ P = 0 ˙

Proof

Step Hyp Ref Expression
1 m.b ⊢ B = Base K
2 m.m ⊢ ∧ ˙ = meet ⁡ K
3 m.z ⊢ 0 ˙ = 0. ⁡ K
4 m.a ⊢ A = Atoms ⁡ K
5 ollat ⊢ K ∈ OL → K ∈ Lat
6 5 3ad2ant1 ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → K ∈ Lat
7 simp2 ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∈ B
8 simp3 ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → P ∈ A
9 1 4 atbase ⊢ P ∈ A → P ∈ B
10 8 9 syl ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → P ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 latmle2 ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∈ B → X ∧ ˙ P ≤ K P
13 6 7 10 12 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∧ ˙ P ≤ K P
14 olop ⊢ K ∈ OL → K ∈ OP
15 14 3ad2ant1 ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → K ∈ OP
16 1 2 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∈ B → X ∧ ˙ P ∈ B
17 6 7 10 16 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∧ ˙ P ∈ B
18 1 11 3 4 leatb ⊢ K ∈ OP ∧ X ∧ ˙ P ∈ B ∧ P ∈ A → X ∧ ˙ P ≤ K P ↔ X ∧ ˙ P = P ∨ X ∧ ˙ P = 0 ˙
19 15 17 8 18 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∧ ˙ P ≤ K P ↔ X ∧ ˙ P = P ∨ X ∧ ˙ P = 0 ˙
20 13 19 mpbid ⊢ K ∈ OL ∧ X ∈ B ∧ P ∈ A → X ∧ ˙ P = P ∨ X ∧ ˙ P = 0 ˙