P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cvllat 40201	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
Theorem	cvlposN 40202	An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Poset)
Theorem	cvlexch1 40203	An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch2 40204	An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	cvlexchb1 40205	An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	cvlexchb2 40206	An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	cvlexch3 40207	An atomic covering lattice has the exchange property. (atexch 32863 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	cvlexch4N 40208	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 40209	A version of cvlexchb1 40205 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄)))
Theorem	cvlatexchb2 40210	A version of cvlexchb2 40206 for atoms. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)))
Theorem	cvlatexch1 40211	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃)))
Theorem	cvlatexch2 40212	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅)))
Theorem	cvlatexch3 40213	Atom exchange property. (Contributed by NM, 29-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 ≤ (𝑄 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
Theorem	cvlcvr1 40214	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32837 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlcvrp 40215	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32857 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvlatcvr1 40216	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄)))
Theorem	cvlatcvr2 40217	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃)))
Theorem	cvlsupr2 40218	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))))
Theorem	cvlsupr3 40219	Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 40227, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 40229. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑃 ≠ 𝑄 → (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))))
Theorem	cvlsupr4 40220	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
Theorem	cvlsupr5 40221	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑃)
Theorem	cvlsupr6 40222	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄)
Theorem	cvlsupr7 40223	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄))
Theorem	cvlsupr8 40224	Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))
21.29.11  Hilbert lattices
Syntax	chlt 40225	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 40226*	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 40227*	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 40228*	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 40229*	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 40230*	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 40231	A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
Theorem	hloml 40232	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
Theorem	hlclat 40233	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
Theorem	hlcvl 40234	A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
Theorem	hlatl 40235	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Theorem	hlol 40236	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
Theorem	hlop 40237	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
Theorem	hllat 40238	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
Theorem	hllatd 40239	Deduction form of hllat 40238. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.)
⊢ (𝜑 → 𝐾 ∈ HL)    ⇒   ⊢ (𝜑 → 𝐾 ∈ Lat)
Theorem	hlomcmat 40240	A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
Theorem	hlpos 40241	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
Theorem	hlatjcl 40242	Closure of join operation. Frequently-used special case of latjcl 18531 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	hlatjcom 40243	Commutatitivity of join operation. Frequently-used special case of latjcom 18539 for atoms. (Contributed by NM, 15-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	hlatjidm 40244	Idempotence of join operation. Frequently-used special case of latjcom 18539 for atoms. (Contributed by NM, 15-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	hlatjass 40245	Lattice join is associative. Frequently-used special case of latjass 18575 for atoms. (Contributed by NM, 27-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅)))
Theorem	hlatj12 40246	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18577 for atoms. (Contributed by NM, 4-Jun-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ (𝑃 ∨ 𝑅)))
Theorem	hlatj32 40247	Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18577 for atoms. (Contributed by NM, 21-Jul-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑃 ∨ 𝑅) ∨ 𝑄))
Theorem	hlatjrot 40248	Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18580 for atoms. (Contributed by NM, 2-Aug-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑅 ∨ 𝑃) ∨ 𝑄))
Theorem	hlatj4 40249	Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18581 for atoms. (Contributed by NM, 9-Aug-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)))
Theorem	hlatlej1 40250	A join's first argument is less than or equal to the join. Special case of latlej1 18540 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))
Theorem	hlatlej2 40251	A join's second argument is less than or equal to the join. Special case of latlej2 18541 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄))
Theorem	glbconN 40252*	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 7373. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
Theorem	glbconxN 40253*	De Morgan's law for GLB and LUB. Index-set version of glbconN 40252, where we read 𝑆 as 𝑆(𝑖). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)})))
Theorem	atnlej1 40254	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 40255	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 40256*	A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))
Theorem	hlexch1 40257	A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	hlexch2 40258	A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋)))
Theorem	hlexchb1 40259	A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	hlexchb2 40260	A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋)))
Theorem	hlsupr 40261*	A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Theorem	hlsupr2 40262*	A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ∃𝑟 ∈ 𝐴 (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟))
Theorem	hlhgt4 40263*	A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))
Theorem	hlhgt2 40264*	A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ 𝐵 ( 0 < 𝑥 ∧ 𝑥 < 1 ))
Theorem	hl0lt1N 40265	Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.)
⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → 0 < 1 )
Theorem	hlexch3 40266	A Hilbert lattice has the exchange property. (atexch 32863 analog.) (Contributed by NM, 15-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
Theorem	hlexch4N 40267	A Hilbert lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 15-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄)))
Theorem	hlatexchb1 40268	A version of hlexchb1 40259 for atoms. (Contributed by NM, 15-Nov-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄)))
Theorem	hlatexchb2 40269	A version of hlexchb2 40260 for atoms. (Contributed by NM, 7-Feb-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)))
Theorem	hlatexch1 40270	Atom exchange property. (Contributed by NM, 7-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃)))
Theorem	hlatexch2 40271	Atom exchange property. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅)))
Theorem	hlatmstcOLDN 40272*	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 32844 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	hlatle 40273*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32853 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
Theorem	hlateq 40274*	The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 32855 analog.) (Contributed by NM, 24-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌) ↔ 𝑋 = 𝑌))
Theorem	hlrelat1 40275*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32845, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌)))
Theorem	hlrelat5N 40276*	An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋 < (𝑋 ∨ 𝑝) ∧ 𝑝 ≤ 𝑌))
Theorem	hlrelat 40277*	A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32846 analog.) (Contributed by NM, 4-Feb-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋 < (𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌))
Theorem	hlrelat2 40278*	A consequence of relative atomicity. (chrelat2i 32847 analog.) (Contributed by NM, 5-Feb-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌)))
Theorem	exatleN 40279	A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃))
Theorem	hl2at 40280*	A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 𝑝 ≠ 𝑞)
Theorem	atex 40281	At least one atom exists. (Contributed by NM, 15-Jul-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → 𝐴 ≠ ∅)
Theorem	intnatN 40282	If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (¬ 𝑌 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ∈ 𝐴)) → ¬ 𝑌 ∈ 𝐴)
Theorem	2llnne2N 40283	Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑄)) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄))
Theorem	2llnneN 40284	Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄))
Theorem	cvr1 40285	A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32837 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	cvr2N 40286	Less-than and covers equivalence in a Hilbert lattice. (chcv2 32838 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 < (𝑋 ∨ 𝑃) ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	hlrelat3 40287*	The Hilbert lattice is relatively atomic. Stronger version of hlrelat 40277. (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋𝐶(𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌))
Theorem	cvrval3 40288*	Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ (𝑋 ∨ 𝑝) = 𝑌)))
Theorem	cvrval4N 40289*	Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∃𝑝 ∈ 𝐴 (𝑋 ∨ 𝑝) = 𝑌)))
Theorem	cvrval5 40290*	Binary relation expressing 𝑋 covers 𝑋 ∧ 𝑌. (Contributed by NM, 7-Dec-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑋 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑌 ∧ (𝑝 ∨ (𝑋 ∧ 𝑌)) = 𝑋)))
Theorem	cvrp 40291	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32857 analog.) (Contributed by NM, 18-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃)))
Theorem	atcvr1 40292	An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄)))
Theorem	atcvr2 40293	An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃)))
Theorem	cvrexchlem 40294	Lemma for cvrexch 40295. (cvexchlem 32850 analog.) (Contributed by NM, 18-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → 𝑋𝐶(𝑋 ∨ 𝑌)))
Theorem	cvrexch 40295	A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (cvexchi 32851 analog.) (Contributed by NM, 18-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ 𝑋𝐶(𝑋 ∨ 𝑌)))
Theorem	cvratlem 40296	Lemma for cvrat 40297. (atcvatlem 32867 analog.) (Contributed by NM, 22-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))
Theorem	cvrat 40297	A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 32868 analog.) (Contributed by NM, 22-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋 ∈ 𝐴))
Theorem	ltltncvr 40298	A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → ¬ 𝑋𝐶𝑍))
Theorem	ltcvrntr 40299	Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍))
Theorem	cvrntr 40300	The covers relation is not transitive. (cvntr 32774 analog.) (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍))