HomeTheorem List (p. 343 of 370)
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. 343 of 370) | < 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-25539) |
Hilbert Space Explorer
(25540-27064) |
Users' Mathboxes
(27065-36941) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlsupr2 34201* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
              ![/\](wedge.gif "/\"){kind=small}  
  
| ||
| Theorem | hlhgt4 34202* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
    
  
 
| ||
| Theorem | hlhgt2 34203* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hl0lt1N 34204 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlexch3 34205 | A Hilbert lattice has the exchange property. (atexch 27004 analog.) (Contributed by NM, 15-Nov-2011.) |
 
![./\](_.wedge.gif "./\"){kind=small}
  | ||
| Theorem | hlexch4N 34206 | 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 34207 | A version of hlexchb1 34198 for atoms. (Contributed by NM, 15-Nov-2011.) |
 | ||
| Theorem | hlatexchb2 34208 | A version of hlexchb2 34199 for atoms. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | hlatexch1 34209 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
|
| ||
| Theorem | hlatexch2 34210 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlatmstcOLDN 34211* | 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 26985 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
     | ||
| Theorem | hlatle 34212* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 26994 analog.) (Contributed by NM, 4-Nov-2011.) |
  
| ||
| Theorem | hlateq 34213* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 26996 analog.) (Contributed by NM, 24-May-2012.) |
|
| ||
| Theorem | hlrelat1 34214* |
An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of
[MaedaMaeda] p. 30. (chpssati 26986, with swapped, analog.)
(Contributed by NM, 4-Dec-2011.)
|
 | ||
| Theorem | hlrelat5N 34215* | 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 34216* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 26987 analog.) (Contributed by NM, 4-Feb-2012.) |
|
| ||
| Theorem | hlrelat2 34217* | A consequence of relative atomicity. (chrelat2i 26988 analog.) (Contributed by NM, 5-Feb-2012.) |
|
| ||
| Theorem | exatleN 34218 | 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 34219* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
| ||
| Theorem | atex 34220 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
 | ||
| Theorem | intnatN 34221 | 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 34222 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnneN 34223 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvr1 34224 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 26978 analog.) (Contributed by NM, 17-Nov-2011.) |
 
| ||
| Theorem | cvr2N 34225 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 26979 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat3 34226* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 34216. (Contributed by NM, 2-May-2012.) |
|
| ||
| Theorem | cvrval3 34227* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.)
|
|
| ||
| Theorem | cvrval4N 34228* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cvrval5 34229* |
Binary relation expressing covers
. (Contributed by
NM, 7-Dec-2012.)
|
|
| ||
| Theorem | cvrp 34230 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 26998 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | atcvr1 34231 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvr2 34232 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | cvrexchlem 34233 | Lemma for cvrexch 34234. (cvexchlem 26991 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvrexch 34234 | 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 26992 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvratlem 34235 | Lemma for cvrat 34236. (atcvatlem 27008 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | cvrat 34236 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 27009 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | ltltncvr 34237 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
| ||
| Theorem | ltcvrntr 34238 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | cvrntr 34239 | The covers relation is not transitive. (cvntr 26915 analog.) (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | atcvr0eq 34240 | The covers relation is not transitive. (atcv0eq 27002 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | lnnat 34241 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | atcvrj0 34242 | Two atoms covering the zero subspace are equal. (atcv1 27003 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | cvrat2 34243 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 27010 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | atcvrneN 34244 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atcvrj1 34245 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2b 34246 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2 34247 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atleneN 34248 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atltcvr 34249 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atle 34250* | Any non-zero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
|
| ||
| Theorem | atlt 34251 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atlelt 34252 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
|
| ||
| Theorem | 2atlt 34253* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | atexchcvrN 34254 | Atom exchange property. Version of hlatexch2 34210 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atexchltN 34255 | Atom exchange property. Version of hlatexch2 34210 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvrat3 34256 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 27019 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat4 34257* | 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 27020 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | cvrat42 34258* | Commuted version of cvrat4 34257. (Contributed by NM, 28-Jan-2012.) |
|
| ||
| Theorem | 2atjm 34259 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
|
| ||
| Theorem | atbtwn 34260 |
Property of a 3rd atom on a line
intersecting element
at . (Contributed by NM,
30-Jul-2012.)
|
|
| ||
| Theorem | atbtwnexOLDN 34261* |
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 34262* |
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 34263 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 3noncolr1N 34264 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlatcon3 34265 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | hlatcon2 34266 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | 4noncolr3 34267 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
| ||
| Theorem | 4noncolr2 34268 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4noncolr1 34269 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | athgt 34270* | 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 34271* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem1 34272 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) |
| ||
| Theorem | 3dimlem2 34273 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3a 34274 | Lemma for 3dim3 34283. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3 34275 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem3OLDN 34276 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | 3dimlem4a 34277 | Lemma for 3dim3 34283. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 3dimlem4 34278 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) |
|
| ||
| Theorem | 3dimlem4OLDN 34279 | Lemma for 3dim1 34281. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | 3dim1lem5 34280* | Lemma for 3dim1 34281. (Contributed by NM, 26-Jul-2012.) |
  
| ||
| Theorem | 3dim1 34281* |
Construct a 3-dimensional volume (height-4 element) on top of a given
atom .
(Contributed by NM, 25-Jul-2012.)
|
|
| ||
| Theorem | 3dim2 34282* | Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 3dim3 34283* | Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | 2dim 34284* | Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012.) |
|
| ||
| Theorem | 1dimN 34285* | An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 1cvrco 34286 | The orthocomplement of an element covered by 1 is an atom. (Contributed by NM, 7-May-2012.) |
 | ||
| Theorem | 1cvratex 34287* | There exists an atom less than an element covered by 1. (Contributed by NM, 7-May-2012.) (Revised by Mario Carneiro, 13-Jun-2014.) |
|
| ||
| Theorem | 1cvratlt 34288 | An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012.) |
|
| ||
| Theorem | 1cvrjat 34289 | An element covered by the lattice unit, when joined with an atom not under it, equals the lattice unit. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | 1cvrat 34290 | Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | ps-1 34291 |
The join of two atoms
(specifying a projective
geometry
line) is determined uniquely by any two atoms (specifying two points)
less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda]
p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67.
(Contributed by NM, 15-Nov-2011.)
|
|
| ||
| Theorem | ps-2 34292* | Lattice analog for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in [MaedaMaeda] p. 68 and part of Theorem 16.4 in [MaedaMaeda] p. 69. (Contributed by NM, 1-Dec-2011.) |
|
| ||
| Theorem | 2atjlej 34293 | Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013.) |
|
| ||
| Theorem | hlatexch3N 34294 | Rearrange join of atoms in an equality. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | hlatexch4 34295 | Exchange 2 atoms. (Contributed by NM, 13-May-2013.) |
|
| ||
| Theorem | ps-2b 34296 | Variation of projective geometry axiom ps-2 34292. (Contributed by NM, 3-Jul-2012.) |
|
| ||
| Theorem | 3atlem1 34297 | Lemma for 3at 34304. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | 3atlem2 34298 | Lemma for 3at 34304. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | 3atlem3 34299 | Lemma for 3at 34304. (Contributed by NM, 23-Jun-2012.) |
|
| ||
| Theorem | 3atlem4 34300 | Lemma for 3at 34304. (Contributed by NM, 23-Jun-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |