P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ldual0vs 37101	Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ( 0 · 𝐺) = 𝑂)
Theorem	lkr0f2 37102	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = 0 ))
Theorem	lduallkr3 37103	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 ))
Theorem	lkrpssN 37104	Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊊ (𝐾‘𝐻) ↔ (𝐺 ≠ 0 ∧ 𝐻 = 0 )))
Theorem	lkrin 37105	Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∩ (𝐾‘𝐻)) ⊆ (𝐾‘(𝐺 + 𝐻)))
Theorem	eqlkr4 37106*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺))
Theorem	ldual1dim 37107*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)})
Theorem	ldualkrsc 37108	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺))
Theorem	lkrss 37109	The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺)))
Theorem	lkrss2N 37110*	Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊆ (𝐾‘𝐻) ↔ ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺)))
Theorem	lkreqN 37111	Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑅 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (𝐴 · 𝐻))    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))
Theorem	lkrlspeqN 37112	Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ ((𝑁‘{𝐻}) ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐻))
20.24.9  Ortholattices and orthomodular lattices
Syntax	cops 37113	Extend class notation with orthoposets.
class OP
Syntax	ccmtN 37114	Extend class notation with the commutes relation.
class cm
Syntax	col 37115	Extend class notation with orthlattices.
class OL
Syntax	coml 37116	Extend class notation with orthomodular lattices.
class OML
Definition	df-oposet 37117*	Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that (Base p ) e. dom ( lub 𝑝) means there is an upper bound 1., and similarly for the 0. element. (Contributed by NM, 20-Oct-2011.) (Revised by NM, 13-Sep-2018.)
⊢ OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))}
Definition	df-cmtN 37118*	Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.)
⊢ cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
Definition	df-ol 37119	Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
⊢ OL = (Lat ∩ OP)
Definition	df-oml 37120*	Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
⊢ OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
Theorem	isopos 37121*	The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )))
Theorem	opposet 37122	Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.)
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset)
Theorem	oposlem 37123	Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
Theorem	op01dm 37124	Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))
Theorem	op0cl 37125	An orthoposet has a zero element. (h0elch 29518 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵)
Theorem	op1cl 37126	An orthoposet has a unit element. (helch 29506 analog.) (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵)
Theorem	op0le 37127	Orthoposet zero is less than or equal to any element. (ch0le 29704 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	ople0 37128	An element less than or equal to zero equals zero. (chle0 29706 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	opnlen0 37129	An element not less than another is nonzero. TODO: Look for uses of necon3bd 2956 and op0le 37127 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 )
Theorem	lub0N 37130	The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013.) (New usage is discouraged.)
⊢ 1 = (lub‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( 1 ‘∅) = 0 )
Theorem	opltn0 37131	A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	ople1 37132	Any element is less than the orthoposet unit. (chss 29492 analog.) (Contributed by NM, 23-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 )
Theorem	op1le 37133	If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 29706 analog.) (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 ))
Theorem	glb0N 37134	The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1 )
Theorem	opoccl 37135	Closure of orthocomplement operation. (choccl 29569 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
Theorem	opococ 37136	Double negative law for orthoposets. (ococ 29669 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	opcon3b 37137	Contraposition law for orthoposets. (chcon3i 29729 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ( ⊥ ‘𝑌) = ( ⊥ ‘𝑋)))
Theorem	opcon2b 37138	Orthocomplement contraposition law. (negcon2 11204 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ( ⊥ ‘𝑌) ↔ 𝑌 = ( ⊥ ‘𝑋)))
Theorem	opcon1b 37139	Orthocomplement contraposition law. (negcon1 11203 analog.) (Contributed by NM, 24-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) = 𝑌 ↔ ( ⊥ ‘𝑌) = 𝑋))
Theorem	oplecon3 37140	Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))
Theorem	oplecon3b 37141	Contraposition law for orthoposets. (chsscon3 29763 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))
Theorem	oplecon1b 37142	Contraposition law for strict ordering in orthoposets. (chsscon1 29764 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋))
Theorem	opoc1 37143	Orthocomplement of orthoposet unit. (Contributed by NM, 24-Jan-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 )
Theorem	opoc0 37144	Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 )
Theorem	opltcon3b 37145	Contraposition law for strict ordering in orthoposets. (chpsscon3 29766 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋)))
Theorem	opltcon1b 37146	Contraposition law for strict ordering in orthoposets. (chpsscon1 29767 analog.) (Contributed by NM, 5-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋))
Theorem	opltcon2b 37147	Contraposition law for strict ordering in orthoposets. (chsscon2 29765 analog.) (Contributed by NM, 5-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋)))
Theorem	opexmid 37148	Law of excluded middle for orthoposets. (chjo 29778 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 )
Theorem	opnoncon 37149	Law of contradiction for orthoposets. (chocin 29758 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )
Theorem	riotaocN 37150*	The orthocomplement of the unique poset element such that 𝜓. (riotaneg 11884 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓)))
Theorem	cmtfvalN 37151*	Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))})
Theorem	cmtvalN 37152	Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 29847 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
Theorem	isolat 37153	The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
Theorem	ollat 37154	An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat)
Theorem	olop 37155	An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)
Theorem	olposN 37156	An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset)
Theorem	isolatiN 37157	Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.)
⊢ 𝐾 ∈ Lat    &   ⊢ 𝐾 ∈ OP    ⇒   ⊢ 𝐾 ∈ OL
Theorem	oldmm1 37158	De Morgan's law for meet in an ortholattice. (chdmm1 29788 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)))
Theorem	oldmm2 37159	De Morgan's law for meet in an ortholattice. (chdmm2 29789 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌)))
Theorem	oldmm3N 37160	De Morgan's law for meet in an ortholattice. (chdmm3 29790 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
Theorem	oldmm4 37161	De Morgan's law for meet in an ortholattice. (chdmm4 29791 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌))
Theorem	oldmj1 37162	De Morgan's law for join in an ortholattice. (chdmj1 29792 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj2 37163	De Morgan's law for join in an ortholattice. (chdmj2 29793 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj3 37164	De Morgan's law for join in an ortholattice. (chdmj3 29794 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌))
Theorem	oldmj4 37165	De Morgan's law for join in an ortholattice. (chdmj4 29795 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌))
Theorem	olj01 37166	An ortholattice element joined with zero equals itself. (chj0 29760 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋)
Theorem	olj02 37167	An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋)
Theorem	olm11 37168	The meet of an ortholattice element with one equals itself. (chm1i 29719 analog.) (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋)
Theorem	olm12 37169	The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋)
Theorem	latmassOLD 37170	Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4150 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍)))
Theorem	latm12 37171	A rearrangement of lattice meet. (in12 4151 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍)))
Theorem	latm32 37172	A rearrangement of lattice meet. (in12 4151 analog.) (Contributed by NM, 13-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌))
Theorem	latmrot 37173	Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌))
Theorem	latm4 37174	Rearrangement of lattice meet of 4 classes. (in4 4156 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊)))
Theorem	latmmdiN 37175	Lattice meet distributes over itself. (inindi 4157 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍)))
Theorem	latmmdir 37176	Lattice meet distributes over itself. (inindir 4158 analog.) (Contributed by NM, 6-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍)))
Theorem	olm01 37177	Meet with lattice zero is zero. (chm0 29754 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 )
Theorem	olm02 37178	Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 )
Theorem	isoml 37179*	The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
Theorem	isomliN 37180*	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 37181	An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
Theorem	omlop 37182	An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
Theorem	omllat 37183	An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
Theorem	omllaw 37184	The orthomodular law. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
Theorem	omllaw2N 37185	Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 29848 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌))
Theorem	omllaw3 37186	Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 29699 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌))
Theorem	omllaw4 37187	Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋))
Theorem	omllaw5N 37188	The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 29876 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
Theorem	cmtcomlemN 37189	Lemma for cmtcomN 37190. (cmcmlem 29854 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋))
Theorem	cmtcomN 37190	Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 29855 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋))
Theorem	cmt2N 37191	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 29856 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌)))
Theorem	cmt3N 37192	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 29858 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌))
Theorem	cmt4N 37193	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 29858 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌)))
Theorem	cmtbr2N 37194	Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 29859 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌)))))
Theorem	cmtbr3N 37195	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 29871 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
Theorem	cmtbr4N 37196	Alternate definition for the commutes relation. (cmbr4i 29864 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌))
Theorem	lecmtN 37197	Ordered elements commute. (lecmi 29865 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌))
Theorem	cmtidN 37198	Any element commutes with itself. (cmidi 29873 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋)
Theorem	omlfh1N 37199	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 29881 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))
Theorem	omlfh3N 37200	Foulis-Holland Theorem, part 3. Dual of omlfh1N 37199. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍)))