Home | Metamath
Proof Explorer Theorem List (p. 377 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmtbr2N 37601 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 30324 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) | ||
Theorem | cmtbr3N 37602 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 30336 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π))) | ||
Theorem | cmtbr4N 37603 | Alternate definition for the commutes relation. (cmbr4i 30329 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) β€ π)) | ||
Theorem | lecmtN 37604 | Ordered elements commute. (lecmi 30330 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β ππΆπ)) | ||
Theorem | cmtidN 37605 | Any element commutes with itself. (cmidi 30338 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅) β ππΆπ) | ||
Theorem | omlfh1N 37606 | 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 30346 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) | ||
Theorem | omlfh3N 37607 | Foulis-Holland Theorem, part 3. Dual of omlfh1N 37606. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ (π β¨ π))) | ||
Theorem | omlmod1i2N 37608 | Analogue of modular law atmod1i2 38208 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) | ||
Theorem | omlspjN 37609 | Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β¨ ( β₯ βπ)) β§ π) = π) | ||
Syntax | ccvr 37610 | Extend class notation with covers relation. |
class β | ||
Syntax | catm 37611 | Extend class notation with atoms. |
class Atoms | ||
Syntax | cal 37612 | Extend class notation with atomic lattices. |
class AtLat | ||
Syntax | clc 37613 | Extend class notation with lattices with the covering property. |
class CvLat | ||
Definition | df-covers 37614* | 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 37617 for the relation form. (Contributed by NM, 18-Sep-2011.) |
β’ β = (π β V β¦ {β¨π, πβ© β£ ((π β (Baseβπ) β§ π β (Baseβπ)) β§ π(ltβπ)π β§ Β¬ βπ§ β (Baseβπ)(π(ltβπ)π§ β§ π§(ltβπ)π))}) | ||
Definition | df-ats 37615* | Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.) |
β’ Atoms = (π β V β¦ {π β (Baseβπ) β£ (0.βπ)( β βπ)π}) | ||
Theorem | cvrfval 37616* | Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ (πΎ β π΄ β πΆ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ < π¦ β§ Β¬ βπ§ β π΅ (π₯ < π§ β§ π§ < π¦))}) | ||
Theorem | cvrval 37617* | Binary relation expressing π΅ covers π΄, which means that π΅ is larger than π΄ and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (cvbr 31010 analog.) (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)))) | ||
Theorem | cvrlt 37618 | The covers relation implies the less-than relation. (cvpss 31013 analog.) (Contributed by NM, 8-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π < π) | ||
Theorem | cvrnbtwn 37619 | There is no element between the two arguments of the covers relation. (cvnbtwn 31014 analog.) (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β Β¬ (π < π β§ π < π)) | ||
Theorem | ncvr1 37620 | No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ π β π΅) β Β¬ 1 πΆπ) | ||
Theorem | cvrletrN 37621 | Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ π β€ π) β π < π)) | ||
Theorem | cvrval2 37622* | Binary relation expressing π covers π. Definition of covers in [Kalmbach] p. 15. (cvbr2 31011 analog.) (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π)))) | ||
Theorem | cvrnbtwn2 37623 | The covers relation implies no in-betweenness. (cvnbtwn2 31015 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π < π β§ π β€ π) β π = π)) | ||
Theorem | cvrnbtwn3 37624 | The covers relation implies no in-betweenness. (cvnbtwn3 31016 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π < π) β π = π)) | ||
Theorem | cvrcon3b 37625 | Contraposition law for the covers relation. (cvcon3 31012 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆ( β₯ βπ))) | ||
Theorem | cvrle 37626 | The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) | ||
Theorem | cvrnbtwn4 37627 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 31017 analog.) (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π))) | ||
Theorem | cvrnle 37628 | The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ ππΆπ) β Β¬ π β€ π) | ||
Theorem | cvrne 37629 | The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β π) | ||
Theorem | cvrnrefN 37630 | The covers relation is not reflexive. (cvnref 31019 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β Β¬ ππΆπ) | ||
Theorem | cvrcmp 37631 | If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β€ π β π = π)) | ||
Theorem | cvrcmp2 37632 | If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β€ π β π = π)) | ||
Theorem | pats 37633* | The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β π΄ = {π₯ β π΅ β£ 0 πΆπ₯}) | ||
Theorem | isat 37634 | The predicate "is an atom". (ela 31067 analog.) (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β (π β π΄ β (π β π΅ β§ 0 πΆπ))) | ||
Theorem | isat2 37635 | The predicate "is an atom". (elatcv0 31069 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΅) β (π β π΄ β 0 πΆπ)) | ||
Theorem | atcvr0 37636 | An atom covers zero. (atcv0 31070 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΄) β 0 πΆπ) | ||
Theorem | atbase 37637 | An atom is a member of the lattice base set (i.e. a lattice element). (atelch 31072 analog.) (Contributed by NM, 10-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β π΄ β π β π΅) | ||
Theorem | atssbase 37638 | The set of atoms is a subset of the base set. (atssch 31071 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ π΄ β π΅ | ||
Theorem | 0ltat 37639 | An atom is greater than zero. (Contributed by NM, 4-Jul-2012.) |
β’ 0 = (0.βπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΄) β 0 < π) | ||
Theorem | leatb 37640 | A poset element less than or equal to an atom equals either zero or the atom. (atss 31074 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΄) β (π β€ π β (π = π β¨ π = 0 ))) | ||
Theorem | leat 37641 | A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OP β§ π β π΅ β§ π β π΄) β§ π β€ π) β (π = π β¨ π = 0 )) | ||
Theorem | leat2 37642 | A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OP β§ π β π΅ β§ π β π΄) β§ (π β 0 β§ π β€ π)) β π = π) | ||
Theorem | leat3 37643 | A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OP β§ π β π΅ β§ π β π΄) β§ π β€ π) β (π β π΄ β¨ π = 0 )) | ||
Theorem | meetat 37644 | The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΄) β ((π β§ π) = π β¨ (π β§ π) = 0 )) | ||
Theorem | meetat2 37645 | The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OL β§ π β π΅ β§ π β π΄) β ((π β§ π) β π΄ β¨ (π β§ π) = 0 )) | ||
Definition | df-atl 37646* | Define the class of atomic lattices, in which every nonzero element is greater than or equal to an atom. We also ensure the existence of a lattice zero, since a lattice by itself may not have a zero. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.) |
β’ AtLat = {π β Lat β£ ((Baseβπ) β dom (glbβπ) β§ βπ₯ β (Baseβπ)(π₯ β (0.βπ) β βπ β (Atomsβπ)π(leβπ)π₯))} | ||
Theorem | isatl 37647* | The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β AtLat β (πΎ β Lat β§ π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯))) | ||
Theorem | atllat 37648 | An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.) |
β’ (πΎ β AtLat β πΎ β Lat) | ||
Theorem | atlpos 37649 | An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β AtLat β πΎ β Poset) | ||
Theorem | atl0dm 37650 | Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β AtLat β π΅ β dom πΊ) | ||
Theorem | atl0cl 37651 | An atomic lattice has a zero element. We can use this in place of op0cl 37532 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β AtLat β 0 β π΅) | ||
Theorem | atl0le 37652 | Orthoposet zero is less than or equal to any element. (ch0le 30169 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β 0 β€ π) | ||
Theorem | atlle0 37653 | An element less than or equal to zero equals zero. (chle0 30171 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β (π β€ 0 β π = 0 )) | ||
Theorem | atlltn0 37654 | A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β ( 0 < π β π β 0 )) | ||
Theorem | isat3 37655* | The predicate "is an atom". (elat2 31068 analog.) (Contributed by NM, 27-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) | ||
Theorem | atn0 37656 | An atom is not zero. (atne0 31073 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β π β 0 ) | ||
Theorem | atnle0 37657 | An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β Β¬ π β€ 0 ) | ||
Theorem | atlen0 37658 | A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β 0 ) | ||
Theorem | atcmp 37659 | If two atoms are comparable, they are equal. (atsseq 31075 analog.) (Contributed by NM, 13-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β€ π β π = π)) | ||
Theorem | atncmp 37660 | Frequently-used variation of atcmp 37659. (Contributed by NM, 29-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (Β¬ π β€ π β π β π)) | ||
Theorem | atnlt 37661 | Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ π < π) | ||
Theorem | atcvreq0 37662 | An element covered by an atom must be zero. (atcveq0 31076 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (ππΆπ β π = 0 )) | ||
Theorem | atncvrN 37663 | Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ ππΆπ) | ||
Theorem | atlex 37664* | Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 31088 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β 0 ) β βπ¦ β π΄ π¦ β€ π) | ||
Theorem | atnle 37665 | Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 31104 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) = 0 )) | ||
Theorem | atnem0 37666 | The meet of distinct atoms is zero. (atnemeq0 31105 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β π β (π β§ π) = 0 )) | ||
Theorem | atlatmstc 37667* | An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 31090 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅) β ( 1 β{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | atlatle 37668* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 31099 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | atlrelat1 37669* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 31091, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Definition | df-cvlat 37670* | Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.) |
β’ CvLat = {π β AtLat β£ βπ β (Atomsβπ)βπ β (Atomsβπ)βπ β (Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π))} | ||
Theorem | iscvlat 37671* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β CvLat β (πΎ β AtLat β§ βπ β π΄ βπ β π΄ βπ₯ β π΅ ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) | ||
Theorem | iscvlat2N 37672* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β CvLat β (πΎ β AtLat β§ βπ β π΄ βπ β π΄ βπ₯ β π΅ (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) | ||
Theorem | cvlatl 37673 | An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β AtLat) | ||
Theorem | cvllat 37674 | An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β Lat) | ||
Theorem | cvlposN 37675 | An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ (πΎ β CvLat β πΎ β Poset) | ||
Theorem | cvlexch1 37676 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch2 37677 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexchb1 37678 | An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexchb2 37679 | An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexch3 37680 | An atomic covering lattice has the exchange property. (atexch 31109 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch4N 37681 | An atomic covering lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlatexchb1 37682 | A version of cvlexchb1 37678 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlatexchb2 37683 | A version of cvlexchb2 37679 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | cvlatexch1 37684 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlatexch2 37685 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | cvlatexch3 37686 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π )) β (π β€ (π β¨ π ) β (π β¨ π) = (π β¨ π ))) | ||
Theorem | cvlcvr1 37687 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31083 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvlcvrp 37688 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31103 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr1 37689 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr2 37690 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlsupr2 37691 | Two equivalent ways of expressing that π is a superposition of π and π. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π ) = (π β¨ π ) β (π β π β§ π β π β§ π β€ (π β¨ π)))) | ||
Theorem | cvlsupr3 37692 | Two equivalent ways of expressing that π is a superposition of π and π, which can replace the superposition part of ishlat1 37700, (π₯ β π¦ β βπ§ β π΄(π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)) ), with the simpler βπ§ β π΄(π₯ β¨ π§) = (π¦ β¨ π§) as shown in ishlat3N 37702. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π ) = (π β¨ π ) β (π β π β (π β π β§ π β π β§ π β€ (π β¨ π))))) | ||
Theorem | cvlsupr4 37693 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β€ (π β¨ π)) | ||
Theorem | cvlsupr5 37694 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr6 37695 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr7 37696 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cvlsupr8 37697 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π )) | ||
Syntax | chlt 37698 | Extend class notation with Hilbert lattices. |
class HL | ||
Definition | df-hlat 37699* | Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.) |
β’ HL = {π β ((OML β© CLat) β© CvLat) β£ (βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))))} | ||
Theorem | ishlat1 37700* | The predicate "is a Hilbert lattice", which is: is orthomodular (πΎ β OML), complete (πΎ β CLat), atomic and satisfies the exchange (or covering) property (πΎ β CvLat), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |