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

Metamath Proof Explorer

Theorem atl0cl

Description: An atomic lattice has a zero element. We can use this in place of op0cl for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses atl0cl.b ⊢ B = Base K
atl0cl.z ⊢ 0 ˙ = 0. ⁡ K
Assertion atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 atl0cl.b ⊢ B = Base K
2 atl0cl.z ⊢ 0 ˙ = 0. ⁡ K
3 eqid ⊢ glb ⁡ K = glb ⁡ K
4 1 3 2 p0val ⊢ K ∈ AtLat → 0 ˙ = glb ⁡ K ⁡ B
5 id ⊢ K ∈ AtLat → K ∈ AtLat
6 eqid ⊢ lub ⁡ K = lub ⁡ K
7 1 6 3 atl0dm ⊢ K ∈ AtLat → B ∈ dom ⁡ glb ⁡ K
8 1 3 5 7 glbcl ⊢ K ∈ AtLat → glb ⁡ K ⁡ B ∈ B
9 4 8 eqeltrd ⊢ K ∈ AtLat → 0 ˙ ∈ B