HomeTheorem List (p. 353 of 383)
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. 353 of 383) | < 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-25962) |
Hilbert Space Explorer
(25963-27487) |
Users' Mathboxes
(27488-38213) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cvlexch4N 35201 | 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.) |
           
 ![./\](_.wedge.gif "./\"){kind=small}
        ![/\](wedge.gif "/\"){kind=small}   
 | ||
| Theorem | cvlatexchb1 35202 | A version of cvlexchb1 35198 for atoms. (Contributed by NM, 5-Nov-2012.) |
 
| ||
| Theorem | cvlatexchb2 35203 | A version of cvlexchb2 35199 for atoms. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch1 35204 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch2 35205 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatexch3 35206 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cvlcvr1 35207 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27401 analog.) (Contributed by NM, 5-Nov-2012.) |
   
 | ||
| Theorem | cvlcvrp 35208 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27421 analog.) (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatcvr1 35209 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlatcvr2 35210 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | cvlsupr2 35211 |
Two equivalent ways of expressing that is a superposition of
and .
(Contributed by NM, 5-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr3 35212 |
Two equivalent ways of expressing that is a superposition of
and , which can
replace the superposition part of ishlat1 35220,
 
 
, with the
simpler as
shown in ishlat3N 35222. (Contributed by NM, 5-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr4 35213 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr5 35214 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr6 35215 |
Consequence of superposition condition
.
(Contributed by NM, 9-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr7 35216 |
Consequence of superposition condition
.
(Contributed by NM, 24-Nov-2012.)
|
|
| ||
| Theorem | cvlsupr8 35217 |
Consequence of superposition condition
.
(Contributed by NM, 24-Nov-2012.)
|
|
| ||
| Syntax | chlt 35218 | Extend class notation with Hilbert lattices. |
  | ||
| Definition | df-hlat 35219* | 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 35220* |
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 35221* |
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 35222* |
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 35223* | Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlomcmcv 35224 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hloml 35225 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlclat 35226 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlcvl 35227 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hlatl 35228 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
|
| ||
| Theorem | hlol 35229 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlop 35230 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hllat 35231 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlomcmat 35232 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
|
| ||
| Theorem | hlpos 35233 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
 | ||
| Theorem | hlatjcl 35234 | Closure of join operation. Frequently-used special case of latjcl 15808 for atoms. (Contributed by NM, 15-Jun-2012.) |
| ||
| Theorem | hlatjcom 35235 | Commutatitivity of join operation. Frequently-used special case of latjcom 15816 for atoms. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | hlatjidm 35236 | Idempotence of join operation. Frequently-used special case of latjcom 15816 for atoms. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | hlatjass 35237 | Lattice join is associative. Frequently-used special case of latjass 15852 for atoms. (Contributed by NM, 27-Jul-2012.) |
|
| ||
| Theorem | hlatj12 35238 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 15854 for atoms. (Contributed by NM, 4-Jun-2012.) |
|
| ||
| Theorem | hlatj32 35239 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 15854 for atoms. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | hlatjrot 35240 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 15857 for atoms. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | hlatj4 35241 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 15858 for atoms. (Contributed by NM, 9-Aug-2012.) |
| ||
| Theorem | hlatlej1 35242 | A join's first argument is less than or equal to the join. Special case of latlej1 15817 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | hlatlej2 35243 | A join's second argument is less than or equal to the join. Special case of latlej2 15818 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
|
| ||
| Theorem | glbconN 35244* |
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 35245* |
De Morgan's law for GLB and LUB. Index-set version of glbconN 35244, where
we read as
 .
(Contributed by NM, 17-Jan-2012.)
(New usage is discouraged.)
|
| ||
| Theorem | atnlej1 35246 | 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 35247 | 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 35248* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch1 35249 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
|
| ||
| Theorem | hlexch2 35250 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
|
| ||
| Theorem | hlexchb1 35251 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
|
| ||
| Theorem | hlexchb2 35252 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
|
| ||
| Theorem | hlsupr 35253* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
| ||
| Theorem | hlsupr2 35254* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
|
| ||
| Theorem | hlhgt4 35255* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hlhgt2 35256* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
|
| ||
| Theorem | hl0lt1N 35257 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | hlexch3 35258 | A Hilbert lattice has the exchange property. (atexch 27427 analog.) (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlexch4N 35259 | 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 35260 | A version of hlexchb1 35251 for atoms. (Contributed by NM, 15-Nov-2011.) |
|
| ||
| Theorem | hlatexchb2 35261 | A version of hlexchb2 35252 for atoms. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | hlatexch1 35262 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
|
| ||
| Theorem | hlatexch2 35263 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | hlatmstcOLDN 35264* | 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 27408 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
| | ||
| Theorem | hlatle 35265* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 27417 analog.) (Contributed by NM, 4-Nov-2011.) |
| ||
| Theorem | hlateq 35266* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 27419 analog.) (Contributed by NM, 24-May-2012.) |
|
| ||
| Theorem | hlrelat1 35267* |
An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of
[MaedaMaeda] p. 30. (chpssati 27409, with swapped, analog.)
(Contributed by NM, 4-Dec-2011.)
|
|
| ||
| Theorem | hlrelat5N 35268* | 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 35269* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 27410 analog.) (Contributed by NM, 4-Feb-2012.) |
|
| ||
| Theorem | hlrelat2 35270* | A consequence of relative atomicity. (chrelat2i 27411 analog.) (Contributed by NM, 5-Feb-2012.) |
|
| ||
| Theorem | exatleN 35271 | 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 35272* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
| ||
| Theorem | atex 35273 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
 | ||
| Theorem | intnatN 35274 | 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 35275 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnneN 35276 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cvr1 35277 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27401 analog.) (Contributed by NM, 17-Nov-2011.) |
|
| ||
| Theorem | cvr2N 35278 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 27402 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | hlrelat3 35279* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 35269. (Contributed by NM, 2-May-2012.) |
|
| ||
| Theorem | cvrval3 35280* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.)
|
|
| ||
| Theorem | cvrval4N 35281* |
Binary relation expressing covers .
(Contributed by NM,
16-Jun-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cvrval5 35282* |
Binary relation expressing covers
. (Contributed by
NM, 7-Dec-2012.)
|
|
| ||
| Theorem | cvrp 35283 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27421 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | atcvr1 35284 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvr2 35285 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | cvrexchlem 35286 | Lemma for cvrexch 35287. (cvexchlem 27414 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvrexch 35287 | 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 27415 analog.) (Contributed by NM, 18-Nov-2011.) |
|
| ||
| Theorem | cvratlem 35288 | Lemma for cvrat 35289. (atcvatlem 27431 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | cvrat 35289 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 27432 analog.) (Contributed by NM, 22-Nov-2011.) |
|
| ||
| Theorem | ltltncvr 35290 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
| ||
| Theorem | ltcvrntr 35291 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | cvrntr 35292 | The covers relation is not transitive. (cvntr 27338 analog.) (Contributed by NM, 18-Jun-2012.) |
|
| ||
| Theorem | atcvr0eq 35293 | The covers relation is not transitive. (atcv0eq 27425 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | lnnat 35294 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | atcvrj0 35295 | Two atoms covering the zero subspace are equal. (atcv1 27426 analog.) (Contributed by NM, 29-Nov-2011.) |
|
| ||
| Theorem | cvrat2 35296 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 27433 analog.) (Contributed by NM, 30-Nov-2011.) |
|
| ||
| Theorem | atcvrneN 35297 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | atcvrj1 35298 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2b 35299 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| Theorem | atcvrj2 35300 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |