HomeTheorem List (p. 330 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. 330 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-26569) |
Hilbert Space Explorer
(26570-28092) |
Users' Mathboxes
(28093-40161) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlatjcl 32901 | Closure of join operation. Frequently-used special case of latjcl 16296 for atoms. (Contributed by NM, 15-Jun-2012.) |
                ![/\](wedge.gif "/\"){kind=small}  
| ||
| Theorem | hlatjcom 32902 | Commutatitivity of join operation. Frequently-used special case of latjcom 16304 for atoms. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | hlatjidm 32903 | Idempotence of join operation. Frequently-used special case of latjcom 16304 for atoms. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | hlatjass 32904 | Lattice join is associative. Frequently-used special case of latjass 16340 for atoms. (Contributed by NM, 27-Jul-2012.) |
  
| ||
| Theorem | hlatj12 32905 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 16342 for atoms. (Contributed by NM, 4-Jun-2012.) |
|
| ||
| Theorem | hlatj32 32906 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 16342 for atoms. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | hlatjrot 32907 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 16345 for atoms. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | hlatj4 32908 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 16346 for atoms. (Contributed by NM, 9-Aug-2012.) |
| ||
| Theorem | hlatlej1 32909 | A join's first argument is less than or equal to the join. Special case of latlej1 16305 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
 
| ||
| Theorem | hlatlej2 32910 | A join's second argument is less than or equal to the join. Special case of latlej2 16306 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | glbconN 32911* |
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 32912* |
De Morgan's law for GLB and LUB. Index-set version of glbconN 32911, where
we read as
 .
(Contributed by NM, 17-Jan-2012.)
(New usage is discouraged.)
|
 
| ||
| Theorem | atnlej1 32913 | 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 32914 | 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 32915* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
 | ||
| Theorem | hlexch1 32916 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch2 32917 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | hlexchb1 32918 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
 | ||
| Theorem | hlexchb2 32919 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | hlsupr 32920* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
| ||
| Theorem | hlsupr2 32921* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
|
| ||
| Theorem | hlhgt4 32922* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
  
  
| ||
| Theorem | hlhgt2 32923* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hl0lt1N 32924 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlexch3 32925 | A Hilbert lattice has the exchange property. (atexch 28032 analog.) (Contributed by NM, 15-Nov-2011.) |
![./\](_.wedge.gif "./\"){kind=small}
 | ||
| Theorem | hlexch4N 32926 | 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 32927 | A version of hlexchb1 32918 for atoms. (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlatexchb2 32928 | A version of hlexchb2 32919 for atoms. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | hlatexch1 32929 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
|
| ||
| Theorem | hlatexch2 32930 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlatmstcOLDN 32931* | 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 28013 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
| | ||
| Theorem | hlatle 32932* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 28022 analog.) (Contributed by NM, 4-Nov-2011.) |
| ||
| Theorem | hlateq 32933* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 28024 analog.) (Contributed by NM, 24-May-2012.) |
|
| ||
| Theorem | hlrelat1 32934* |
An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of
[MaedaMaeda] p. 30. (chpssati 28014, with swapped, analog.)
(Contributed by NM, 4-Dec-2011.)
|
|
| ||
| Theorem | hlrelat5N 32935* | 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 32936* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 28015 analog.) (Contributed by NM, 4-Feb-2012.) |
|
| ||
| Theorem | hlrelat2 32937* | A consequence of relative atomicity. (chrelat2i 28016 analog.) (Contributed by NM, 5-Feb-2012.) |
|
| ||
| Theorem | exatleN 32938 | 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 32939* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
| ||
| Theorem | atex 32940 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
 | ||
| Theorem | intnatN 32941 | 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 32942 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnneN 32943 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvr1 32944 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 28006 analog.) (Contributed by NM, 17-Nov-2011.) |
 
| ||
| Theorem | cvr2N 32945 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 28007 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat3 32946* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 32936. (Contributed by NM, 2-May-2012.) |
|
| ||
| Theorem | cvrval3 32947* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.)
|
|
| ||
| Theorem | cvrval4N 32948* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cvrval5 32949* |
Binary relation expressing covers
. (Contributed by
NM, 7-Dec-2012.)
|
|
| ||
| Theorem | cvrp 32950 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28026 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | atcvr1 32951 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvr2 32952 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | cvrexchlem 32953 | Lemma for cvrexch 32954. (cvexchlem 28019 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvrexch 32954 | 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 28020 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvratlem 32955 | Lemma for cvrat 32956. (atcvatlem 28036 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | cvrat 32956 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 28037 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | ltltncvr 32957 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
| ||
| Theorem | ltcvrntr 32958 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | cvrntr 32959 | The covers relation is not transitive. (cvntr 27943 analog.) (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | atcvr0eq 32960 | The covers relation is not transitive. (atcv0eq 28030 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | lnnat 32961 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | atcvrj0 32962 | Two atoms covering the zero subspace are equal. (atcv1 28031 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | cvrat2 32963 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 28038 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | atcvrneN 32964 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atcvrj1 32965 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2b 32966 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2 32967 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atleneN 32968 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atltcvr 32969 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atle 32970* | Any non-zero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
|
| ||
| Theorem | atlt 32971 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atlelt 32972 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
|
| ||
| Theorem | 2atlt 32973* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atexchcvrN 32974 | Atom exchange property. Version of hlatexch2 32930 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atexchltN 32975 | Atom exchange property. Version of hlatexch2 32930 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvrat3 32976 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28047 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat4 32977* | 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 28048 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat42 32978* | Commuted version of cvrat4 32977. (Contributed by NM, 28-Jan-2012.) |
|
| ||
| Theorem | 2atjm 32979 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
|
| ||
| Theorem | atbtwn 32980 |
Property of a 3rd atom on a line
intersecting element
at . (Contributed by NM,
30-Jul-2012.)
|
|
| ||
| Theorem | atbtwnexOLDN 32981* |
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 32982* |
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 32983 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 3noncolr1N 32984 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlatcon3 32985 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | hlatcon2 32986 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | 4noncolr3 32987 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4noncolr2 32988 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4noncolr1 32989 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | athgt 32990* | 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 32991* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem1 32992 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) |
| ||
| Theorem | 3dimlem2 32993 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3a 32994 | Lemma for 3dim3 33003. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3 32995 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3OLDN 32996 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | 3dimlem4a 32997 | Lemma for 3dim3 33003. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 3dimlem4 32998 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem4OLDN 32999 | Lemma for 3dim1 33001. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | 3dim1lem5 33000* | Lemma for 3dim1 33001. (Contributed by NM, 26-Jul-2012.) |
  
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |