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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | omllaw2N 37601 | Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 30325 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β (π β¨ (( β₯ βπ) β§ π)) = π)) | ||
Theorem | omllaw3 37602 | Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 30176 analog.) (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β€ π β§ (π β§ ( β₯ βπ)) = 0 ) β π = π)) | ||
Theorem | omllaw4 37603 | Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β (( β₯ β(( β₯ βπ) β§ π)) β§ π) = π)) | ||
Theorem | omllaw5N 37604 | The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 30353 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ (( β₯ βπ) β§ (π β¨ π))) = (π β¨ π)) | ||
Theorem | cmtcomlemN 37605 | Lemma for cmtcomN 37606. (cmcmlem 30331 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) | ||
Theorem | cmtcomN 37606 | Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 30332 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) | ||
Theorem | cmt2N 37607 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 30333 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆ( β₯ βπ))) | ||
Theorem | cmt3N 37608 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 30335 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆπ)) | ||
Theorem | cmt4N 37609 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 30335 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆ( β₯ βπ))) | ||
Theorem | cmtbr2N 37610 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 30336 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) | ||
Theorem | cmtbr3N 37611 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 30348 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π))) | ||
Theorem | cmtbr4N 37612 | Alternate definition for the commutes relation. (cmbr4i 30341 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) β€ π)) | ||
Theorem | lecmtN 37613 | Ordered elements commute. (lecmi 30342 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β ππΆπ)) | ||
Theorem | cmtidN 37614 | Any element commutes with itself. (cmidi 30350 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ π β π΅) β ππΆπ) | ||
Theorem | omlfh1N 37615 | 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 30358 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) | ||
Theorem | omlfh3N 37616 | Foulis-Holland Theorem, part 3. Dual of omlfh1N 37615. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ (π β¨ π))) | ||
Theorem | omlmod1i2N 37617 | Analogue of modular law atmod1i2 38217 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = (cmβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) | ||
Theorem | omlspjN 37618 | Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β¨ ( β₯ βπ)) β§ π) = π) | ||
Syntax | ccvr 37619 | Extend class notation with covers relation. |
class β | ||
Syntax | catm 37620 | Extend class notation with atoms. |
class Atoms | ||
Syntax | cal 37621 | Extend class notation with atomic lattices. |
class AtLat | ||
Syntax | clc 37622 | Extend class notation with lattices with the covering property. |
class CvLat | ||
Definition | df-covers 37623* | 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 37626 for the relation form. (Contributed by NM, 18-Sep-2011.) |
β’ β = (π β V β¦ {β¨π, πβ© β£ ((π β (Baseβπ) β§ π β (Baseβπ)) β§ π(ltβπ)π β§ Β¬ βπ§ β (Baseβπ)(π(ltβπ)π§ β§ π§(ltβπ)π))}) | ||
Definition | df-ats 37624* | Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.) |
β’ Atoms = (π β V β¦ {π β (Baseβπ) β£ (0.βπ)( β βπ)π}) | ||
Theorem | cvrfval 37625* | Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ (πΎ β π΄ β πΆ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ < π¦ β§ Β¬ βπ§ β π΅ (π₯ < π§ β§ π§ < π¦))}) | ||
Theorem | cvrval 37626* | 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 31022 analog.) (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)))) | ||
Theorem | cvrlt 37627 | The covers relation implies the less-than relation. (cvpss 31025 analog.) (Contributed by NM, 8-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π < π) | ||
Theorem | cvrnbtwn 37628 | There is no element between the two arguments of the covers relation. (cvnbtwn 31026 analog.) (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β Β¬ (π < π β§ π < π)) | ||
Theorem | ncvr1 37629 | No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ π β π΅) β Β¬ 1 πΆπ) | ||
Theorem | cvrletrN 37630 | Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ π β€ π) β π < π)) | ||
Theorem | cvrval2 37631* | Binary relation expressing π covers π. Definition of covers in [Kalmbach] p. 15. (cvbr2 31023 analog.) (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π)))) | ||
Theorem | cvrnbtwn2 37632 | The covers relation implies no in-betweenness. (cvnbtwn2 31027 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π < π β§ π β€ π) β π = π)) | ||
Theorem | cvrnbtwn3 37633 | The covers relation implies no in-betweenness. (cvnbtwn3 31028 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π < π) β π = π)) | ||
Theorem | cvrcon3b 37634 | Contraposition law for the covers relation. (cvcon3 31024 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆ( β₯ βπ))) | ||
Theorem | cvrle 37635 | The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) | ||
Theorem | cvrnbtwn4 37636 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 31029 analog.) (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π))) | ||
Theorem | cvrnle 37637 | 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 37638 | The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β π) | ||
Theorem | cvrnrefN 37639 | The covers relation is not reflexive. (cvnref 31031 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β Β¬ ππΆπ) | ||
Theorem | cvrcmp 37640 | 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 37641 | 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 37642* | The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β π΄ = {π₯ β π΅ β£ 0 πΆπ₯}) | ||
Theorem | isat 37643 | The predicate "is an atom". (ela 31079 analog.) (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β (π β π΄ β (π β π΅ β§ 0 πΆπ))) | ||
Theorem | isat2 37644 | The predicate "is an atom". (elatcv0 31081 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΅) β (π β π΄ β 0 πΆπ)) | ||
Theorem | atcvr0 37645 | An atom covers zero. (atcv0 31082 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΄) β 0 πΆπ) | ||
Theorem | atbase 37646 | An atom is a member of the lattice base set (i.e. a lattice element). (atelch 31084 analog.) (Contributed by NM, 10-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β π΄ β π β π΅) | ||
Theorem | atssbase 37647 | The set of atoms is a subset of the base set. (atssch 31083 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ π΄ β π΅ | ||
Theorem | 0ltat 37648 | An atom is greater than zero. (Contributed by NM, 4-Jul-2012.) |
β’ 0 = (0.βπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΄) β 0 < π) | ||
Theorem | leatb 37649 | A poset element less than or equal to an atom equals either zero or the atom. (atss 31086 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΄) β (π β€ π β (π = π β¨ π = 0 ))) | ||
Theorem | leat 37650 | 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 37651 | 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 37652 | 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 37653 | 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 37654 | 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 37655* | 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 37656* | 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 37657 | An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.) |
β’ (πΎ β AtLat β πΎ β Lat) | ||
Theorem | atlpos 37658 | An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β AtLat β πΎ β Poset) | ||
Theorem | atl0dm 37659 | Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β AtLat β π΅ β dom πΊ) | ||
Theorem | atl0cl 37660 | An atomic lattice has a zero element. We can use this in place of op0cl 37541 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β AtLat β 0 β π΅) | ||
Theorem | atl0le 37661 | Orthoposet zero is less than or equal to any element. (ch0le 30181 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β 0 β€ π) | ||
Theorem | atlle0 37662 | An element less than or equal to zero equals zero. (chle0 30183 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β (π β€ 0 β π = 0 )) | ||
Theorem | atlltn0 37663 | A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β ( 0 < π β π β 0 )) | ||
Theorem | isat3 37664* | The predicate "is an atom". (elat2 31080 analog.) (Contributed by NM, 27-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) | ||
Theorem | atn0 37665 | An atom is not zero. (atne0 31085 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β π β 0 ) | ||
Theorem | atnle0 37666 | An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β Β¬ π β€ 0 ) | ||
Theorem | atlen0 37667 | 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 37668 | If two atoms are comparable, they are equal. (atsseq 31087 analog.) (Contributed by NM, 13-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β€ π β π = π)) | ||
Theorem | atncmp 37669 | Frequently-used variation of atcmp 37668. (Contributed by NM, 29-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (Β¬ π β€ π β π β π)) | ||
Theorem | atnlt 37670 | Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ π < π) | ||
Theorem | atcvreq0 37671 | An element covered by an atom must be zero. (atcveq0 31088 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (ππΆπ β π = 0 )) | ||
Theorem | atncvrN 37672 | Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ ππΆπ) | ||
Theorem | atlex 37673* | Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 31100 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β 0 ) β βπ¦ β π΄ π¦ β€ π) | ||
Theorem | atnle 37674 | Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 31116 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) = 0 )) | ||
Theorem | atnem0 37675 | The meet of distinct atoms is zero. (atnemeq0 31117 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β π β (π β§ π) = 0 )) | ||
Theorem | atlatmstc 37676* | 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 31102 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅) β ( 1 β{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | atlatle 37677* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 31111 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | atlrelat1 37678* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 31103, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Definition | df-cvlat 37679* | 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 37680* | 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 37681* | 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 37682 | An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β AtLat) | ||
Theorem | cvllat 37683 | An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β Lat) | ||
Theorem | cvlposN 37684 | An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ (πΎ β CvLat β πΎ β Poset) | ||
Theorem | cvlexch1 37685 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch2 37686 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexchb1 37687 | An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexchb2 37688 | An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexch3 37689 | An atomic covering lattice has the exchange property. (atexch 31121 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch4N 37690 | 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 37691 | A version of cvlexchb1 37687 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlatexchb2 37692 | A version of cvlexchb2 37688 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | cvlatexch1 37693 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlatexch2 37694 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | cvlatexch3 37695 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π )) β (π β€ (π β¨ π ) β (π β¨ π) = (π β¨ π ))) | ||
Theorem | cvlcvr1 37696 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31095 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvlcvrp 37697 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31115 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr1 37698 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr2 37699 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlsupr2 37700 | Two equivalent ways of expressing that π is a superposition of π and π. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π ) = (π β¨ π ) β (π β π β§ π β π β§ π β€ (π β¨ π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |