![]() |
Metamath
Proof Explorer Theorem List (p. 386 of 481) | < 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-30604) |
![]() (30605-32127) |
![]() (32128-48014) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ldualkrsc 38501 | 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 38502 | 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 38503* | 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 38504 | 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 38505 | 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 38506 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 38507 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 38508 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 38509 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 38510* | 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 38511* | 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 38512 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OL = (Lat ∩ OP) | ||
Definition | df-oml 38513* | 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 38514* | 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 38515 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) | ||
Theorem | oposlem 38516 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | ||
Theorem | op01dm 38517 | Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) | ||
Theorem | op0cl 38518 | An orthoposet has a zero element. (h0elch 30941 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵) | ||
Theorem | op1cl 38519 | An orthoposet has a unity element. (helch 30929 analog.) (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) | ||
Theorem | op0le 38520 | Orthoposet zero is less than or equal to any element. (ch0le 31127 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋) | ||
Theorem | ople0 38521 | An element less than or equal to zero equals zero. (chle0 31129 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 )) | ||
Theorem | opnlen0 38522 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2953 and op0le 38520 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 ) | ||
Theorem | lub0N 38523 | 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 38524 | 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 38525 | Any element is less than the orthoposet unity. (chss 30915 analog.) (Contributed by NM, 23-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 ) | ||
Theorem | op1le 38526 | If the orthoposet unity is less than or equal to an element, the element equals the unit. (chle0 31129 analog.) (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 )) | ||
Theorem | glb0N 38527 | 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 38528 | Closure of orthocomplement operation. (choccl 30992 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | ||
Theorem | opococ 38529 | Double negative law for orthoposets. (ococ 31092 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | opcon3b 38530 | Contraposition law for orthoposets. (chcon3i 31152 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ( ⊥ ‘𝑌) = ( ⊥ ‘𝑋))) | ||
Theorem | opcon2b 38531 | Orthocomplement contraposition law. (negcon2 11520 analog.) (Contributed by NM, 16-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ( ⊥ ‘𝑌) ↔ 𝑌 = ( ⊥ ‘𝑋))) | ||
Theorem | opcon1b 38532 | Orthocomplement contraposition law. (negcon1 11519 analog.) (Contributed by NM, 24-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) = 𝑌 ↔ ( ⊥ ‘𝑌) = 𝑋)) | ||
Theorem | oplecon3 38533 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon3b 38534 | Contraposition law for orthoposets. (chsscon3 31186 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon1b 38535 | Contraposition law for strict ordering in orthoposets. (chsscon1 31187 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋)) | ||
Theorem | opoc1 38536 | Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 ) | ||
Theorem | opoc0 38537 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 ) | ||
Theorem | opltcon3b 38538 | Contraposition law for strict ordering in orthoposets. (chpsscon3 31189 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋))) | ||
Theorem | opltcon1b 38539 | Contraposition law for strict ordering in orthoposets. (chpsscon1 31190 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋)) | ||
Theorem | opltcon2b 38540 | Contraposition law for strict ordering in orthoposets. (chsscon2 31188 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋))) | ||
Theorem | opexmid 38541 | Law of excluded middle for orthoposets. (chjo 31201 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ) | ||
Theorem | opnoncon 38542 | Law of contradiction for orthoposets. (chocin 31181 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) | ||
Theorem | riotaocN 38543* | The orthocomplement of the unique poset element such that 𝜓. (riotaneg 12200 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓))) | ||
Theorem | cmtfvalN 38544* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))}) | ||
Theorem | cmtvalN 38545 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 31270 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))) | ||
Theorem | isolat 38546 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | ||
Theorem | ollat 38547 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) | ||
Theorem | olop 38548 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | ||
Theorem | olposN 38549 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset) | ||
Theorem | isolatiN 38550 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
⊢ 𝐾 ∈ Lat & ⊢ 𝐾 ∈ OP ⇒ ⊢ 𝐾 ∈ OL | ||
Theorem | oldmm1 38551 | De Morgan's law for meet in an ortholattice. (chdmm1 31211 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm2 38552 | De Morgan's law for meet in an ortholattice. (chdmm2 31212 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm3N 38553 | De Morgan's law for meet in an ortholattice. (chdmm3 31213 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌)) | ||
Theorem | oldmm4 38554 | De Morgan's law for meet in an ortholattice. (chdmm4 31214 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌)) | ||
Theorem | oldmj1 38555 | De Morgan's law for join in an ortholattice. (chdmj1 31215 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) | ||
Theorem | oldmj2 38556 | De Morgan's law for join in an ortholattice. (chdmj2 31216 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌))) | ||
Theorem | oldmj3 38557 | De Morgan's law for join in an ortholattice. (chdmj3 31217 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌)) | ||
Theorem | oldmj4 38558 | De Morgan's law for join in an ortholattice. (chdmj4 31218 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌)) | ||
Theorem | olj01 38559 | An ortholattice element joined with zero equals itself. (chj0 31183 analog.) (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋) | ||
Theorem | olj02 38560 | An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋) | ||
Theorem | olm11 38561 | The meet of an ortholattice element with one equals itself. (chm1i 31142 analog.) (Contributed by NM, 22-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋) | ||
Theorem | olm12 38562 | The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋) | ||
Theorem | latmassOLD 38563 | Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4219 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | latm12 38564 | A rearrangement of lattice meet. (in12 4220 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍))) | ||
Theorem | latm32 38565 | A rearrangement of lattice meet. (in12 4220 analog.) (Contributed by NM, 13-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌)) | ||
Theorem | latmrot 38566 | Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌)) | ||
Theorem | latm4 38567 | Rearrangement of lattice meet of 4 classes. (in4 4225 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊))) | ||
Theorem | latmmdiN 38568 | Lattice meet distributes over itself. (inindi 4226 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍))) | ||
Theorem | latmmdir 38569 | Lattice meet distributes over itself. (inindir 4227 analog.) (Contributed by NM, 6-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | olm01 38570 | Meet with lattice zero is zero. (chm0 31177 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 ) | ||
Theorem | olm02 38571 | Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 ) | ||
Theorem | isoml 38572* | The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | ||
Theorem | isomliN 38573* | 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 38574 | An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | ||
Theorem | omlop 38575 | An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) | ||
Theorem | omllat 38576 | An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.) |
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) | ||
Theorem | omllaw 38577 | The orthomodular law. (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))) | ||
Theorem | omllaw2N 38578 | Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 31271 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌)) | ||
Theorem | omllaw3 38579 | Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 31122 analog.) (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌)) | ||
Theorem | omllaw4 38580 | Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋)) | ||
Theorem | omllaw5N 38581 | The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 31299 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌)) | ||
Theorem | cmtcomlemN 38582 | Lemma for cmtcomN 38583. (cmcmlem 31277 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋)) | ||
Theorem | cmtcomN 38583 | Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 31278 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋)) | ||
Theorem | cmt2N 38584 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 31279 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) | ||
Theorem | cmt3N 38585 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31281 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌)) | ||
Theorem | cmt4N 38586 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31281 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌))) | ||
Theorem | cmtbr2N 38587 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 31282 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌))))) | ||
Theorem | cmtbr3N 38588 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 31294 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌))) | ||
Theorem | cmtbr4N 38589 | Alternate definition for the commutes relation. (cmbr4i 31287 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌)) | ||
Theorem | lecmtN 38590 | Ordered elements commute. (lecmi 31288 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌)) | ||
Theorem | cmtidN 38591 | Any element commutes with itself. (cmidi 31296 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋) | ||
Theorem | omlfh1N 38592 | 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 31304 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
Theorem | omlfh3N 38593 | Foulis-Holland Theorem, part 3. Dual of omlfh1N 38592. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
Theorem | omlmod1i2N 38594 | Analogue of modular law atmod1i2 39194 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ 𝑍)) | ||
Theorem | omlspjN 38595 | Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋) | ||
Syntax | ccvr 38596 | Extend class notation with covers relation. |
class ⋖ | ||
Syntax | catm 38597 | Extend class notation with atoms. |
class Atoms | ||
Syntax | cal 38598 | Extend class notation with atomic lattices. |
class AtLat | ||
Syntax | clc 38599 | Extend class notation with lattices with the covering property. |
class CvLat | ||
Definition | df-covers 38600* | 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 38603 for the relation form. (Contributed by NM, 18-Sep-2011.) |
⊢ ⋖ = (𝑝 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |