P. 400 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39901-40000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ncvr1 39901	No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ¬ 1 𝐶𝑋)
Theorem	cvrletrN 39902	Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	cvrval2 39903*	Binary relation expressing 𝑌 covers 𝑋. Definition of covers in [Kalmbach] p. 15. (cvbr2 32493 analog.) (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∀𝑧 ∈ 𝐵 ((𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌) → 𝑧 = 𝑌))))
Theorem	cvrnbtwn2 39904	The covers relation implies no in-betweenness. (cvnbtwn2 32497 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 = 𝑌))
Theorem	cvrnbtwn3 39905	The covers relation implies no in-betweenness. (cvnbtwn3 32498 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌) ↔ 𝑋 = 𝑍))
Theorem	cvrcon3b 39906	Contraposition law for the covers relation. (cvcon3 32494 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑌)𝐶( ⊥ ‘𝑋)))
Theorem	cvrle 39907	The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≤ 𝑌)
Theorem	cvrnbtwn4 39908	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 32499 analog.) (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ (𝑋 = 𝑍 ∨ 𝑍 = 𝑌)))
Theorem	cvrnle 39909	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 39910	The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≠ 𝑌)
Theorem	cvrnrefN 39911	The covers relation is not reflexive. (cvnref 32501 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋𝐶𝑋)
Theorem	cvrcmp 39912	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 39913	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 39914*	The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → 𝐴 = {𝑥 ∈ 𝐵 ∣ 0 𝐶𝑥})
Theorem	isat 39915	The predicate "is an atom". (ela 32549 analog.) (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 0 𝐶𝑃)))
Theorem	isat2 39916	The predicate "is an atom". (elatcv0 32551 analog.) (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃))
Theorem	atcvr0 39917	An atom covers zero. (atcv0 32552 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃)
Theorem	atbase 39918	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32554 analog.) (Contributed by NM, 10-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
Theorem	atssbase 39919	The set of atoms is a subset of the base set. (atssch 32553 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	0ltat 39920	An atom is greater than zero. (Contributed by NM, 4-Jul-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃)
Theorem	leatb 39921	A poset element less than or equal to an atom equals either zero or the atom. (atss 32556 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 )))
Theorem	leat 39922	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 39923	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 39924	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 39925	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 39926	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 39927*	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 39928*	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 39929	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
Theorem	atlpos 39930	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
Theorem	atl0dm 39931	Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺)
Theorem	atl0cl 39932	An atomic lattice has a zero element. We can use this in place of op0cl 39813 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 0 ∈ 𝐵)
Theorem	atl0le 39933	Orthoposet zero is less than or equal to any element. (ch0le 31651 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	atlle0 39934	An element less than or equal to zero equals zero. (chle0 31653 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	atlltn0 39935	A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	isat3 39936*	The predicate "is an atom". (elat2 32550 analog.) (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 )))))
Theorem	atn0 39937	An atom is not zero. (atne0 32555 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 )
Theorem	atnle0 39938	An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ¬ 𝑃 ≤ 0 )
Theorem	atlen0 39939	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 39940	If two atoms are comparable, they are equal. (atsseq 32557 analog.) (Contributed by NM, 13-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))
Theorem	atncmp 39941	Frequently-used variation of atcmp 39940. (Contributed by NM, 29-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄))
Theorem	atnlt 39942	Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃 < 𝑄)
Theorem	atcvreq0 39943	An element covered by an atom must be zero. (atcveq0 32558 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋𝐶𝑃 ↔ 𝑋 = 0 ))
Theorem	atncvrN 39944	Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃𝐶𝑄)
Theorem	atlex 39945*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 32570 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑋)
Theorem	atnle 39946	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 32586 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 ↔ (𝑃 ∧ 𝑋) = 0 ))
Theorem	atnem0 39947	The meet of distinct atoms is zero. (atnemeq0 32587 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ (𝑃 ∧ 𝑄) = 0 ))
Theorem	atlatmstc 39948*	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 32572 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ( 1 ‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	atlatle 39949*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32581 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
Theorem	atlrelat1 39950*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32573, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌)))
Definition	df-cvlat 39951*	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 39952*	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 39953*	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 39954	An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
Theorem	cvllat 39955	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
Theorem	cvlposN 39956	An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Poset)
Theorem	cvlexch1 39957	An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch2 39958	An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	cvlexchb1 39959	An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	cvlexchb2 39960	An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	cvlexch3 39961	An atomic covering lattice has the exchange property. (atexch 32591 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch4N 39962	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 39963	A version of cvlexchb1 39959 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄)))
Theorem	cvlatexchb2 39964	A version of cvlexchb2 39960 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)))
Theorem	cvlatexch1 39965	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃)))
Theorem	cvlatexch2 39966	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅)))
Theorem	cvlatexch3 39967	Atom exchange property. (Contributed by NM, 29-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 ≤ (𝑄 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
Theorem	cvlcvr1 39968	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32565 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlcvrp 39969	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32585 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlatcvr1 39970	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄)))
Theorem	cvlatcvr2 39971	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃)))
Theorem	cvlsupr2 39972	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))))
Theorem	cvlsupr3 39973	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 39981, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 39983. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑃 ≠ 𝑄 → (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))))
Theorem	cvlsupr4 39974	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
Theorem	cvlsupr5 39975	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑃)
Theorem	cvlsupr6 39976	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄)
Theorem	cvlsupr7 39977	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄))
Theorem	cvlsupr8 39978	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))
21.28.11  Hilbert lattices
Syntax	chlt 39979	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 39980*	Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.)
⊢ HL = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))}
Theorem	ishlat1 39981*	The predicate "is a Hilbert lattice", which is: is orthomodular (𝐾 ∈ OML), complete (𝐾 ∈ CLat), atomic and satisfies the exchange (or covering) property (𝐾 ∈ CvLat), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
Theorem	ishlat2 39982*	The predicate "is a Hilbert lattice". Here we replace 𝐾 ∈ CvLat with the weaker 𝐾 ∈ AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
Theorem	ishlat3N 39983*	The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧). The exchange property and atomicity are provided by 𝐾 ∈ CvLat, and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
Theorem	ishlatiN 39984*	Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.)
⊢ 𝐾 ∈ OML    &   ⊢ 𝐾 ∈ CLat    &   ⊢ 𝐾 ∈ AtLat    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))    &   ⊢ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))    ⇒   ⊢ 𝐾 ∈ HL
Theorem	hlomcmcv 39985	A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
Theorem	hloml 39986	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
Theorem	hlclat 39987	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
Theorem	hlcvl 39988	A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
Theorem	hlatl 39989	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Theorem	hlol 39990	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
Theorem	hlop 39991	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
Theorem	hllat 39992	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
Theorem	hllatd 39993	Deduction form of hllat 39992. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.)
⊢ (𝜑 → 𝐾 ∈ HL)    ⇒   ⊢ (𝜑 → 𝐾 ∈ Lat)
Theorem	hlomcmat 39994	A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
Theorem	hlpos 39995	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
Theorem	hlatjcl 39996	Closure of join operation. Frequently-used special case of latjcl 18481 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	hlatjcom 39997	Commutatitivity of join operation. Frequently-used special case of latjcom 18489 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	hlatjidm 39998	Idempotence of join operation. Frequently-used special case of latjcom 18489 for atoms. (Contributed by NM, 15-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	hlatjass 39999	Lattice join is associative. Frequently-used special case of latjass 18525 for atoms. (Contributed by NM, 27-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅)))
Theorem	hlatj12 40000	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18527 for atoms. (Contributed by NM, 4-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ (𝑃 ∨ 𝑅)))