![]() |
Metamath
Proof Explorer Theorem List (p. 389 of 484) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvrcon3b 38801 | Contraposition law for the covers relation. (cvcon3 32133 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (ππΆπ β ( β₯ βπ)πΆ( β₯ βπ))) | ||
Theorem | cvrle 38802 | The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) | ||
Theorem | cvrnbtwn4 38803 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 32138 analog.) (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π))) | ||
Theorem | cvrnle 38804 | 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 38805 | The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ (((πΎ β π΄ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β π) | ||
Theorem | cvrnrefN 38806 | The covers relation is not reflexive. (cvnref 32140 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β Β¬ ππΆπ) | ||
Theorem | cvrcmp 38807 | 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 38808 | 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 38809* | The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β π΄ = {π₯ β π΅ β£ 0 πΆπ₯}) | ||
Theorem | isat 38810 | The predicate "is an atom". (ela 32188 analog.) (Contributed by NM, 18-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β π· β (π β π΄ β (π β π΅ β§ 0 πΆπ))) | ||
Theorem | isat2 38811 | The predicate "is an atom". (elatcv0 32190 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΅) β (π β π΄ β 0 πΆπ)) | ||
Theorem | atcvr0 38812 | An atom covers zero. (atcv0 32191 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β π· β§ π β π΄) β 0 πΆπ) | ||
Theorem | atbase 38813 | An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32193 analog.) (Contributed by NM, 10-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β π΄ β π β π΅) | ||
Theorem | atssbase 38814 | The set of atoms is a subset of the base set. (atssch 32192 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ π΄ β π΅ | ||
Theorem | 0ltat 38815 | An atom is greater than zero. (Contributed by NM, 4-Jul-2012.) |
β’ 0 = (0.βπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΄) β 0 < π) | ||
Theorem | leatb 38816 | A poset element less than or equal to an atom equals either zero or the atom. (atss 32195 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β OP β§ π β π΅ β§ π β π΄) β (π β€ π β (π = π β¨ π = 0 ))) | ||
Theorem | leat 38817 | 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 38818 | 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 38819 | 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 38820 | 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 38821 | 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 38822* | 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 38823* | 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 38824 | An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.) |
β’ (πΎ β AtLat β πΎ β Lat) | ||
Theorem | atlpos 38825 | An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β AtLat β πΎ β Poset) | ||
Theorem | atl0dm 38826 | Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β AtLat β π΅ β dom πΊ) | ||
Theorem | atl0cl 38827 | An atomic lattice has a zero element. We can use this in place of op0cl 38708 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β AtLat β 0 β π΅) | ||
Theorem | atl0le 38828 | Orthoposet zero is less than or equal to any element. (ch0le 31290 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β 0 β€ π) | ||
Theorem | atlle0 38829 | An element less than or equal to zero equals zero. (chle0 31292 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β (π β€ 0 β π = 0 )) | ||
Theorem | atlltn0 38830 | A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) β β’ ((πΎ β AtLat β§ π β π΅) β ( 0 < π β π β 0 )) | ||
Theorem | isat3 38831* | The predicate "is an atom". (elat2 32189 analog.) (Contributed by NM, 27-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) | ||
Theorem | atn0 38832 | An atom is not zero. (atne0 32194 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β π β 0 ) | ||
Theorem | atnle0 38833 | An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β Β¬ π β€ 0 ) | ||
Theorem | atlen0 38834 | 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 38835 | If two atoms are comparable, they are equal. (atsseq 32196 analog.) (Contributed by NM, 13-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β€ π β π = π)) | ||
Theorem | atncmp 38836 | Frequently-used variation of atcmp 38835. (Contributed by NM, 29-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (Β¬ π β€ π β π β π)) | ||
Theorem | atnlt 38837 | Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ π < π) | ||
Theorem | atcvreq0 38838 | An element covered by an atom must be zero. (atcveq0 32197 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (ππΆπ β π = 0 )) | ||
Theorem | atncvrN 38839 | Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β Β¬ ππΆπ) | ||
Theorem | atlex 38840* | Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 32209 analog.) (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΅ β§ π β 0 ) β βπ¦ β π΄ π¦ β€ π) | ||
Theorem | atnle 38841 | Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 32225 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) = 0 )) | ||
Theorem | atnem0 38842 | The meet of distinct atoms is zero. (atnemeq0 32226 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β π β (π β§ π) = 0 )) | ||
Theorem | atlatmstc 38843* | 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 32211 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅) β ( 1 β{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | atlatle 38844* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32220 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | atlrelat1 38845* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32212, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Definition | df-cvlat 38846* | 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 38847* | 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 38848* | 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 38849 | An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β AtLat) | ||
Theorem | cvllat 38850 | An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β CvLat β πΎ β Lat) | ||
Theorem | cvlposN 38851 | An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ (πΎ β CvLat β πΎ β Poset) | ||
Theorem | cvlexch1 38852 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch2 38853 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexchb1 38854 | An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexchb2 38855 | An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlexch3 38856 | An atomic covering lattice has the exchange property. (atexch 32230 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlexch4N 38857 | 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 38858 | A version of cvlexchb1 38854 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | cvlatexchb2 38859 | A version of cvlexchb2 38855 for atoms. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | cvlatexch1 38860 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | cvlatexch2 38861 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | cvlatexch3 38862 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π )) β (π β€ (π β¨ π ) β (π β¨ π) = (π β¨ π ))) | ||
Theorem | cvlcvr1 38863 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32204 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvlcvrp 38864 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32224 analog.) (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr1 38865 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlatcvr2 38866 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvlsupr2 38867 | Two equivalent ways of expressing that π is a superposition of π and π. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π ) = (π β¨ π ) β (π β π β§ π β π β§ π β€ (π β¨ π)))) | ||
Theorem | cvlsupr3 38868 | Two equivalent ways of expressing that π is a superposition of π and π, which can replace the superposition part of ishlat1 38876, (π₯ β π¦ β βπ§ β π΄(π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)) ), with the simpler βπ§ β π΄(π₯ β¨ π§) = (π¦ β¨ π§) as shown in ishlat3N 38878. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π ) = (π β¨ π ) β (π β π β (π β π β§ π β π β§ π β€ (π β¨ π))))) | ||
Theorem | cvlsupr4 38869 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β€ (π β¨ π)) | ||
Theorem | cvlsupr5 38870 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr6 38871 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr7 38872 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cvlsupr8 38873 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π )) | ||
Syntax | chlt 38874 | Extend class notation with Hilbert lattices. |
class HL | ||
Definition | df-hlat 38875* | 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 38876* | 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 ))))) | ||
Theorem | ishlat2 38877* | The predicate "is a Hilbert lattice". Here we replace πΎ β CvLat with the weaker πΎ β AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ (βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) | ||
Theorem | ishlat3N 38878* | The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form βπ§ β π΄(π₯ β¨ π§) = (π¦ β¨ π§). The exchange property and atomicity are provided by πΎ β CvLat, and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) | ||
Theorem | ishlatiN 38879* | Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.) |
β’ πΎ β OML & β’ πΎ β CLat & β’ πΎ β AtLat & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) & β’ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )) β β’ πΎ β HL | ||
Theorem | hlomcmcv 38880 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat)) | ||
Theorem | hloml 38881 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OML) | ||
Theorem | hlclat 38882 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β CLat) | ||
Theorem | hlcvl 38883 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β πΎ β CvLat) | ||
Theorem | hlatl 38884 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β AtLat) | ||
Theorem | hlol 38885 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OL) | ||
Theorem | hlop 38886 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OP) | ||
Theorem | hllat 38887 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Lat) | ||
Theorem | hllatd 38888 | Deduction form of hllat 38887. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.) |
β’ (π β πΎ β HL) β β’ (π β πΎ β Lat) | ||
Theorem | hlomcmat 38889 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) | ||
Theorem | hlpos 38890 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Poset) | ||
Theorem | hlatjcl 38891 | Closure of join operation. Frequently-used special case of latjcl 18425 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΅) | ||
Theorem | hlatjcom 38892 | Commutatitivity of join operation. Frequently-used special case of latjcom 18433 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) | ||
Theorem | hlatjidm 38893 | Idempotence of join operation. Frequently-used special case of latjcom 18433 for atoms. (Contributed by NM, 15-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) | ||
Theorem | hlatjass 38894 | Lattice join is associative. Frequently-used special case of latjass 18469 for atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj12 38895 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18471 for atoms. (Contributed by NM, 4-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π )) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj32 38896 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18471 for atoms. (Contributed by NM, 21-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π ) β¨ π)) | ||
Theorem | hlatjrot 38897 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18474 for atoms. (Contributed by NM, 2-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | hlatj4 38898 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18475 for atoms. (Contributed by NM, 9-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π ) β¨ (π β¨ π))) | ||
Theorem | hlatlej1 38899 | A join's first argument is less than or equal to the join. Special case of latlej1 18434 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) | ||
Theorem | hlatlej2 38900 | A join's second argument is less than or equal to the join. Special case of latlej2 18435 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |