P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	omlop 38601	An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
Theorem	omllat 38602	An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
Theorem	omllaw 38603	The orthomodular law. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
Theorem	omllaw2N 38604	Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 31307 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌))
Theorem	omllaw3 38605	Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 31158 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌))
Theorem	omllaw4 38606	Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋))
Theorem	omllaw5N 38607	The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 31335 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
Theorem	cmtcomlemN 38608	Lemma for cmtcomN 38609. (cmcmlem 31313 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋))
Theorem	cmtcomN 38609	Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 31314 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋))
Theorem	cmt2N 38610	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 31315 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌)))
Theorem	cmt3N 38611	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31317 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌))
Theorem	cmt4N 38612	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31317 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌)))
Theorem	cmtbr2N 38613	Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 31318 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌)))))
Theorem	cmtbr3N 38614	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 31330 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
Theorem	cmtbr4N 38615	Alternate definition for the commutes relation. (cmbr4i 31323 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌))
Theorem	lecmtN 38616	Ordered elements commute. (lecmi 31324 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌))
Theorem	cmtidN 38617	Any element commutes with itself. (cmidi 31332 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋)
Theorem	omlfh1N 38618	Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 31340 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))
Theorem	omlfh3N 38619	Foulis-Holland Theorem, part 3. Dual of omlfh1N 38618. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍)))
Theorem	omlmod1i2N 38620	Analogue of modular law atmod1i2 39220 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ 𝑍))
Theorem	omlspjN 38621	Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋)
21.26.10  Atomic lattices with covering property
Syntax	ccvr 38622	Extend class notation with covers relation.
class ⋖
Syntax	catm 38623	Extend class notation with atoms.
class Atoms
Syntax	cal 38624	Extend class notation with atomic lattices.
class AtLat
Syntax	clc 38625	Extend class notation with lattices with the covering property.
class CvLat
Definition	df-covers 38626*	Define the covers relation ("is covered by") for posets. "𝑎 is covered by 𝑏 " means that 𝑎 is strictly less than 𝑏 and there is nothing in between. See cvrval 38629 for the relation form. (Contributed by NM, 18-Sep-2011.)
⊢ ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})
Definition	df-ats 38627*	Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.)
⊢ Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎})
Theorem	cvrfval 38628*	Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 < 𝑦 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑥 < 𝑧 ∧ 𝑧 < 𝑦))})
Theorem	cvrval 38629*	Binary relation expressing 𝐵 covers 𝐴, which means that 𝐵 is larger than 𝐴 and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (cvbr 32004 analog.) (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑋 < 𝑧 ∧ 𝑧 < 𝑌))))
Theorem	cvrlt 38630	The covers relation implies the less-than relation. (cvpss 32007 analog.) (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 < 𝑌)
Theorem	cvrnbtwn 38631	There is no element between the two arguments of the covers relation. (cvnbtwn 32008 analog.) (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍 ∧ 𝑍 < 𝑌))
Theorem	ncvr1 38632	No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ¬ 1 𝐶𝑋)
Theorem	cvrletrN 38633	Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	cvrval2 38634*	Binary relation expressing 𝑌 covers 𝑋. Definition of covers in [Kalmbach] p. 15. (cvbr2 32005 analog.) (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∀𝑧 ∈ 𝐵 ((𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌) → 𝑧 = 𝑌))))
Theorem	cvrnbtwn2 38635	The covers relation implies no in-betweenness. (cvnbtwn2 32009 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 = 𝑌))
Theorem	cvrnbtwn3 38636	The covers relation implies no in-betweenness. (cvnbtwn3 32010 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌) ↔ 𝑋 = 𝑍))
Theorem	cvrcon3b 38637	Contraposition law for the covers relation. (cvcon3 32006 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑌)𝐶( ⊥ ‘𝑋)))
Theorem	cvrle 38638	The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≤ 𝑌)
Theorem	cvrnbtwn4 38639	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 32011 analog.) (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ (𝑋 = 𝑍 ∨ 𝑍 = 𝑌)))
Theorem	cvrnle 38640	The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	cvrne 38641	The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≠ 𝑌)
Theorem	cvrnrefN 38642	The covers relation is not reflexive. (cvnref 32013 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋𝐶𝑋)
Theorem	cvrcmp 38643	If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌))
Theorem	cvrcmp2 38644	If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌))
Theorem	pats 38645*	The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → 𝐴 = {𝑥 ∈ 𝐵 ∣ 0 𝐶𝑥})
Theorem	isat 38646	The predicate "is an atom". (ela 32061 analog.) (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 0 𝐶𝑃)))
Theorem	isat2 38647	The predicate "is an atom". (elatcv0 32063 analog.) (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃))
Theorem	atcvr0 38648	An atom covers zero. (atcv0 32064 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃)
Theorem	atbase 38649	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32066 analog.) (Contributed by NM, 10-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
Theorem	atssbase 38650	The set of atoms is a subset of the base set. (atssch 32065 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	0ltat 38651	An atom is greater than zero. (Contributed by NM, 4-Jul-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃)
Theorem	leatb 38652	A poset element less than or equal to an atom equals either zero or the atom. (atss 32068 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 )))
Theorem	leat 38653	A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑋 ≤ 𝑃) → (𝑋 = 𝑃 ∨ 𝑋 = 0 ))
Theorem	leat2 38654	A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋 ≠ 0 ∧ 𝑋 ≤ 𝑃)) → 𝑋 = 𝑃)
Theorem	leat3 38655	A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑋 ≤ 𝑃) → (𝑋 ∈ 𝐴 ∨ 𝑋 = 0 ))
Theorem	meetat 38656	The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 𝑃 ∨ (𝑋 ∧ 𝑃) = 0 ))
Theorem	meetat2 38657	The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) ∈ 𝐴 ∨ (𝑋 ∧ 𝑃) = 0 ))
Definition	df-atl 38658*	Define the class of atomic lattices, in which every nonzero element is greater than or equal to an atom. We also ensure the existence of a lattice zero, since a lattice by itself may not have a zero. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.)
⊢ AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
Theorem	isatl 38659*	The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))
Theorem	atllat 38660	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
Theorem	atlpos 38661	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
Theorem	atl0dm 38662	Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺)
Theorem	atl0cl 38663	An atomic lattice has a zero element. We can use this in place of op0cl 38544 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 0 ∈ 𝐵)
Theorem	atl0le 38664	Orthoposet zero is less than or equal to any element. (ch0le 31163 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	atlle0 38665	An element less than or equal to zero equals zero. (chle0 31165 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	atlltn0 38666	A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	isat3 38667*	The predicate "is an atom". (elat2 32062 analog.) (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 )))))
Theorem	atn0 38668	An atom is not zero. (atne0 32067 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 )
Theorem	atnle0 38669	An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ¬ 𝑃 ≤ 0 )
Theorem	atlen0 38670	A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑃 ≤ 𝑋) → 𝑋 ≠ 0 )
Theorem	atcmp 38671	If two atoms are comparable, they are equal. (atsseq 32069 analog.) (Contributed by NM, 13-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))
Theorem	atncmp 38672	Frequently-used variation of atcmp 38671. (Contributed by NM, 29-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄))
Theorem	atnlt 38673	Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃 < 𝑄)
Theorem	atcvreq0 38674	An element covered by an atom must be zero. (atcveq0 32070 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋𝐶𝑃 ↔ 𝑋 = 0 ))
Theorem	atncvrN 38675	Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃𝐶𝑄)
Theorem	atlex 38676*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 32082 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑋)
Theorem	atnle 38677	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 32098 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 ↔ (𝑃 ∧ 𝑋) = 0 ))
Theorem	atnem0 38678	The meet of distinct atoms is zero. (atnemeq0 32099 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ (𝑃 ∧ 𝑄) = 0 ))
Theorem	atlatmstc 38679*	An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 32084 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ( 1 ‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	atlatle 38680*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32093 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
Theorem	atlrelat1 38681*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32085, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌)))
Definition	df-cvlat 38682*	Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.)
⊢ CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
Theorem	iscvlat 38683*	The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
Theorem	iscvlat2N 38684*	The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 (((𝑝 ∧ 𝑥) = 0 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
Theorem	cvlatl 38685	An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
Theorem	cvllat 38686	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
Theorem	cvlposN 38687	An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Poset)
Theorem	cvlexch1 38688	An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch2 38689	An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	cvlexchb1 38690	An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	cvlexchb2 38691	An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	cvlexch3 38692	An atomic covering lattice has the exchange property. (atexch 32103 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch4N 38693	An atomic covering lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	cvlatexchb1 38694	A version of cvlexchb1 38690 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄)))
Theorem	cvlatexchb2 38695	A version of cvlexchb2 38691 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)))
Theorem	cvlatexch1 38696	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃)))
Theorem	cvlatexch2 38697	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅)))
Theorem	cvlatexch3 38698	Atom exchange property. (Contributed by NM, 29-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 ≤ (𝑄 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
Theorem	cvlcvr1 38699	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32077 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlcvrp 38700	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32097 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))