![]() |
Metamath
Proof Explorer Theorem List (p. 354 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43650) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lduallmodlem 35301 | Lemma for lduallmod 35302. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘𝑓 (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallmod 35302 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallvec 35303 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 19010; 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 35304 | 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 35305 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹) | ||
Theorem | ldualvsubval 35306 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 35304? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑆 = (-g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) | ||
Theorem | ldualssvscl 35307 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | ldualssvsubcl 35308 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈) | ||
Theorem | ldual0vs 35309 | 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 35310 | 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 35311 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 )) | ||
Theorem | lkrpssN 35312 | 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 35313 | 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 35314* | 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 35315* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)}) | ||
Theorem | ldualkrsc 35316 | 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 35317 | 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 35318* | 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 35319 | 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 35320 | 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 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐻)) | ||
Syntax | cops 35321 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 35322 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 35323 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 35324 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 35325* | 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 35326* | 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 35327 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OL = (Lat ∩ OP) | ||
Definition | df-oml 35328* | 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 35329* | 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 35330 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) | ||
Theorem | oposlem 35331 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | ||
Theorem | op01dm 35332 | Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) | ||
Theorem | op0cl 35333 | An orthoposet has a zero element. (h0elch 28684 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵) | ||
Theorem | op1cl 35334 | An orthoposet has a unit element. (helch 28672 analog.) (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) | ||
Theorem | op0le 35335 | Orthoposet zero is less than or equal to any element. (ch0le 28872 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋) | ||
Theorem | ople0 35336 | An element less than or equal to zero equals zero. (chle0 28874 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 )) | ||
Theorem | opnlen0 35337 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2982 and op0le 35335 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 ) | ||
Theorem | lub0N 35338 | 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 35339 | 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 35340 | Any element is less than the orthoposet unit. (chss 28658 analog.) (Contributed by NM, 23-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 ) | ||
Theorem | op1le 35341 | If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 28874 analog.) (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 )) | ||
Theorem | glb0N 35342 | 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 35343 | Closure of orthocomplement operation. (choccl 28737 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | ||
Theorem | opococ 35344 | Double negative law for orthoposets. (ococ 28837 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | opcon3b 35345 | Contraposition law for orthoposets. (chcon3i 28897 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ( ⊥ ‘𝑌) = ( ⊥ ‘𝑋))) | ||
Theorem | opcon2b 35346 | Orthocomplement contraposition law. (negcon2 10676 analog.) (Contributed by NM, 16-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ( ⊥ ‘𝑌) ↔ 𝑌 = ( ⊥ ‘𝑋))) | ||
Theorem | opcon1b 35347 | Orthocomplement contraposition law. (negcon1 10675 analog.) (Contributed by NM, 24-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) = 𝑌 ↔ ( ⊥ ‘𝑌) = 𝑋)) | ||
Theorem | oplecon3 35348 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon3b 35349 | Contraposition law for orthoposets. (chsscon3 28931 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon1b 35350 | Contraposition law for strict ordering in orthoposets. (chsscon1 28932 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋)) | ||
Theorem | opoc1 35351 | Orthocomplement of orthoposet unit. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 ) | ||
Theorem | opoc0 35352 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 ) | ||
Theorem | opltcon3b 35353 | Contraposition law for strict ordering in orthoposets. (chpsscon3 28934 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋))) | ||
Theorem | opltcon1b 35354 | Contraposition law for strict ordering in orthoposets. (chpsscon1 28935 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋)) | ||
Theorem | opltcon2b 35355 | Contraposition law for strict ordering in orthoposets. (chsscon2 28933 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋))) | ||
Theorem | opexmid 35356 | Law of excluded middle for orthoposets. (chjo 28946 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ) | ||
Theorem | opnoncon 35357 | Law of contradiction for orthoposets. (chocin 28926 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) | ||
Theorem | riotaocN 35358* | The orthocomplement of the unique poset element such that 𝜓. (riotaneg 11356 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓))) | ||
Theorem | cmtfvalN 35359* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))}) | ||
Theorem | cmtvalN 35360 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 29015 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))) | ||
Theorem | isolat 35361 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | ||
Theorem | ollat 35362 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) | ||
Theorem | olop 35363 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | ||
Theorem | olposN 35364 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset) | ||
Theorem | isolatiN 35365 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
⊢ 𝐾 ∈ Lat & ⊢ 𝐾 ∈ OP ⇒ ⊢ 𝐾 ∈ OL | ||
Theorem | oldmm1 35366 | De Morgan's law for meet in an ortholattice. (chdmm1 28956 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm2 35367 | De Morgan's law for meet in an ortholattice. (chdmm2 28957 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm3N 35368 | De Morgan's law for meet in an ortholattice. (chdmm3 28958 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌)) | ||
Theorem | oldmm4 35369 | De Morgan's law for meet in an ortholattice. (chdmm4 28959 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌)) | ||
Theorem | oldmj1 35370 | De Morgan's law for join in an ortholattice. (chdmj1 28960 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) | ||
Theorem | oldmj2 35371 | De Morgan's law for join in an ortholattice. (chdmj2 28961 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌))) | ||
Theorem | oldmj3 35372 | De Morgan's law for join in an ortholattice. (chdmj3 28962 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌)) | ||
Theorem | oldmj4 35373 | De Morgan's law for join in an ortholattice. (chdmj4 28963 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌)) | ||
Theorem | olj01 35374 | An ortholattice element joined with zero equals itself. (chj0 28928 analog.) (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋) | ||
Theorem | olj02 35375 | An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋) | ||
Theorem | olm11 35376 | The meet of an ortholattice element with one equals itself. (chm1i 28887 analog.) (Contributed by NM, 22-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋) | ||
Theorem | olm12 35377 | The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋) | ||
Theorem | latmassOLD 35378 | Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4043 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | latm12 35379 | A rearrangement of lattice meet. (in12 4044 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍))) | ||
Theorem | latm32 35380 | A rearrangement of lattice meet. (in12 4044 analog.) (Contributed by NM, 13-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌)) | ||
Theorem | latmrot 35381 | Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌)) | ||
Theorem | latm4 35382 | Rearrangement of lattice meet of 4 classes. (in4 4049 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊))) | ||
Theorem | latmmdiN 35383 | Lattice meet distributes over itself. (inindi 4050 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍))) | ||
Theorem | latmmdir 35384 | Lattice meet distributes over itself. (inindir 4051 analog.) (Contributed by NM, 6-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | olm01 35385 | Meet with lattice zero is zero. (chm0 28922 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 ) | ||
Theorem | olm02 35386 | Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 ) | ||
Theorem | isoml 35387* | The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | ||
Theorem | isomliN 35388* | 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 35389 | An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | ||
Theorem | omlop 35390 | An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) | ||
Theorem | omllat 35391 | An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) | ||
Theorem | omllaw 35392 | The orthomodular law. (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))) | ||
Theorem | omllaw2N 35393 | Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 29016 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌)) | ||
Theorem | omllaw3 35394 | Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 28867 analog.) (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌)) | ||
Theorem | omllaw4 35395 | Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋)) | ||
Theorem | omllaw5N 35396 | The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 29044 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌)) | ||
Theorem | cmtcomlemN 35397 | Lemma for cmtcomN 35398. (cmcmlem 29022 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋)) | ||
Theorem | cmtcomN 35398 | Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 29023 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋)) | ||
Theorem | cmt2N 35399 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 29024 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) | ||
Theorem | cmt3N 35400 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 29026 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |