HomeTheorem List (p. 333 of 411)
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. 333 of 411) | < 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-26652) |
Hilbert Space Explorer
(26653-28175) |
Users' Mathboxes
(28176-41046) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lplnnlt 33201 | Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012.) |
              ![/\](wedge.gif "/\"){kind=small}     | ||
| Theorem | 2llnjaN 33202 | The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 33203 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
  
      
 
| ||
| Theorem | 2llnjN 33203 | The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnm2N 33204 | The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
![./\](_.wedge.gif "./\"){kind=small} 
| ||
| Theorem | 2llnm3N 33205 | Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
| ||
| Theorem | 2llnm4 33206 | Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
|
| ||
| Theorem | 2llnmeqat 33207 | An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013.) |
|
| ||
| Theorem | lvolset 33208* | The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012.) |
  
    
  
 | ||
| Theorem | islvol 33209* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
 | ||
| Theorem | islvol4 33210* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | lvoli 33211 | Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012.) |
| ||
| Theorem | islvol3 33212* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
| ||
| Theorem | lvoli3 33213 | Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | lvolbase 33214 | A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | islvol5 33215* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
 
| ||
| Theorem | islvol2 33216* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | lvoli2 33217 | The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.) |
|
| ||
| Theorem | lvolnle3at 33218 | A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.) |
|
| ||
| Theorem | lvolnleat 33219 | An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | lvolnlelln 33220 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | lvolnlelpln 33221 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | 3atnelvolN 33222 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2atnelvolN 33223 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lvolneatN 33224 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | lvolnelln 33225 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
| | ||
| Theorem | lvolnelpln 33226 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
| | ||
| Theorem | lvoln0N 33227 | A lattice volume is non-zero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | islvol2aN 33228 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 4atlem0a 33229 | Lemma for 4at 33249. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0ae 33230 | Lemma for 4at 33249. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0be 33231 | Lemma for 4at 33249. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem3 33232 | Lemma for 4at 33249. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
| ||
| Theorem | 4atlem3a 33233 | Lemma for 4at 33249. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem3b 33234 | Lemma for 4at 33249. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4a 33235 | Lemma for 4at 33249. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4b 33236 | Lemma for 4at 33249. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4c 33237 | Lemma for 4at 33249. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4d 33238 | Lemma for 4at 33249. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem9 33239 |
Lemma for 4at 33249. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10a 33240 |
Lemma for 4at 33249. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10b 33241 |
Lemma for 4at 33249. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10 33242 | Lemma for 4at 33249. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem11a 33243 |
Lemma for 4at 33249. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11b 33244 |
Lemma for 4at 33249. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11 33245 | Lemma for 4at 33249. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem12a 33246 |
Lemma for 4at 33249. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12b 33247 |
Lemma for 4at 33249. Substitute for (cont.). (Contributed by
NM, 11-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12 33248 | Lemma for 4at 33249. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at 33249 | Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 33113 and 3at 33126. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at2 33250 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | lplncvrlvol2 33251 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
| | ||
| Theorem | lplncvrlvol 33252 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | lvolcmp 33253 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | lvolnltN 33254 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | 2lplnja 33255 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 33256 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnj 33256 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnm2N 33257 | The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2lplnmj 33258 | The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.) |
|
| ||
| Theorem | dalemkehl 33259 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 
| ||
| Theorem | dalemkelat 33260 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemkeop 33261 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalempea 33262 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqea 33263 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemrea 33264 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsea 33265 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtea 33266 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemuea 33267 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeo 33268 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemzeo 33269 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclpjs 33270 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclqjt 33271 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclrju 33272 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalem-clpjq 33273 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemceb 33274 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempeb 33275 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqeb 33276 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemreb 33277 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemseb 33278 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemteb 33279 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemueb 33280 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjqeb 33281 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsjteb 33282 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtjueb 33283 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqrprot 33284 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeb 33285 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemcnes 33286 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempnes 33287 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqnet 33288 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjsen 33289 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemply 33290 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsly 33291 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyz 33292 |
Lemma for dath 33372. Swap the role of planes and to allow
reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalemrot 33293 |
Lemma for dath 33372. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
14-Aug-2012.)
|
|
| ||
| Theorem | dalemrotyz 33294 |
Lemma for dath 33372. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
19-Aug-2012.)
|
|
| ||
| Theorem | dalem1 33295 |
Lemma for dath 33372. Show the lines and are different.
(Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalemcea 33296 |
Lemma for dath 33372. Frequently-used utility lemma. Here we
show that
must be an
atom. This is an assumption in most presentations of
Desargue's theorem; instead, we assume only the is a lattice
element, in order to make later substitutions for easier.
(Contributed by NM, 23-Sep-2012.)
|
|
| ||
| Theorem | dalem2 33297 |
Lemma for dath 33372. Show the lines and form a plane.
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalemdea 33298 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
|
| ||
| Theorem | dalemeea 33299 | Lemma for dath 33372. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalem3 33300 | Lemma for dalemdnee 33302. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |