P. 393 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39201-39300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oldmm4 39201	De Morgan's law for meet in an ortholattice. (chdmm4 31556 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌))
Theorem	oldmj1 39202	De Morgan's law for join in an ortholattice. (chdmj1 31557 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj2 39203	De Morgan's law for join in an ortholattice. (chdmj2 31558 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj3 39204	De Morgan's law for join in an ortholattice. (chdmj3 31559 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌))
Theorem	oldmj4 39205	De Morgan's law for join in an ortholattice. (chdmj4 31560 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌))
Theorem	olj01 39206	An ortholattice element joined with zero equals itself. (chj0 31525 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋)
Theorem	olj02 39207	An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋)
Theorem	olm11 39208	The meet of an ortholattice element with one equals itself. (chm1i 31484 analog.) (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋)
Theorem	olm12 39209	The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋)
Theorem	latmassOLD 39210	Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4235 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍)))
Theorem	latm12 39211	A rearrangement of lattice meet. (in12 4236 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍)))
Theorem	latm32 39212	A rearrangement of lattice meet. (in12 4236 analog.) (Contributed by NM, 13-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌))
Theorem	latmrot 39213	Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌))
Theorem	latm4 39214	Rearrangement of lattice meet of 4 classes. (in4 4241 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊)))
Theorem	latmmdiN 39215	Lattice meet distributes over itself. (inindi 4242 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍)))
Theorem	latmmdir 39216	Lattice meet distributes over itself. (inindir 4243 analog.) (Contributed by NM, 6-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍)))
Theorem	olm01 39217	Meet with lattice zero is zero. (chm0 31519 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 )
Theorem	olm02 39218	Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 )
Theorem	isoml 39219*	The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
Theorem	isomliN 39220*	Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.)
⊢ 𝐾 ∈ OL    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))    ⇒   ⊢ 𝐾 ∈ OML
Theorem	omlol 39221	An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
Theorem	omlop 39222	An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
Theorem	omllat 39223	An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
Theorem	omllaw 39224	The orthomodular law. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
Theorem	omllaw2N 39225	Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 31613 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌))
Theorem	omllaw3 39226	Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 31464 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌))
Theorem	omllaw4 39227	Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋))
Theorem	omllaw5N 39228	The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 31641 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
Theorem	cmtcomlemN 39229	Lemma for cmtcomN 39230. (cmcmlem 31619 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋))
Theorem	cmtcomN 39230	Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 31620 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋))
Theorem	cmt2N 39231	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 31621 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌)))
Theorem	cmt3N 39232	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31623 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌))
Theorem	cmt4N 39233	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31623 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌)))
Theorem	cmtbr2N 39234	Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 31624 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌)))))
Theorem	cmtbr3N 39235	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 31636 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
Theorem	cmtbr4N 39236	Alternate definition for the commutes relation. (cmbr4i 31629 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌))
Theorem	lecmtN 39237	Ordered elements commute. (lecmi 31630 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌))
Theorem	cmtidN 39238	Any element commutes with itself. (cmidi 31638 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋)
Theorem	omlfh1N 39239	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 31646 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))
Theorem	omlfh3N 39240	Foulis-Holland Theorem, part 3. Dual of omlfh1N 39239. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍)))
Theorem	omlmod1i2N 39241	Analogue of modular law atmod1i2 39841 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ 𝑍))
Theorem	omlspjN 39242	Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋)
21.28.10  Atomic lattices with covering property
Syntax	ccvr 39243	Extend class notation with covers relation.
class ⋖
Syntax	catm 39244	Extend class notation with atoms.
class Atoms
Syntax	cal 39245	Extend class notation with atomic lattices.
class AtLat
Syntax	clc 39246	Extend class notation with lattices with the covering property.
class CvLat
Definition	df-covers 39247*	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 39250 for the relation form. (Contributed by NM, 18-Sep-2011.)
⊢ ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})
Definition	df-ats 39248*	Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.)
⊢ Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎})
Theorem	cvrfval 39249*	Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 < 𝑦 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑥 < 𝑧 ∧ 𝑧 < 𝑦))})
Theorem	cvrval 39250*	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 32310 analog.) (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑋 < 𝑧 ∧ 𝑧 < 𝑌))))
Theorem	cvrlt 39251	The covers relation implies the less-than relation. (cvpss 32313 analog.) (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 < 𝑌)
Theorem	cvrnbtwn 39252	There is no element between the two arguments of the covers relation. (cvnbtwn 32314 analog.) (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍 ∧ 𝑍 < 𝑌))
Theorem	ncvr1 39253	No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ¬ 1 𝐶𝑋)
Theorem	cvrletrN 39254	Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	cvrval2 39255*	Binary relation expressing 𝑌 covers 𝑋. Definition of covers in [Kalmbach] p. 15. (cvbr2 32311 analog.) (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∀𝑧 ∈ 𝐵 ((𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌) → 𝑧 = 𝑌))))
Theorem	cvrnbtwn2 39256	The covers relation implies no in-betweenness. (cvnbtwn2 32315 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 = 𝑌))
Theorem	cvrnbtwn3 39257	The covers relation implies no in-betweenness. (cvnbtwn3 32316 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌) ↔ 𝑋 = 𝑍))
Theorem	cvrcon3b 39258	Contraposition law for the covers relation. (cvcon3 32312 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑌)𝐶( ⊥ ‘𝑋)))
Theorem	cvrle 39259	The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≤ 𝑌)
Theorem	cvrnbtwn4 39260	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 32317 analog.) (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ (𝑋 = 𝑍 ∨ 𝑍 = 𝑌)))
Theorem	cvrnle 39261	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 39262	The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≠ 𝑌)
Theorem	cvrnrefN 39263	The covers relation is not reflexive. (cvnref 32319 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋𝐶𝑋)
Theorem	cvrcmp 39264	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 39265	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 39266*	The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → 𝐴 = {𝑥 ∈ 𝐵 ∣ 0 𝐶𝑥})
Theorem	isat 39267	The predicate "is an atom". (ela 32367 analog.) (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 0 𝐶𝑃)))
Theorem	isat2 39268	The predicate "is an atom". (elatcv0 32369 analog.) (Contributed by NM, 18-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃))
Theorem	atcvr0 39269	An atom covers zero. (atcv0 32370 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃)
Theorem	atbase 39270	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32372 analog.) (Contributed by NM, 10-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
Theorem	atssbase 39271	The set of atoms is a subset of the base set. (atssch 32371 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	0ltat 39272	An atom is greater than zero. (Contributed by NM, 4-Jul-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃)
Theorem	leatb 39273	A poset element less than or equal to an atom equals either zero or the atom. (atss 32374 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 )))
Theorem	leat 39274	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 39275	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 39276	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 39277	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 39278	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 39279*	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 39280*	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 39281	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
Theorem	atlpos 39282	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
Theorem	atl0dm 39283	Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺)
Theorem	atl0cl 39284	An atomic lattice has a zero element. We can use this in place of op0cl 39165 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → 0 ∈ 𝐵)
Theorem	atl0le 39285	Orthoposet zero is less than or equal to any element. (ch0le 31469 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	atlle0 39286	An element less than or equal to zero equals zero. (chle0 31471 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	atlltn0 39287	A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	isat3 39288*	The predicate "is an atom". (elat2 32368 analog.) (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 )))))
Theorem	atn0 39289	An atom is not zero. (atne0 32373 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 )
Theorem	atnle0 39290	An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ¬ 𝑃 ≤ 0 )
Theorem	atlen0 39291	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 39292	If two atoms are comparable, they are equal. (atsseq 32375 analog.) (Contributed by NM, 13-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))
Theorem	atncmp 39293	Frequently-used variation of atcmp 39292. (Contributed by NM, 29-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄))
Theorem	atnlt 39294	Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃 < 𝑄)
Theorem	atcvreq0 39295	An element covered by an atom must be zero. (atcveq0 32376 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋𝐶𝑃 ↔ 𝑋 = 0 ))
Theorem	atncvrN 39296	Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃𝐶𝑄)
Theorem	atlex 39297*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 32388 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑋)
Theorem	atnle 39298	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 32404 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 ↔ (𝑃 ∧ 𝑋) = 0 ))
Theorem	atnem0 39299	The meet of distinct atoms is zero. (atnemeq0 32405 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ (𝑃 ∧ 𝑄) = 0 ))
Theorem	atlatmstc 39300*	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 32390 analog.) (Contributed by NM, 5-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ( 1 ‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋)