P. 395 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39401-39500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ldualgrplem 39401	Lemma for ldualgrp 39402. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldualgrp 39402	The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldual0 39403	The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑂 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = 0 )
Theorem	ldual1 39404	The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝐼 = (1r‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐼 = 1 )
Theorem	ldualneg 39405	The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑁 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑁 = 𝑀)
Theorem	ldual0v 39406	The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = (𝑉 × { 0 }))
Theorem	ldual0vcl 39407	The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐹)
Theorem	lduallmodlem 39408	Lemma for lduallmod 39409. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallmod 39409	The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallvec 39410	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 20273; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LVec)
Theorem	ldualvsub 39411	The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) = (𝐺 + ((𝑁‘ 1 ) · 𝐻)))
Theorem	ldualvsubcl 39412	Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹)
Theorem	ldualvsubval 39413	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 39411? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑆 = (-g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋)))
Theorem	ldualssvscl 39414	Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	ldualssvsubcl 39415	Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	ldual0vs 39416	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 39417	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 39418	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 ))
Theorem	lkrpssN 39419	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 39420	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 39421*	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 39422*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)})
Theorem	ldualkrsc 39423	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 39424	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 39425*	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 39426	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 39427	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 }))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐻))
21.28.9  Ortholattices and orthomodular lattices
Syntax	cops 39428	Extend class notation with orthoposets.
class OP
Syntax	ccmtN 39429	Extend class notation with the commutes relation.
class cm
Syntax	col 39430	Extend class notation with orthlattices.
class OL
Syntax	coml 39431	Extend class notation with orthomodular lattices.
class OML
Definition	df-oposet 39432*	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 39433*	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 39434	Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
⊢ OL = (Lat ∩ OP)
Definition	df-oml 39435*	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 39436*	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 39437	Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.)
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset)
Theorem	oposlem 39438	Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
Theorem	op01dm 39439	Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))
Theorem	op0cl 39440	An orthoposet has a zero element. (h0elch 31330 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵)
Theorem	op1cl 39441	An orthoposet has a unity element. (helch 31318 analog.) (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵)
Theorem	op0le 39442	Orthoposet zero is less than or equal to any element. (ch0le 31516 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	ople0 39443	An element less than or equal to zero equals zero. (chle0 31518 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	opnlen0 39444	An element not less than another is nonzero. TODO: Look for uses of necon3bd 2946 and op0le 39442 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 )
Theorem	lub0N 39445	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 39446	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 39447	Any element is less than the orthoposet unity. (chss 31304 analog.) (Contributed by NM, 23-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 )
Theorem	op1le 39448	If the orthoposet unity is less than or equal to an element, the element equals the unit. (chle0 31518 analog.) (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 ))
Theorem	glb0N 39449	The greatest lower bound of the empty set is the unity element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1 )
Theorem	opoccl 39450	Closure of orthocomplement operation. (choccl 31381 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
Theorem	opococ 39451	Double negative law for orthoposets. (ococ 31481 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	opcon3b 39452	Contraposition law for orthoposets. (chcon3i 31541 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ( ⊥ ‘𝑌) = ( ⊥ ‘𝑋)))
Theorem	opcon2b 39453	Orthocomplement contraposition law. (negcon2 11434 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ( ⊥ ‘𝑌) ↔ 𝑌 = ( ⊥ ‘𝑋)))
Theorem	opcon1b 39454	Orthocomplement contraposition law. (negcon1 11433 analog.) (Contributed by NM, 24-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) = 𝑌 ↔ ( ⊥ ‘𝑌) = 𝑋))
Theorem	oplecon3 39455	Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))
Theorem	oplecon3b 39456	Contraposition law for orthoposets. (chsscon3 31575 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))
Theorem	oplecon1b 39457	Contraposition law for strict ordering in orthoposets. (chsscon1 31576 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋))
Theorem	opoc1 39458	Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 )
Theorem	opoc0 39459	Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 )
Theorem	opltcon3b 39460	Contraposition law for strict ordering in orthoposets. (chpsscon3 31578 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋)))
Theorem	opltcon1b 39461	Contraposition law for strict ordering in orthoposets. (chpsscon1 31579 analog.) (Contributed by NM, 5-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋))
Theorem	opltcon2b 39462	Contraposition law for strict ordering in orthoposets. (chsscon2 31577 analog.) (Contributed by NM, 5-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋)))
Theorem	opexmid 39463	Law of excluded middle for orthoposets. (chjo 31590 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 )
Theorem	opnoncon 39464	Law of contradiction for orthoposets. (chocin 31570 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )
Theorem	riotaocN 39465*	The orthocomplement of the unique poset element such that 𝜓. (riotaneg 12121 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓)))
Theorem	cmtfvalN 39466*	Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))})
Theorem	cmtvalN 39467	Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 31659 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐶 = (cm‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
Theorem	isolat 39468	The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
Theorem	ollat 39469	An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat)
Theorem	olop 39470	An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)
Theorem	olposN 39471	An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.)
⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset)
Theorem	isolatiN 39472	Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.)
⊢ 𝐾 ∈ Lat    &   ⊢ 𝐾 ∈ OP    ⇒   ⊢ 𝐾 ∈ OL
Theorem	oldmm1 39473	De Morgan's law for meet in an ortholattice. (chdmm1 31600 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)))
Theorem	oldmm2 39474	De Morgan's law for meet in an ortholattice. (chdmm2 31601 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌)))
Theorem	oldmm3N 39475	De Morgan's law for meet in an ortholattice. (chdmm3 31602 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
Theorem	oldmm4 39476	De Morgan's law for meet in an ortholattice. (chdmm4 31603 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌))
Theorem	oldmj1 39477	De Morgan's law for join in an ortholattice. (chdmj1 31604 analog.) (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj2 39478	De Morgan's law for join in an ortholattice. (chdmj2 31605 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌)))
Theorem	oldmj3 39479	De Morgan's law for join in an ortholattice. (chdmj3 31606 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌))
Theorem	oldmj4 39480	De Morgan's law for join in an ortholattice. (chdmj4 31607 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌))
Theorem	olj01 39481	An ortholattice element joined with zero equals itself. (chj0 31572 analog.) (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋)
Theorem	olj02 39482	An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋)
Theorem	olm11 39483	The meet of an ortholattice element with one equals itself. (chm1i 31531 analog.) (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋)
Theorem	olm12 39484	The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋)
Theorem	latmassOLD 39485	Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4180 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍)))
Theorem	latm12 39486	A rearrangement of lattice meet. (in12 4181 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍)))
Theorem	latm32 39487	A rearrangement of lattice meet. (in12 4181 analog.) (Contributed by NM, 13-Nov-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌))
Theorem	latmrot 39488	Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌))
Theorem	latm4 39489	Rearrangement of lattice meet of 4 classes. (in4 4186 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊)))
Theorem	latmmdiN 39490	Lattice meet distributes over itself. (inindi 4187 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍)))
Theorem	latmmdir 39491	Lattice meet distributes over itself. (inindir 4188 analog.) (Contributed by NM, 6-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍)))
Theorem	olm01 39492	Meet with lattice zero is zero. (chm0 31566 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 )
Theorem	olm02 39493	Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 )
Theorem	isoml 39494*	The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
Theorem	isomliN 39495*	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 39496	An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
Theorem	omlop 39497	An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
Theorem	omllat 39498	An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.)
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
Theorem	omllaw 39499	The orthomodular law. (Contributed by NM, 18-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
Theorem	omllaw2N 39500	Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 31660 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌))