HomeTheorem List (p. 329 of 402)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 329 of 402) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-26513) |
Hilbert Space Explorer
(26514-28036) |
Users' Mathboxes
(28037-40133) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iscvlat 32801* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) |
           
        ![/\](wedge.gif "/\"){kind=small}  
    | ||
| Theorem | iscvlat2N 32802* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
![./\](_.wedge.gif "./\"){kind=small}
  
| ||
| Theorem | cvlatl 32803 | An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvllat 32804 | An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.) |
 | ||
| Theorem | cvlposN 32805 | An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
 | ||
| Theorem | cvlexch1 32806 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.) |
  
| ||
| Theorem | cvlexch2 32807 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | cvlexchb1 32808 | An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
|
| ||
| Theorem | cvlexchb2 32809 | An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | cvlexch3 32810 | An atomic covering lattice has the exchange property. (atexch 27976 analog.) (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlexch4N 32811 | 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.) |
|
| ||
| Theorem | cvlatexchb1 32812 | A version of cvlexchb1 32808 for atoms. (Contributed by NM, 5-Nov-2012.) |
 
| ||
| Theorem | cvlatexchb2 32813 | A version of cvlexchb2 32809 for atoms. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch1 32814 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch2 32815 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch3 32816 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cvlcvr1 32817 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27950 analog.) (Contributed by NM, 5-Nov-2012.) |
   
| ||
| Theorem | cvlcvrp 32818 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27970 analog.) (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatcvr1 32819 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatcvr2 32820 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlsupr2 32821 |
Two equivalent ways of expressing that is a superposition of
and .
(Contributed by NM, 5-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr3 32822 |
Two equivalent ways of expressing that is a superposition of
and , which can
replace the superposition part of ishlat1 32830,
 
, with the
simpler as
shown in ishlat3N 32832. (Contributed by NM, 5-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr4 32823 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr5 32824 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr6 32825 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr7 32826 |
Consequence of superposition condition
.
(Contributed by NM, 24-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr8 32827 |
Consequence of superposition condition
.
(Contributed by NM, 24-Nov-2012.)
|
|
| ||
| Syntax | chlt 32828 | Extend class notation with Hilbert lattices. |
  | ||
| Definition | df-hlat 32829* | Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.) |
 
   
   | ||
| Theorem | ishlat1 32830* |
The predicate "is a Hilbert lattice," which is orthomodular
( ), complete ( ), atomic and satisfying the
exchange (or covering) property (
),
satisfies the
superposition principle, and has a minimum height of 4. (Contributed by
NM, 5-Nov-2012.)
|
| ||
| Theorem | ishlat2 32831* |
The predicate "is a Hilbert lattice". Here we replace
with the weaker and show the
exchange property
explicitly. (Contributed by NM, 5-Nov-2012.)
|
|
| ||
| Theorem | ishlat3N 32832* |
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 , and
"minimum height 4" is
shown explicitly. (Contributed by NM, 8-Nov-2012.)
(New usage is discouraged.)
|
|
| ||
| Theorem | ishlatiN 32833* | Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlomcmcv 32834 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hloml 32835 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlclat 32836 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlcvl 32837 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hlatl 32838 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlol 32839 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlop 32840 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hllat 32841 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlomcmat 32842 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hlpos 32843 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlatjcl 32844 | Closure of join operation. Frequently-used special case of latjcl 16240 for atoms. (Contributed by NM, 15-Jun-2012.) |
| ||
| Theorem | hlatjcom 32845 | Commutatitivity of join operation. Frequently-used special case of latjcom 16248 for atoms. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | hlatjidm 32846 | Idempotence of join operation. Frequently-used special case of latjcom 16248 for atoms. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | hlatjass 32847 | Lattice join is associative. Frequently-used special case of latjass 16284 for atoms. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | hlatj12 32848 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 16286 for atoms. (Contributed by NM, 4-Jun-2012.) |
|
| ||
| Theorem | hlatj32 32849 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 16286 for atoms. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | hlatjrot 32850 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 16289 for atoms. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | hlatj4 32851 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 16290 for atoms. (Contributed by NM, 9-Aug-2012.) |
| ||
| Theorem | hlatlej1 32852 | A join's first argument is less than or equal to the join. Special case of latlej1 16249 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | hlatlej2 32853 | A join's second argument is less than or equal to the join. Special case of latlej2 16250 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | glbconN 32854* |
De Morgan's law for GLB and LUB. This holds in any complete
ortholattice, although we assume for convenience. (Contributed
by NM, 17-Jan-2012.) (New usage is discouraged.)
|
    
 
| ||
| Theorem | glbconxN 32855* |
De Morgan's law for GLB and LUB. Index-set version of glbconN 32854, where
we read as
 .
(Contributed by NM, 17-Jan-2012.)
(New usage is discouraged.)
|
| ||
| Theorem | atnlej1 32856 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | atnlej2 32857 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlsuprexch 32858* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch1 32859 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch2 32860 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | hlexchb1 32861 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
|
| ||
| Theorem | hlexchb2 32862 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | hlsupr 32863* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
| ||
| Theorem | hlsupr2 32864* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
|
| ||
| Theorem | hlhgt4 32865* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hlhgt2 32866* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hl0lt1N 32867 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlexch3 32868 | A Hilbert lattice has the exchange property. (atexch 27976 analog.) (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlexch4N 32869 | A Hilbert lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 15-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlatexchb1 32870 | A version of hlexchb1 32861 for atoms. (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlatexchb2 32871 | A version of hlexchb2 32862 for atoms. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | hlatexch1 32872 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
|
| ||
| Theorem | hlatexch2 32873 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlatmstcOLDN 32874* | 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 27957 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
| | ||
| Theorem | hlatle 32875* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 27966 analog.) (Contributed by NM, 4-Nov-2011.) |
|
| ||
| Theorem | hlateq 32876* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 27968 analog.) (Contributed by NM, 24-May-2012.) |
|
| ||
| Theorem | hlrelat1 32877* |
An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of
[MaedaMaeda] p. 30. (chpssati 27958, with swapped, analog.)
(Contributed by NM, 4-Dec-2011.)
|
|
| ||
| Theorem | hlrelat5N 32878* | An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat 32879* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 27959 analog.) (Contributed by NM, 4-Feb-2012.) |
|
| ||
| Theorem | hlrelat2 32880* | A consequence of relative atomicity. (chrelat2i 27960 analog.) (Contributed by NM, 5-Feb-2012.) |
|
| ||
| Theorem | exatleN 32881 | A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hl2at 32882* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
|
| ||
| Theorem | atex 32883 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
 | ||
| Theorem | intnatN 32884 | If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnne2N 32885 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnneN 32886 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvr1 32887 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27950 analog.) (Contributed by NM, 17-Nov-2011.) |
|
| ||
| Theorem | cvr2N 32888 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 27951 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat3 32889* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 32879. (Contributed by NM, 2-May-2012.) |
|
| ||
| Theorem | cvrval3 32890* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.)
|
|
| ||
| Theorem | cvrval4N 32891* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cvrval5 32892* |
Binary relation expressing covers
. (Contributed by
NM, 7-Dec-2012.)
|
|
| ||
| Theorem | cvrp 32893 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27970 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | atcvr1 32894 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvr2 32895 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | cvrexchlem 32896 | Lemma for cvrexch 32897. (cvexchlem 27963 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvrexch 32897 | A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (cvexchi 27964 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvratlem 32898 | Lemma for cvrat 32899. (atcvatlem 27980 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | cvrat 32899 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 27981 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | ltltncvr 32900 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |