Home | Metamath
Proof Explorer Theorem List (p. 353 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 | 2polssN 35201 | A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
Theorem | 3polN 35202 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
Theorem | polcon3N 35203 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
Theorem | 2polcon4bN 35204 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
Theorem | polcon2N 35205 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
Theorem | polcon2bN 35206 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
Theorem | pclss2polN 35207 | The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
Theorem | pcl0N 35208 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
Theorem | pcl0bN 35209 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
Theorem | pmaplubN 35210 | The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012.) (New usage is discouraged.) |
Theorem | sspmaplubN 35211 | A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
Theorem | 2pmaplubN 35212 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
Theorem | paddunN 35213 | The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 6195.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
Theorem | poldmj1N 35214 | De Morgan's law for polarity of projective sum. (oldmj1 34508 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
Theorem | pmapj2N 35215 | The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
Theorem | pmapocjN 35216 | The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
Theorem | polatN 35217 | The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
Theorem | 2polatN 35218 | Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | pnonsingN 35219 | The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in [Holland95] p. 214. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
Syntax | cpscN 35220 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
Definition | df-psubclN 35221* | Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in [Holland95] p. 223. (Contributed by NM, 23-Jan-2012.) |
Theorem | psubclsetN 35222* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
Theorem | ispsubclN 35223 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
Theorem | psubcliN 35224 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
Theorem | psubcli2N 35225 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
Theorem | psubclsubN 35226 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
Theorem | psubclssatN 35227 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | pmapidclN 35228 | Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | 0psubclN 35229 | The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | 1psubclN 35230 | The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | atpsubclN 35231 | A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | pmapsubclN 35232 | A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
Theorem | ispsubcl2N 35233* | Alternate predicate for "is a closed projective subspace". Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
Theorem | psubclinN 35234 | The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | paddatclN 35235 | The projective sum of a closed subspace and an atom is a closed projective subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | pclfinclN 35236 | The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 35186 and also pclcmpatN 35187. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
Theorem | linepsubclN 35237 | A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | polsubclN 35238 | A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
Theorem | poml4N 35239 | Orthomodular law for projective lattices. Lemma 3.3(1) in [Holland95] p. 215. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
Theorem | poml5N 35240 | Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
Theorem | poml6N 35241 | Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem1N 35242 | Lemma for osumclN 35253. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem2N 35243 | Lemma for osumclN 35253. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem3N 35244 | Lemma for osumclN 35253. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem4N 35245 | Lemma for osumclN 35253. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem5N 35246 | Lemma for osumclN 35253. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem6N 35247 | Lemma for osumclN 35253. Use atom exchange hlatexch1 34681 to swap and . (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem7N 35248* | Lemma for osumclN 35253. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem8N 35249 | Lemma for osumclN 35253. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem9N 35250 | Lemma for osumclN 35253. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem10N 35251 | Lemma for osumclN 35253. Contradict osumcllem9N 35250. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | osumcllem11N 35252 | Lemma for osumclN 35253. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | osumclN 35253 | Closure of orthogonal sum. If and are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | pmapojoinN 35254 | For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 35138 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.) |
Theorem | pexmidN 35255 | Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 35239. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 35253. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
Theorem | pexmidlem1N 35256 | Lemma for pexmidN 35255. Holland's proof implicitly requires , which we prove here. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem2N 35257 | Lemma for pexmidN 35255. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem3N 35258 | Lemma for pexmidN 35255. Use atom exchange hlatexch1 34681 to swap and . (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem4N 35259* | Lemma for pexmidN 35255. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem5N 35260 | Lemma for pexmidN 35255. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem6N 35261 | Lemma for pexmidN 35255. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem7N 35262 | Lemma for pexmidN 35255. Contradict pexmidlem6N 35261. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidlem8N 35263 | Lemma for pexmidN 35255. The contradiction of pexmidlem6N 35261 and pexmidlem7N 35262 shows that there can be no atom that is not in , which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | pexmidALTN 35264 | Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 35239. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables , , , , in place of Hollands' l, m, P, Q, L respectively. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
Theorem | pl42lem1N 35265 | Lemma for pl42N 35269. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
Theorem | pl42lem2N 35266 | Lemma for pl42N 35269. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
Theorem | pl42lem3N 35267 | Lemma for pl42N 35269. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
Theorem | pl42lem4N 35268 | Lemma for pl42N 35269. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
Theorem | pl42N 35269 | Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in [MegPav2000] p. 2366). (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
Syntax | clh 35270 | Extend class notation with set of all co-atoms (lattice hyperplanes). |
Syntax | claut 35271 | Extend class notation with set of all lattice automorphisms. |
Syntax | cwpointsN 35272 | Extend class notation with W points. |
Syntax | cpautN 35273 | Extend class notation with set of all projective automorphisms. |
Definition | df-lhyp 35274* | Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.) |
Definition | df-laut 35275* | Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.) |
Definition | df-watsN 35276* | Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" . These are all atoms not in the polarity of , which is the hyperplane determined by . Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.) |
Definition | df-pautN 35277* | Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.) |
Theorem | watfvalN 35278* | The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Theorem | watvalN 35279 | Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Theorem | iswatN 35280 | The predicate "is a W atom" (corresponding to fiducial atom ). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
Theorem | lhpset 35281* | The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.) |
Theorem | islhp 35282 | The predicate "is a co-atom (lattice hyperplane)." (Contributed by NM, 11-May-2012.) |
Theorem | islhp2 35283 | The predicate "is a co-atom (lattice hyperplane)." (Contributed by NM, 18-May-2012.) |
Theorem | lhpbase 35284 | A co-atom is a member of the lattice base set (i.e. a lattice element). (Contributed by NM, 18-May-2012.) |
Theorem | lhp1cvr 35285 | The lattice unit covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.) |
Theorem | lhplt 35286 | An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
Theorem | lhp2lt 35287 | The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.) |
Theorem | lhpexlt 35288* | There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
Theorem | lhp0lt 35289 | A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
Theorem | lhpn0 35290 | A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013.) |
Theorem | lhpexle 35291* | There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013.) |
Theorem | lhpexnle 35292* | There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013.) |
Theorem | lhpexle1lem 35293* | Lemma for lhpexle1 35294 and others that eliminates restrictions on . (Contributed by NM, 24-Jul-2013.) |
Theorem | lhpexle1 35294* | There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013.) |
Theorem | lhpexle2lem 35295* | Lemma for lhpexle2 35296. (Contributed by NM, 19-Jun-2013.) |
Theorem | lhpexle2 35296* | There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013.) |
Theorem | lhpexle3lem 35297* | There exists atom under a co-atom different from any 3 other atoms. TODO: study if adant*,simp* usage can be improved. (Contributed by NM, 9-Jul-2013.) |
Theorem | lhpexle3 35298* | There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013.) |
Theorem | lhpex2leN 35299* | There exist at least two different atoms under a co-atom. This allows us to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) (New usage is discouraged.) |
Theorem | lhpoc 35300 | The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |