Home | Metamath
Proof Explorer Theorem List (p. 354 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lhpoc2N 35301 | The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
Theorem | lhpocnle 35302 | The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012.) |
Theorem | lhpocat 35303 | The orthocomplement of a co-atom is an atom. (Contributed by NM, 9-Feb-2013.) |
Theorem | lhpocnel 35304 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012.) |
Theorem | lhpocnel2 35305 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014.) |
Theorem | lhpjat1 35306 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 18-May-2012.) |
Theorem | lhpjat2 35307 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 4-Jun-2012.) |
Theorem | lhpj1 35308 | The join of a co-atom (hyperplane) and an element not under it is the lattice unit. (Contributed by NM, 7-Dec-2012.) |
Theorem | lhpmcvr 35309 | The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012.) |
Theorem | lhpmcvr2 35310* | Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013.) |
Theorem | lhpmcvr3 35311 | Specialization of lhpmcvr2 35310. TODO: Use this to simplify many uses of to become . (Contributed by NM, 6-Apr-2014.) |
Theorem | lhpmcvr4N 35312 | Specialization of lhpmcvr2 35310. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
Theorem | lhpmcvr5N 35313* | Specialization of lhpmcvr2 35310. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
Theorem | lhpmcvr6N 35314* | Specialization of lhpmcvr2 35310. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
Theorem | lhpm0atN 35315 | If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014.) (New usage is discouraged.) |
Theorem | lhpmat 35316 | An element covered by the lattice unit, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012.) |
Theorem | lhpmatb 35317 | An element covered by the lattice unit, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013.) |
Theorem | lhp2at0 35318 | Join and meet with different atoms under co-atom . (Contributed by NM, 15-Jun-2013.) |
Theorem | lhp2atnle 35319 | Inequality for 2 different atoms under co-atom . (Contributed by NM, 17-Jun-2013.) |
Theorem | lhp2atne 35320 | Inequality for joins with 2 different atoms under co-atom . (Contributed by NM, 22-Jul-2013.) |
Theorem | lhp2at0nle 35321 | Inequality for 2 different atoms (or an atom and zero) under co-atom . (Contributed by NM, 28-Jul-2013.) |
Theorem | lhp2at0ne 35322 | Inequality for joins with 2 different atoms (or an atom and zero) under co-atom . (Contributed by NM, 28-Jul-2013.) |
Theorem | lhpelim 35323 | Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 35316 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.) |
Theorem | lhpmod2i2 35324 | Modular law for hyperplanes analogous to atmod2i2 35148 for atoms. (Contributed by NM, 9-Feb-2013.) |
Theorem | lhpmod6i1 35325 | Modular law for hyperplanes analogous to complement of atmod2i1 35147 for atoms. (Contributed by NM, 1-Jun-2013.) |
Theorem | lhprelat3N 35326* | The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 34698. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
Theorem | cdlemb2 35327* | Given two atoms not under the fiducial (reference) co-atom , there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 30-May-2012.) |
Theorem | lhple 35328 | Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.) |
Theorem | lhpat 35329 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
Theorem | lhpat4N 35330 | Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
Theorem | lhpat2 35331 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.) |
Theorem | lhpat3 35332 | There is only one atom under both and co-atom . (Contributed by NM, 21-Nov-2012.) |
Theorem | 4atexlemk 35333 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemw 35334 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlempw 35335 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemp 35336 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemq 35337 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlems 35338 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemt 35339 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemutvt 35340 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlempnq 35341 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemnslpq 35342 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemkl 35343 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemkc 35344 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemwb 35345 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlempsb 35346 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemqtb 35347 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlempns 35348 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemswapqr 35349 | Lemma for 4atexlem7 35361. Swap and , so that theorems involving can be reused for . Note that must be expanded because it involves . (Contributed by NM, 25-Nov-2012.) |
Theorem | 4atexlemu 35350 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemv 35351 | Lemma for 4atexlem7 35361. (Contributed by NM, 23-Nov-2012.) |
Theorem | 4atexlemunv 35352 | Lemma for 4atexlem7 35361. (Contributed by NM, 21-Nov-2012.) |
Theorem | 4atexlemtlw 35353 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlemntlpq 35354 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlemc 35355 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlemnclw 35356 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlemex2 35357* | Lemma for 4atexlem7 35361. Show that when , satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.) |
Theorem | 4atexlemcnd 35358 | Lemma for 4atexlem7 35361. (Contributed by NM, 24-Nov-2012.) |
Theorem | 4atexlemex4 35359* | Lemma for 4atexlem7 35361. Show that when , satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.) |
Theorem | 4atexlemex6 35360* | Lemma for 4atexlem7 35361. (Contributed by NM, 25-Nov-2012.) |
Theorem | 4atexlem7 35361* | Whenever there are at least 4 atoms under (specifically, , , , and ), there are also at least 4 atoms under . This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p q/0 and hence p s/0 contains at least four atoms..." Note that by cvlsupr2 34630, our is a shorter way to express . With a longer proof, the condition could be eliminated (see 4atex 35362), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.) |
Theorem | 4atex 35362* | Whenever there are at least 4 atoms under (specifically, , , , and ), there are also at least 4 atoms under . This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p q/0 and hence p s/0 contains at least four atoms..." Note that by cvlsupr2 34630, our is a shorter way to express . (Contributed by NM, 27-May-2013.) |
Theorem | 4atex2 35363* | More general version of 4atex 35362 for a line not necessarily connected to . (Contributed by NM, 27-May-2013.) |
Theorem | 4atex2-0aOLDN 35364* | Same as 4atex2 35363 except that is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
Theorem | 4atex2-0bOLDN 35365* | Same as 4atex2 35363 except that is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
Theorem | 4atex2-0cOLDN 35366* | Same as 4atex2 35363 except that and are zero. TODO: do we need this one or 4atex2-0aOLDN 35364 or 4atex2-0bOLDN 35365? (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
Theorem | 4atex3 35367* | More general version of 4atex 35362 for a line not necessarily connected to . (Contributed by NM, 29-May-2013.) |
Theorem | lautset 35368* | The set of lattice automorphisms. (Contributed by NM, 11-May-2012.) |
Theorem | islaut 35369* | The predictate "is a lattice automorphism." (Contributed by NM, 11-May-2012.) |
Theorem | lautle 35370 | Less-than or equal property of a lattice automorphism. (Contributed by NM, 19-May-2012.) |
Theorem | laut1o 35371 | A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012.) |
Theorem | laut11 35372 | One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
Theorem | lautcl 35373 | A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012.) |
Theorem | lautcnvclN 35374 | Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012.) (New usage is discouraged.) |
Theorem | lautcnvle 35375 | Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012.) |
Theorem | lautcnv 35376 | The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013.) |
Theorem | lautlt 35377 | Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
Theorem | lautcvr 35378 | Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
Theorem | lautj 35379 | Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.) |
Theorem | lautm 35380 | Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012.) |
Theorem | lauteq 35381* | A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012.) |
Theorem | idlaut 35382 | The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012.) |
Theorem | lautco 35383 | The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.) |
Theorem | pautsetN 35384* | The set of projective automorphisms. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Theorem | ispautN 35385* | The predictate "is a projective automorphism." (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Syntax | cldil 35386 | Extend class notation with set of all lattice dilations. |
Syntax | cltrn 35387 | Extend class notation with set of all lattice translations. |
Syntax | cdilN 35388 | Extend class notation with set of all dilations. |
Syntax | ctrnN 35389 | Extend class notation with set of all translations. |
Definition | df-ldil 35390* | Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
Definition | df-ltrn 35391* | Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
Definition | df-dilN 35392* | Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.) |
Definition | df-trnN 35393* | Define set of all translations. Definition of translation in [Crawley] p. 111. (Contributed by NM, 4-Feb-2012.) |
Theorem | ldilfset 35394* | The mapping from fiducial co-atom to its set of lattice dilations. (Contributed by NM, 11-May-2012.) |
Theorem | ldilset 35395* | The set of lattice dilations for a fiducial co-atom . (Contributed by NM, 11-May-2012.) |
Theorem | isldil 35396* | The predicate "is a lattice dilation". Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
Theorem | ldillaut 35397 | A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012.) |
Theorem | ldil1o 35398 | A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013.) |
Theorem | ldilval 35399 | Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012.) |
Theorem | idldil 35400 | The identity function is a lattice dilation. (Contributed by NM, 18-May-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |