P. 402 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40101-40200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isat2 40101	The predicate "is an atom". (elatcv0 32730 analog.) (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃))
Theorem	atcvr0 40102	An atom covers zero. (atcv0 32731 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃)
Theorem	atbase 40103	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32733 analog.) (Contributed by NM, 10-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
Theorem	atssbase 40104	The set of atoms is a subset of the base set. (atssch 32732 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	0ltat 40105	An atom is greater than zero. (Contributed by NM, 4-Jul-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃)
Theorem	leatb 40106	A poset element less than or equal to an atom equals either zero or the atom. (atss 32735 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 )))
Theorem	leat 40107	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 40108	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 40109	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 40110	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 40111	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 40112*	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 40113*	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 40114	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
Theorem	atlpos 40115	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
Theorem	atl0dm 40116	Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺)
Theorem	atl0cl 40117	An atomic lattice has a zero element. We can use this in place of op0cl 39998 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 0 ∈ 𝐵)
Theorem	atl0le 40118	Orthoposet zero is less than or equal to any element. (ch0le 31830 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	atlle0 40119	An element less than or equal to zero equals zero. (chle0 31832 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	atlltn0 40120	A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	isat3 40121*	The predicate "is an atom". (elat2 32729 analog.) (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 )))))
Theorem	atn0 40122	An atom is not zero. (atne0 32734 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 )
Theorem	atnle0 40123	An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ¬ 𝑃 ≤ 0 )
Theorem	atlen0 40124	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 40125	If two atoms are comparable, they are equal. (atsseq 32736 analog.) (Contributed by NM, 13-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))
Theorem	atncmp 40126	Frequently-used variation of atcmp 40125. (Contributed by NM, 29-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄))
Theorem	atnlt 40127	Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃 < 𝑄)
Theorem	atcvreq0 40128	An element covered by an atom must be zero. (atcveq0 32737 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋𝐶𝑃 ↔ 𝑋 = 0 ))
Theorem	atncvrN 40129	Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃𝐶𝑄)
Theorem	atlex 40130*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 32749 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑋)
Theorem	atnle 40131	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 32765 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 ↔ (𝑃 ∧ 𝑋) = 0 ))
Theorem	atnem0 40132	The meet of distinct atoms is zero. (atnemeq0 32766 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ (𝑃 ∧ 𝑄) = 0 ))
Theorem	atlatmstc 40133*	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 32751 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ( 1 ‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	atlatle 40134*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32760 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
Theorem	atlrelat1 40135*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32752, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌)))
Definition	df-cvlat 40136*	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 40137*	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 40138*	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 40139	An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
Theorem	cvllat 40140	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
Theorem	cvlposN 40141	An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Poset)
Theorem	cvlexch1 40142	An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch2 40143	An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	cvlexchb1 40144	An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	cvlexchb2 40145	An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	cvlexch3 40146	An atomic covering lattice has the exchange property. (atexch 32770 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch4N 40147	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 40148	A version of cvlexchb1 40144 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄)))
Theorem	cvlatexchb2 40149	A version of cvlexchb2 40145 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)))
Theorem	cvlatexch1 40150	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃)))
Theorem	cvlatexch2 40151	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅)))
Theorem	cvlatexch3 40152	Atom exchange property. (Contributed by NM, 29-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 ≤ (𝑄 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
Theorem	cvlcvr1 40153	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32744 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlcvrp 40154	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32764 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlatcvr1 40155	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄)))
Theorem	cvlatcvr2 40156	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃)))
Theorem	cvlsupr2 40157	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))))
Theorem	cvlsupr3 40158	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 40166, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 40168. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑃 ≠ 𝑄 → (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))))
Theorem	cvlsupr4 40159	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
Theorem	cvlsupr5 40160	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑃)
Theorem	cvlsupr6 40161	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄)
Theorem	cvlsupr7 40162	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄))
Theorem	cvlsupr8 40163	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))
21.28.11  Hilbert lattices
Syntax	chlt 40164	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 40165*	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 40166*	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 40167*	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 40168*	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 40169*	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 40170	A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
Theorem	hloml 40171	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
Theorem	hlclat 40172	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
Theorem	hlcvl 40173	A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
Theorem	hlatl 40174	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Theorem	hlol 40175	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
Theorem	hlop 40176	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
Theorem	hllat 40177	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
Theorem	hllatd 40178	Deduction form of hllat 40177. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.)
⊢ (𝜑 → 𝐾 ∈ HL)    ⇒   ⊢ (𝜑 → 𝐾 ∈ Lat)
Theorem	hlomcmat 40179	A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
Theorem	hlpos 40180	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
Theorem	hlatjcl 40181	Closure of join operation. Frequently-used special case of latjcl 18520 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	hlatjcom 40182	Commutatitivity of join operation. Frequently-used special case of latjcom 18528 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	hlatjidm 40183	Idempotence of join operation. Frequently-used special case of latjcom 18528 for atoms. (Contributed by NM, 15-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	hlatjass 40184	Lattice join is associative. Frequently-used special case of latjass 18564 for atoms. (Contributed by NM, 27-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅)))
Theorem	hlatj12 40185	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18566 for atoms. (Contributed by NM, 4-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ (𝑃 ∨ 𝑅)))
Theorem	hlatj32 40186	Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18566 for atoms. (Contributed by NM, 21-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑃 ∨ 𝑅) ∨ 𝑄))
Theorem	hlatjrot 40187	Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18569 for atoms. (Contributed by NM, 2-Aug-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑅 ∨ 𝑃) ∨ 𝑄))
Theorem	hlatj4 40188	Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18570 for atoms. (Contributed by NM, 9-Aug-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)))
Theorem	hlatlej1 40189	A join's first argument is less than or equal to the join. Special case of latlej1 18529 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))
Theorem	hlatlej2 40190	A join's second argument is less than or equal to the join. Special case of latlej2 18530 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄))
Theorem	glbconN 40191*	De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012.) New df-riota 7380. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
Theorem	glbconxN 40192*	De Morgan's law for GLB and LUB. Index-set version of glbconN 40191, where we read 𝑆 as 𝑆(𝑖). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)})))
Theorem	atnlej1 40193	If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) → 𝑃 ≠ 𝑄)
Theorem	atnlej2 40194	If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) → 𝑃 ≠ 𝑅)
Theorem	hlsuprexch 40195*	A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))
Theorem	hlexch1 40196	A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	hlexch2 40197	A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	hlexchb1 40198	A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	hlexchb2 40199	A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	hlsupr 40200*	A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄)))