HomeTheorem List (p. 331 of 357)
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. 331 of 357) | < 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-24318) |
Hilbert Space Explorer
(24319-25843) |
Users' Mathboxes
(25844-35614) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlcvl 33001 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
   
    | ||
| Theorem | hlatl 33002 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlol 33003 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlop 33004 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hllat 33005 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlomcmat 33006 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
 ![/\](wedge.gif "/\"){kind=small}
 | ||
| Theorem | hlpos 33007 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlatjcl 33008 | Closure of join operation. Frequently-used special case of latjcl 15219 for atoms. (Contributed by NM, 15-Jun-2012.) |
           
| ||
| Theorem | hlatjcom 33009 | Commutatitivity of join operation. Frequently-used special case of latjcom 15227 for atoms. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | hlatjidm 33010 | Idempotence of join operation. Frequently-used special case of latjcom 15227 for atoms. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | hlatjass 33011 | Lattice join is associative. Frequently-used special case of latjass 15263 for atoms. (Contributed by NM, 27-Jul-2012.) |
  
| ||
| Theorem | hlatj12 33012 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 15265 for atoms. (Contributed by NM, 4-Jun-2012.) |
|
| ||
| Theorem | hlatj32 33013 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 15265 for atoms. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | hlatjrot 33014 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 15268 for atoms. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | hlatj4 33015 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 15269 for atoms. (Contributed by NM, 9-Aug-2012.) |
| ||
| Theorem | hlatlej1 33016 | A join's first argument is less than or equal to the join. Special case of latlej1 15228 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
 
| ||
| Theorem | hlatlej2 33017 | A join's second argument is less than or equal to the join. Special case of latlej2 15229 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | glbconN 33018* |
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 33019* |
De Morgan's law for GLB and LUB. Index-set version of glbconN 33018, where
we read as
 .
(Contributed by NM, 17-Jan-2012.)
(New usage is discouraged.)
|
 
| ||
| Theorem | atnlej1 33020 | 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 33021 | 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 33022* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
 | ||
| Theorem | hlexch1 33023 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch2 33024 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | hlexchb1 33025 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
 | ||
| Theorem | hlexchb2 33026 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | hlsupr 33027* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
| ||
| Theorem | hlsupr2 33028* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
|
| ||
| Theorem | hlhgt4 33029* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
  
  
| ||
| Theorem | hlhgt2 33030* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hl0lt1N 33031 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlexch3 33032 | A Hilbert lattice has the exchange property. (atexch 25783 analog.) (Contributed by NM, 15-Nov-2011.) |
![./\](_.wedge.gif "./\"){kind=small}
 | ||
| Theorem | hlexch4N 33033 | 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 33034 | A version of hlexchb1 33025 for atoms. (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlatexchb2 33035 | A version of hlexchb2 33026 for atoms. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | hlatexch1 33036 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
|
| ||
| Theorem | hlatexch2 33037 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlatmstcOLDN 33038* | 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 25764 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
| | ||
| Theorem | hlatle 33039* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 25773 analog.) (Contributed by NM, 4-Nov-2011.) |
| ||
| Theorem | hlateq 33040* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 25775 analog.) (Contributed by NM, 24-May-2012.) |
|
| ||
| Theorem | hlrelat1 33041* |
An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of
[MaedaMaeda] p. 30. (chpssati 25765, with swapped, analog.)
(Contributed by NM, 4-Dec-2011.)
|
|
| ||
| Theorem | hlrelat5N 33042* | 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 33043* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 25766 analog.) (Contributed by NM, 4-Feb-2012.) |
|
| ||
| Theorem | hlrelat2 33044* | A consequence of relative atomicity. (chrelat2i 25767 analog.) (Contributed by NM, 5-Feb-2012.) |
|
| ||
| Theorem | exatleN 33045 | 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 33046* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
| ||
| Theorem | atex 33047 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
 | ||
| Theorem | intnatN 33048 | 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 33049 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnneN 33050 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvr1 33051 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 25757 analog.) (Contributed by NM, 17-Nov-2011.) |
 
| ||
| Theorem | cvr2N 33052 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 25758 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat3 33053* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 33043. (Contributed by NM, 2-May-2012.) |
|
| ||
| Theorem | cvrval3 33054* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.)
|
|
| ||
| Theorem | cvrval4N 33055* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cvrval5 33056* |
Binary relation expressing covers
. (Contributed by
NM, 7-Dec-2012.)
|
|
| ||
| Theorem | cvrp 33057 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 25777 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | atcvr1 33058 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvr2 33059 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | cvrexchlem 33060 | Lemma for cvrexch 33061. (cvexchlem 25770 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvrexch 33061 | 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 25771 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvratlem 33062 | Lemma for cvrat 33063. (atcvatlem 25787 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | cvrat 33063 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 25788 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | ltltncvr 33064 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
| ||
| Theorem | ltcvrntr 33065 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | cvrntr 33066 | The covers relation is not transitive. (cvntr 25694 analog.) (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | atcvr0eq 33067 | The covers relation is not transitive. (atcv0eq 25781 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | lnnat 33068 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | atcvrj0 33069 | Two atoms covering the zero subspace are equal. (atcv1 25782 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | cvrat2 33070 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 25789 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | atcvrneN 33071 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atcvrj1 33072 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2b 33073 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2 33074 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atleneN 33075 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atltcvr 33076 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atle 33077* | Any non-zero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
|
| ||
| Theorem | atlt 33078 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atlelt 33079 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
|
| ||
| Theorem | 2atlt 33080* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atexchcvrN 33081 | Atom exchange property. Version of hlatexch2 33037 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atexchltN 33082 | Atom exchange property. Version of hlatexch2 33037 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvrat3 33083 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 25798 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat4 33084* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 25799 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat42 33085* | Commuted version of cvrat4 33084. (Contributed by NM, 28-Jan-2012.) |
|
| ||
| Theorem | 2atjm 33086 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
|
| ||
| Theorem | atbtwn 33087 |
Property of a 3rd atom on a line
intersecting element
at . (Contributed by NM,
30-Jul-2012.)
|
|
| ||
| Theorem | atbtwnexOLDN 33088* |
There exists a 3rd atom
on a line intersecting element
at , such that is different from and not in
. (Contributed
by NM, 30-Jul-2012.)
(New usage is discouraged.)
|
|
| ||
| Theorem | atbtwnex 33089* |
Given atoms in and not in , there exists an atom
not in such that the line intersects at
. (Contributed
by NM, 1-Aug-2012.)
|
|
| ||
| Theorem | 3noncolr2 33090 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 3noncolr1N 33091 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlatcon3 33092 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | hlatcon2 33093 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | 4noncolr3 33094 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4noncolr2 33095 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4noncolr1 33096 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | athgt 33097* | A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.) |
| ||
| Theorem | 3dim0 33098* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem1 33099 | Lemma for 3dim1 33108. (Contributed by NM, 25-Jul-2012.) |
| ||
| Theorem | 3dimlem2 33100 | Lemma for 3dim1 33108. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |