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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ldualvsdi2 37501 | Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.) |
β’ πΉ = (LFnlβπ) & β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ πΎ = (Baseβπ ) & β’ π· = (LDualβπ) & β’ β = (+gβπ·) & β’ Β· = ( Β·π βπ·) & β’ (π β π β LMod) & β’ (π β π β πΎ) & β’ (π β π β πΎ) & β’ (π β πΊ β πΉ) β β’ (π β ((π + π) Β· πΊ) = ((π Β· πΊ) β (π Β· πΊ))) | ||
Theorem | ldualgrplem 37502 | Lemma for ldualgrp 37503. (Contributed by NM, 22-Oct-2014.) |
β’ π· = (LDualβπ) & β’ (π β π β LMod) & β’ π = (Baseβπ) & β’ + = βf (+gβπ) & β’ πΉ = (LFnlβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = (opprβπ ) & β’ Β· = ( Β·π βπ·) β β’ (π β π· β Grp) | ||
Theorem | ldualgrp 37503 | The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.) |
β’ π· = (LDualβπ) & β’ (π β π β LMod) β β’ (π β π· β Grp) | ||
Theorem | ldual0 37504 | 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 37505 | 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 37506 | 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 37507 | 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 37508 | The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.) |
β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ 0 = (0gβπ·) & β’ (π β π β LMod) β β’ (π β 0 β πΉ) | ||
Theorem | lduallmodlem 37509 | Lemma for lduallmod 37510. (Contributed by NM, 22-Oct-2014.) |
β’ π· = (LDualβπ) & β’ (π β π β LMod) & β’ π = (Baseβπ) & β’ + = βf (+gβπ) & β’ πΉ = (LFnlβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = (opprβπ ) & β’ Β· = ( Β·π βπ·) β β’ (π β π· β LMod) | ||
Theorem | lduallmod 37510 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
β’ π· = (LDualβπ) & β’ (π β π β LMod) β β’ (π β π· β LMod) | ||
Theorem | lduallvec 37511 | 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 37512 | 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 37513 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) β β’ (π β (πΊ β π») β πΉ) | ||
Theorem | ldualvsubval 37514 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 37512? (Requires π· to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) & β’ (π β π β π) β β’ (π β ((πΊ β π»)βπ) = ((πΊβπ)π(π»βπ))) | ||
Theorem | ldualssvscl 37515 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ π = (LSubSpβπ·) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (π Β· π) β π) | ||
Theorem | ldualssvsubcl 37516 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
β’ π· = (LDualβπ) & β’ β = (-gβπ·) & β’ π = (LSubSpβπ·) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π) β π) | ||
Theorem | ldual0vs 37517 | 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 37518 | 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 37519 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
β’ π» = (LSHypβπ) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) & β’ π· = (LDualβπ) & β’ 0 = (0gβπ·) & β’ (π β π β LVec) & β’ (π β πΊ β πΉ) β β’ (π β ((πΎβπΊ) β π» β πΊ β 0 )) | ||
Theorem | lkrpssN 37520 | 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 37521 | 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 37522* | 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 37523* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSpanβπ·) & β’ (π β π β LVec) & β’ (π β πΊ β πΉ) β β’ (π β (πβ{πΊ}) = {π β πΉ β£ (πΏβπΊ) β (πΏβπ)}) | ||
Theorem | ldualkrsc 37524 | 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 37525 | 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 37526* | 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 37527 | 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 37528 | 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 37529 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 37530 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 37531 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 37532 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 37533* | 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 37534* | 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 37535 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
β’ OL = (Lat β© OP) | ||
Definition | df-oml 37536* | 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 37537* | 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 37538 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
β’ (πΎ β OP β πΎ β Poset) | ||
Theorem | oposlem 37539 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯ βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 )) | ||
Theorem | op01dm 37540 | Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β OP β (π΅ β dom π β§ π΅ β dom πΊ)) | ||
Theorem | op0cl 37541 | An orthoposet has a zero element. (h0elch 29995 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β OP β 0 β π΅) | ||
Theorem | op1cl 37542 | An orthoposet has a unity element. (helch 29983 analog.) (Contributed by NM, 22-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β OP β 1 β π΅) | ||
Theorem | op0le 37543 | Orthoposet zero is less than or equal to any element. (ch0le 30181 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β 0 β€ π) | ||
Theorem | ople0 37544 | An element less than or equal to zero equals zero. (chle0 30183 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β€ 0 β π = 0 )) | ||
Theorem | opnlen0 37545 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2955 and op0le 37543 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ (((πΎ β OP β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β π β 0 ) | ||
Theorem | lub0N 37546 | 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 37547 | 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 37548 | Any element is less than the orthoposet unity. (chss 29969 analog.) (Contributed by NM, 23-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β π β€ 1 ) | ||
Theorem | op1le 37549 | If the orthoposet unity is less than or equal to an element, the element equals the unit. (chle0 30183 analog.) (Contributed by NM, 5-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( 1 β€ π β π = 1 )) | ||
Theorem | glb0N 37550 | 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 37551 | Closure of orthocomplement operation. (choccl 30046 analog.) (Contributed by NM, 20-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) | ||
Theorem | opococ 37552 | Double negative law for orthoposets. (ococ 30146 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | opcon3b 37553 | Contraposition law for orthoposets. (chcon3i 30206 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π = π β ( β₯ βπ) = ( β₯ βπ))) | ||
Theorem | opcon2b 37554 | Orthocomplement contraposition law. (negcon2 11387 analog.) (Contributed by NM, 16-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π = ( β₯ βπ) β π = ( β₯ βπ))) | ||
Theorem | opcon1b 37555 | Orthocomplement contraposition law. (negcon1 11386 analog.) (Contributed by NM, 24-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) = π β ( β₯ βπ) = π)) | ||
Theorem | oplecon3 37556 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) | ||
Theorem | oplecon3b 37557 | Contraposition law for orthoposets. (chsscon3 30240 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) | ||
Theorem | oplecon1b 37558 | Contraposition law for strict ordering in orthoposets. (chsscon1 30241 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β€ π β ( β₯ βπ) β€ π)) | ||
Theorem | opoc1 37559 | Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.) |
β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OP β ( β₯ β 1 ) = 0 ) | ||
Theorem | opoc0 37560 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OP β ( β₯ β 0 ) = 1 ) | ||
Theorem | opltcon3b 37561 | Contraposition law for strict ordering in orthoposets. (chpsscon3 30243 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π < π β ( β₯ βπ) < ( β₯ βπ))) | ||
Theorem | opltcon1b 37562 | Contraposition law for strict ordering in orthoposets. (chpsscon1 30244 analog.) (Contributed by NM, 5-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) < π β ( β₯ βπ) < π)) | ||
Theorem | opltcon2b 37563 | Contraposition law for strict ordering in orthoposets. (chsscon2 30242 analog.) (Contributed by NM, 5-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π < ( β₯ βπ) β π < ( β₯ βπ))) | ||
Theorem | opexmid 37564 | Law of excluded middle for orthoposets. (chjo 30255 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β¨ ( β₯ βπ)) = 1 ) | ||
Theorem | opnoncon 37565 | Law of contradiction for orthoposets. (chocin 30235 analog.) (Contributed by NM, 13-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OP β§ π β π΅) β (π β§ ( β₯ βπ)) = 0 ) | ||
Theorem | riotaocN 37566* | The orthocomplement of the unique poset element such that π. (riotaneg 12067 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ (π₯ = ( β₯ βπ¦) β (π β π)) β β’ ((πΎ β OP β§ β!π₯ β π΅ π) β (β©π₯ β π΅ π) = ( β₯ β(β©π¦ β π΅ π))) | ||
Theorem | cmtfvalN 37567* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ (πΎ β π΄ β πΆ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) | ||
Theorem | cmtvalN 37568 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 30324 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β§ π) β¨ (π β§ ( β₯ βπ))))) | ||
Theorem | isolat 37569 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β (πΎ β Lat β§ πΎ β OP)) | ||
Theorem | ollat 37570 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β πΎ β Lat) | ||
Theorem | olop 37571 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OL β πΎ β OP) | ||
Theorem | olposN 37572 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
β’ (πΎ β OL β πΎ β Poset) | ||
Theorem | isolatiN 37573 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
β’ πΎ β Lat & β’ πΎ β OP β β’ πΎ β OL | ||
Theorem | oldmm1 37574 | De Morgan's law for meet in an ortholattice. (chdmm1 30265 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ π)) = (( β₯ βπ) β¨ ( β₯ βπ))) | ||
Theorem | oldmm2 37575 | De Morgan's law for meet in an ortholattice. (chdmm2 30266 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β§ π)) = (π β¨ ( β₯ βπ))) | ||
Theorem | oldmm3N 37576 | De Morgan's law for meet in an ortholattice. (chdmm3 30267 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ ( β₯ βπ))) = (( β₯ βπ) β¨ π)) | ||
Theorem | oldmm4 37577 | De Morgan's law for meet in an ortholattice. (chdmm4 30268 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β§ ( β₯ βπ))) = (π β¨ π)) | ||
Theorem | oldmj1 37578 | De Morgan's law for join in an ortholattice. (chdmj1 30269 analog.) (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β¨ π)) = (( β₯ βπ) β§ ( β₯ βπ))) | ||
Theorem | oldmj2 37579 | De Morgan's law for join in an ortholattice. (chdmj2 30270 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β¨ π)) = (π β§ ( β₯ βπ))) | ||
Theorem | oldmj3 37580 | De Morgan's law for join in an ortholattice. (chdmj3 30271 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β¨ ( β₯ βπ))) = (( β₯ βπ) β§ π)) | ||
Theorem | oldmj4 37581 | De Morgan's law for join in an ortholattice. (chdmj4 30272 analog.) (Contributed by NM, 7-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯ βπ) β¨ ( β₯ βπ))) = (π β§ π)) | ||
Theorem | olj01 37582 | An ortholattice element joined with zero equals itself. (chj0 30237 analog.) (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β¨ 0 ) = π) | ||
Theorem | olj02 37583 | An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 0 β¨ π) = π) | ||
Theorem | olm11 37584 | The meet of an ortholattice element with one equals itself. (chm1i 30196 analog.) (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β§ 1 ) = π) | ||
Theorem | olm12 37585 | The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 1 = (1.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 1 β§ π) = π) | ||
Theorem | latmassOLD 37586 | Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4177 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = (π β§ (π β§ π))) | ||
Theorem | latm12 37587 | A rearrangement of lattice meet. (in12 4178 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β§ π)) = (π β§ (π β§ π))) | ||
Theorem | latm32 37588 | A rearrangement of lattice meet. (in12 4178 analog.) (Contributed by NM, 13-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ π)) | ||
Theorem | latmrot 37589 | Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ π)) | ||
Theorem | latm4 37590 | Rearrangement of lattice meet of 4 classes. (in4 4183 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β§ π) β§ (π β§ π)) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | latmmdiN 37591 | Lattice meet distributes over itself. (inindi 4184 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β§ π)) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | latmmdir 37592 | Lattice meet distributes over itself. (inindir 4185 analog.) (Contributed by NM, 6-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((π β§ π) β§ (π β§ π))) | ||
Theorem | olm01 37593 | Meet with lattice zero is zero. (chm0 30231 analog.) (Contributed by NM, 8-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β (π β§ 0 ) = 0 ) | ||
Theorem | olm02 37594 | Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OL β§ π β π΅) β ( 0 β§ π) = 0 ) | ||
Theorem | isoml 37595* | The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ (πΎ β OML β (πΎ β OL β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) | ||
Theorem | isomliN 37596* | 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 37597 | An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.) |
β’ (πΎ β OML β πΎ β OL) | ||
Theorem | omlop 37598 | An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.) |
β’ (πΎ β OML β πΎ β OP) | ||
Theorem | omllat 37599 | An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.) |
β’ (πΎ β OML β πΎ β Lat) | ||
Theorem | omllaw 37600 | The orthomodular law. (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β π = (π β¨ (π β§ ( β₯ βπ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |