Home | Metamath
Proof Explorer Theorem List (p. 376 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lduallmod 37501 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
β’ π· = (LDualβπ) & β’ (π β π β LMod) β β’ (π β π· β LMod) | ||
Theorem | lduallvec 37502 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 19972; 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 37503 | 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 37504 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) β β’ (π β (πΊ β π») β πΉ) | ||
Theorem | ldualvsubval 37505 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 37503? (Requires π· to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) & β’ (π β π β π) β β’ (π β ((πΊ β π»)βπ) = ((πΊβπ)π(π»βπ))) | ||
Theorem | ldualssvscl 37506 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ π = (LSubSpβπ·) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (π Β· π) β π) | ||
Theorem | ldualssvsubcl 37507 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ π = (LSubSpβπ·) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π) β π) | ||
Theorem | ldual0vs 37508 | 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 37509 | 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 37510 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
β’ π» = (LSHypβπ) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) & β’ π· = (LDualβπ) & β’ 0 = (0gβπ·) & β’ (π β π β LVec) & β’ (π β πΊ β πΉ) β β’ (π β ((πΎβπΊ) β π» β πΊ β 0 )) | ||
Theorem | lkrpssN 37511 | 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 37512 | 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 37513* | 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 37514* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSpanβπ·) & β’ (π β π β LVec) & β’ (π β πΊ β πΉ) β β’ (π β (πβ{πΊ}) = {π β πΉ β£ (πΏβπΊ) β (πΏβπ)}) | ||
Theorem | ldualkrsc 37515 | 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 37516 | 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 37517* | 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 37518 | 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 37519 | 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 37520 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 37521 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 37522 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 37523 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 37524* | 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 37525* | 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 37526 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
β’ OL = (Lat β© OP) | ||
Definition | df-oml 37527* | 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 37528* | 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 37529 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
β’ (πΎ β OP β πΎ β Poset) | ||
Theorem | oposlem 37530 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯ βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 )) | ||
Theorem | op01dm 37531 | Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β OP β (π΅ β dom π β§ π΅ β dom πΊ)) | ||
Theorem | op0cl 37532 | An orthoposet has a zero element. (h0elch 29983 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β OP β 0 β π΅) | ||
Theorem | op1cl 37533 | An orthoposet has a unity element. (helch 29971 analog.) (Contributed by NM, 22-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β OP β 1 β π΅) | ||
Theorem | op0le 37534 | Orthoposet zero is less than or equal to any element. (ch0le 30169 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β 0 β€ π) | ||
Theorem | ople0 37535 | An element less than or equal to zero equals zero. (chle0 30171 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β€ 0 β π = 0 )) | ||
Theorem | opnlen0 37536 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2956 and op0le 37534 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ (((πΎ β OP β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β π β 0 ) | ||
Theorem | lub0N 37537 | 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 37538 | 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 37539 | Any element is less than the orthoposet unity. (chss 29957 analog.) (Contributed by NM, 23-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β π β€ 1 ) | ||
Theorem | op1le 37540 | If the orthoposet unity is less than or equal to an element, the element equals the unit. (chle0 30171 analog.) (Contributed by NM, 5-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( 1 β€ π β π = 1 )) | ||
Theorem | glb0N 37541 | 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 37542 | Closure of orthocomplement operation. (choccl 30034 analog.) (Contributed by NM, 20-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) | ||
Theorem | opococ 37543 | Double negative law for orthoposets. (ococ 30134 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | opcon3b 37544 | Contraposition law for orthoposets. (chcon3i 30194 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π = π β ( β₯ βπ) = ( β₯ βπ))) | ||
Theorem | opcon2b 37545 | Orthocomplement contraposition law. (negcon2 11388 analog.) (Contributed by NM, 16-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π = ( β₯ βπ) β π = ( β₯ βπ))) | ||
Theorem | opcon1b 37546 | Orthocomplement contraposition law. (negcon1 11387 analog.) (Contributed by NM, 24-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) = π β ( β₯ βπ) = π)) | ||
Theorem | oplecon3 37547 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) | ||
Theorem | oplecon3b 37548 | Contraposition law for orthoposets. (chsscon3 30228 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) | ||
Theorem | oplecon1b 37549 | Contraposition law for strict ordering in orthoposets. (chsscon1 30229 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β€ π β ( β₯ βπ) β€ π)) | ||
Theorem | opoc1 37550 | Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.) |
β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OP β ( β₯ β 1 ) = 0 ) | ||
Theorem | opoc0 37551 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OP β ( β₯ β 0 ) = 1 ) | ||
Theorem | opltcon3b 37552 | Contraposition law for strict ordering in orthoposets. (chpsscon3 30231 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π < π β ( β₯ βπ) < ( β₯ βπ))) | ||
Theorem | opltcon1b 37553 | Contraposition law for strict ordering in orthoposets. (chpsscon1 30232 analog.) (Contributed by NM, 5-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) < π β ( β₯ βπ) < π)) | ||
Theorem | opltcon2b 37554 | Contraposition law for strict ordering in orthoposets. (chsscon2 30230 analog.) (Contributed by NM, 5-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π < ( β₯ βπ) β π < ( β₯ βπ))) | ||
Theorem | opexmid 37555 | Law of excluded middle for orthoposets. (chjo 30243 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β¨ ( β₯ βπ)) = 1 ) | ||
Theorem | opnoncon 37556 | Law of contradiction for orthoposets. (chocin 30223 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β§ ( β₯ βπ)) = 0 ) | ||
Theorem | riotaocN 37557* | The orthocomplement of the unique poset element such that π. (riotaneg 12068 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ (π₯ = ( β₯ βπ¦) β (π β π)) β β’ ((πΎ β OP β§ β!π₯ β π΅ π) β (β©π₯ β π΅ π) = ( β₯ β(β©π¦ β π΅ π))) | ||
Theorem | cmtfvalN 37558* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ (πΎ β π΄ β πΆ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) | ||
Theorem | cmtvalN 37559 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 30312 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β§ π) β¨ (π β§ ( β₯ βπ))))) | ||
Theorem | isolat 37560 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β (πΎ β Lat β§ πΎ β OP)) | ||
Theorem | ollat 37561 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β πΎ β Lat) | ||
Theorem | olop 37562 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β πΎ β OP) | ||
Theorem | olposN 37563 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
β’ (πΎ β OL β πΎ β Poset) | ||
Theorem | isolatiN 37564 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
β’ πΎ β Lat & β’ πΎ β OP β β’ πΎ β OL | ||
Theorem | oldmm1 37565 | De Morgan's law for meet in an ortholattice. (chdmm1 30253 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ π)) = (( β₯ βπ) β¨ ( β₯ βπ))) | ||
Theorem | oldmm2 37566 | De Morgan's law for meet in an ortholattice. (chdmm2 30254 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β§ π)) = (π β¨ ( β₯ βπ))) | ||
Theorem | oldmm3N 37567 | De Morgan's law for meet in an ortholattice. (chdmm3 30255 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ ( β₯ βπ))) = (( β₯ βπ) β¨ π)) | ||
Theorem | oldmm4 37568 | De Morgan's law for meet in an ortholattice. (chdmm4 30256 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β§ ( β₯ βπ))) = (π β¨ π)) | ||
Theorem | oldmj1 37569 | De Morgan's law for join in an ortholattice. (chdmj1 30257 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β¨ π)) = (( β₯ βπ) β§ ( β₯ βπ))) | ||
Theorem | oldmj2 37570 | De Morgan's law for join in an ortholattice. (chdmj2 30258 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β¨ π)) = (π β§ ( β₯ βπ))) | ||
Theorem | oldmj3 37571 | De Morgan's law for join in an ortholattice. (chdmj3 30259 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β¨ ( β₯ βπ))) = (( β₯ βπ) β§ π)) | ||
Theorem | oldmj4 37572 | De Morgan's law for join in an ortholattice. (chdmj4 30260 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β¨ ( β₯ βπ))) = (π β§ π)) | ||
Theorem | olj01 37573 | An ortholattice element joined with zero equals itself. (chj0 30225 analog.) (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β¨ 0 ) = π) | ||
Theorem | olj02 37574 | An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 0 β¨ π) = π) | ||
Theorem | olm11 37575 | The meet of an ortholattice element with one equals itself. (chm1i 30184 analog.) (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β§ 1 ) = π) | ||
Theorem | olm12 37576 | The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 1 β§ π) = π) | ||
Theorem | latmassOLD 37577 | Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4178 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = (π β§ (π β§ π))) | ||
Theorem | latm12 37578 | A rearrangement of lattice meet. (in12 4179 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β§ π)) = (π β§ (π β§ π))) | ||
Theorem | latm32 37579 | A rearrangement of lattice meet. (in12 4179 analog.) (Contributed by NM, 13-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ π)) | ||
Theorem | latmrot 37580 | Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ π)) | ||
Theorem | latm4 37581 | Rearrangement of lattice meet of 4 classes. (in4 4184 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β§ π) β§ (π β§ π)) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | latmmdiN 37582 | Lattice meet distributes over itself. (inindi 4185 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β§ π)) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | latmmdir 37583 | Lattice meet distributes over itself. (inindir 4186 analog.) (Contributed by NM, 6-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | olm01 37584 | Meet with lattice zero is zero. (chm0 30219 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β§ 0 ) = 0 ) | ||
Theorem | olm02 37585 | Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 0 β§ π) = 0 ) | ||
Theorem | isoml 37586* | The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OML β (πΎ β OL β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) | ||
Theorem | isomliN 37587* | 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 37588 | An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OML β πΎ β OL) | ||
Theorem | omlop 37589 | An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.) |
β’ (πΎ β OML β πΎ β OP) | ||
Theorem | omllat 37590 | An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.) |
β’ (πΎ β OML β πΎ β Lat) | ||
Theorem | omllaw 37591 | The orthomodular law. (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β π = (π β¨ (π β§ ( β₯ βπ))))) | ||
Theorem | omllaw2N 37592 | Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 30313 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β (π β¨ (( β₯ βπ) β§ π)) = π)) | ||
Theorem | omllaw3 37593 | Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 30164 analog.) (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β€ π β§ (π β§ ( β₯ βπ)) = 0 ) β π = π)) | ||
Theorem | omllaw4 37594 | Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β (( β₯ β(( β₯ βπ) β§ π)) β§ π) = π)) | ||
Theorem | omllaw5N 37595 | The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 30341 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ (( β₯ βπ) β§ (π β¨ π))) = (π β¨ π)) | ||
Theorem | cmtcomlemN 37596 | Lemma for cmtcomN 37597. (cmcmlem 30319 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) | ||
Theorem | cmtcomN 37597 | Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 30320 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) | ||
Theorem | cmt2N 37598 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 30321 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆ( β₯ βπ))) | ||
Theorem | cmt3N 37599 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 30323 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆπ)) | ||
Theorem | cmt4N 37600 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 30323 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆ( β₯ βπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |