mmnotes.txt - Notes on Recent Proofs ------------------------------------ These are informal notes on some of the recent proofs. (8-Sep-2008) Although at first glance expimpd and expdimp seem rather specialized, they actually shorten over 80 proofs, so with them the net size of set.mm is reduced. (5-Sep-2008) At first I wasn't sure that fldivt was true (I calculated a few examples to convince myself), and I was surprised that it had a proof. It seems that it just barely works, depending critically on the slightly tighter bound on the floor of rational numbers expressed by intfracq. I don't recall seeing this in any book. It doesn't appear in the properties of floor function in Wikipedia, http://en.wikipedia.org/wiki/Floor_function#Some_properties_of_the_floor_function (not that that is any kind of authoritative list of course). (1-Sep-2008) I am phasing in "A e. Fin" in place of the current "E. x e. om { A } ~~ x" to express "A is finite". The latter idiom is now used frequently enough so that the net size of set.mm will hopefully be reduced as a result. (31-Aug-2008) I did a number of revisions to the Unicode font characters so that all symbols now display in the Opera browser as well as Firefox. (22-May-2008) Yesterday's derivation of axiom ax-4 from the others required new versions of axioms ax-5 and ax-6. The old versions were renamed ax-5o and ax-6o. Theorems ax5o and ax6o derive axioms ax-5o/ax-6o from the new ax-5/ax-6; theorems ax5 and ax6 show the reverse derivations. The organization of the axioms in set.mm has been changed. The new complete set of non-redundant axioms is now introduced in a single place in set.mm in a new section called "Predicate calculus axiomatization". (Before, they were scattered throughout, introduced as they were needed.) We immediately derive ax-4 and the old ax-5 and old ax-6 (now called ax-5o and ax-6o) as theorems ax4, ax5o, and ax6o. The next section in set.mm, "Predicate calculus without distinct variables", has the original gentle derivations from ax-4, ax-5o, and ax-6o, and eventually the equality theorems not needing ax-17. The idea here is that as long as an inexperienced reader accepts ax-4 a priori, there is no need to go through the advanced, $d-using proof of ax4. This also provides us with more meaningful "proved from axioms" lists for the section without distinct variables, without mention of the ax-17 etc. used to prove ax4. We finally introduce the "normal" use of ax-17 in the section "Predicate calculus with distinct variables" with essentially the same organization as before. The reason for proving ax4 at the beginning, and not after say the old place where ax-17 used to be, is to conform to the following convention, mentioned in the comment of ax4: Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ~ ax-4 , ~ ax-5o , ~ ax-6o , ~ ax-9o , ~ ax-10o , ~ ax-11o , ~ ax-15 , and ~ ax-16 are proved by theorems ~ ax4 , ~ ax5o , ~ ax6o , ~ ax9o , ~ ax10o , ~ ax11o , ~ ax15 , and ~ ax16 . so that the proof of theorem ax4 can't have an accidental circular reference to axiom ax-4 (which would be possible if we put the ax4 proof later in the development). The Metamath Proof Explorer Home Page has been updated with the new set of non-redundant (as far as we know) predicate calculus axioms that eliminates axiom ax-4. With ax-4 omitted from the official list of non-redundant axioms, we no longer have the former "pure" predicate calculus subsystem, that used to be ax-4/ax-5o/ax-6o, as part of the non-redundant list. Therefore it no longer makes sense to subdivide the axioms into separate groups on the MPE Home Page, and I combined them into one big table. I moved the description of the "pure" predicate calculus subsystem to the last entry of the subsystem table http://us2.metamath.org:8888/mpeuni/mmset.html#subsys ----- On another matter, the user sandboxes have been moved to the end of set.mm as suggested by O'Cat. Unfortunately, this means the software thinks they are in the "Hilbert Space Explorer" section during the web page generation. This will be a minor cosmetic inconvenience until I address this. (21-May-2008) With slightly modified ax-5 and ax-6, ax-4 becomes redundant as shown by theorem ax4. The ax-5 and ax-6 modifications have the same total length as the old ones, renamed to ax-5o and ax-6o. (17-May-2008) Axiom ax-10 was shortened. The previous version was renamed ax-10o. Theorem ax10o shows that the previous version can be derived from the new ax-10. The Metamath Proof Explorer Home Page has been updated to use the shortened axiom. (14-May-2008) I am hoping that the supremum df-spw for weak orderings will end up being easier to use in general than df-sup, because it doesn't need a separate hypothesis to show that the supremum existence condition is met. Instead, the supremum exists iff the supw value belongs to the relation's field. If this turns out to be useful, I may rethink the definition of df-sup as well. (12-May-2008) The following frequently-used labels have been changed to be slightly less cryptic and more consistent: old new 12-May-08 a4w1 a4eiv 12-May-08 a4w a4imev 12-May-08 a4c1 a4imed 12-May-08 a4c a4ime 12-May-08 a4b1 a4v 12-May-08 a4b a4imv 12-May-08 a4at a4imt 12-May-08 a4a a4im For the new labels, "a4" means related to ax-4, "im" means the implicit substitution hypothesis needs to be satisfied in only one direction, "i" means inference, "e" means existential quantifier version, "v" means distinct variables eliminate a bound-variable hypothesis, "d" means deduction, and "t" means closed theorem. (6-May-2008) The definitions of +oo and -oo (df-pnf and df-mnf) were changed so that the Axiom of Regularity is not required for their justification. Instead, we use Cantor's theorem, as shown in pnfnre, mnfnre, and pnfnemnf. A standard version of the Axiom of Infinity, ax-inf2, has been added to set.mm. It is derived from our version as theorem axinf2, using ax-inf and ax-reg. I broke out ax-inf2 as a separate axiom so that we can more easily identify "normal" uses of Regularity. Before, this was hard to do because any reference to omex would automatically include Regularity as one of the axioms used. (21-Apr-2008) Paul Chapman has replaced the real log with the more general complex log. The earlier real log theorems by Steve Rodriguez have been revised to use the new definition. Steve's original theorems can temporarily be found under the same name suffixed with "OLD", using the token "logOLD" rather than "log". (10-Mar-2008) The complex number axioms use a different naming convention than their corresponding theorems, e.g. we have axaddrcl rather than readdclt, sometimes causing confusion for people entering proofs. Therefore, I added aliases for their names using 1-step proofs, as follows: Axiom Alias axaddcl addclt axaddrcl readdclt axmulcl mulclt axmulrcl remulclt axaddcom addcomt axmulcom mulcomt axaddass addasst axmulass mulasst axdistr adddit ax0id addid1t ax1id mulid1t axlttrn lttrt axmulgt0 mulgt0t (6-Mar-2008) pm3.26, pm3.27, and pm3.28 were erroneously given with logical OR expanded into negation and implication. pm3.26OLD, pm3.27OLD, and pm3.28OLD, which will eventually be deleted, are the erroneous versions of these. This error also found its way into pmproofs.txt http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt which has also been corrected. Going through my backups, I found that this error dates back to pre-Metamath in the early 90's when I converted my manually typed list of 193 Principia Mathematica theorems into the condensed detachment notation of pmproofs.txt. Fortunately, this has no effect on the pmproofs.txt proof itself. I checked against the original typed list, and only these 3 theorems had the mistake. (11-Feb-2008) Theorems whose description begins with "Lemma for" have their math symbols suppressed in the Statement (Theorem) List in order to reduce the bulk of the list for faster web page loading. Sometimes, though, it is useful to have the lemma displayed. As an informal standard, I will change "Lemma for" to "- Lemma for" when we want the lemma displayed. The first one is fsumcllem, requested by Paul Chapman, since it will be used for multiple purposes and may make sense to someday call a "theorem". If there are lemmas you would like to have displayed, let me know. (3-Feb-2008) topbas provides a simpler definition of a basis when we know its topology in advance. It is interesting that the very complex expansion of "( B e. Bases /\ ( topGen ` B ) = J )" simplifies to "A. x e. J E. y ( y (_ B /\ x = U. y )" when J is known. Proving it was trickier than I thought it would be, although the final proof is relatively short. I updated the Description of istopg to explain why the variable name "J" is used for topologies. (16-Jan-2008) ax-12 is the longest predicate calculus axiom, and an open problem is whether it can be shortened or even proved from the others. After 15 years of on-and-off work on this problem with no success, today's a12study finally gives us a first hint, showing that it is possible to represent ax-12 with two shorter formulas. While the shortening of the starting formulas is modest, and of course their combined length is much longer than ax-12, the result is still significant: before, it wasn't clear whether ax-12 had some intrinsic property preventing it from being "broken up" into smaller pieces. It is curious that the hypotheses of a12study have similar forms. I don't know how they might be related. Note that by detaching ax-9 from the second one, they can also be written: a12study.1 $e |- ( -. A. z z = y -> ( A. z ( z = x -> z = y ) -> x = y ) ) $. a12study.2 $e |- ( -. A. z -. z = y -> ( A. z ( z = x -> -. z = y ) -> -. x = y ) $. (12-Jan-2008) cnnvg is designed to match hypotheses of the form "$e |- G = ( +v ` U )" such as in nvass. When nvass is applied to the vector space of complex numbers, cnnvba and cnnvg will change X to CC and G to + with no other manipulations, immediately producing the standard associative law for addition of complex numbers (after "U e. CVec" is detached with cnnv). This method will allow us to make efficient use of complex number theorems, such as when working with linear functionals that map to complex numbers. cnnvdemo shows how this is done. While U is substituted with "<. <. + , x. >. , abs >." in cnnvdemo, we keep the U separate in cnnv, cnnvg, and cnnvba to allow simplifying the display of proof steps (and reducing the web page size) in lemmas for long proofs, to avoid having to repeat "<. <. + , x. >. , abs >." over and over. Analogous cnnv* theorems will be added for other vector space functions. (21-Dec-2007) cofunex2g has a somewhat longer proof than might be expected because A and B are not required to be relations but may be any classes whatsoever. In particular, B may be any proper class. The recent hlxxx theorems are meant to complete the list of "(future)" theorems referenced in the comment of ax-hilex. These theorems will allow us to eliminate the Hilbert Space Explorer axioms in special cases (i.e. for concrete Hilbert spaces like CC), in order to use the Hilbert Space Explorer theorems as part of a ZFC-only theory. (17-Nov-2007) df-pm (with value theorem pmvalg) introduces the notion of partial functions. Although partial functions are ubiquitous in the theory of operators in functional analysis, there seems to be no symbol in the literature for them. The closest I've seen is an occasional "F : dom F --> B" in place of of the total function "F : A --> B", with dom F subset A implicit. But to do operator theory in set.mm, not having a formal notation for for partial functions would make the theory of operators clumsy to work with. There are two ways to do this. One way would be to define an analog of df-f: df-fp $a |- ( F : A -|-> B <-> ( Fun F /\ F (_ ( X X. Y ) ) $. or equivalently (by funssxp) df-fp $a |- ( F : A -|-> B <-> ( F : dom F --> B /\ dom F (_ A ) ) $. Here, the standard mapping arrow with a vertical bar in the middle is used by the Z language to denote a partial function, and it is the only published symbol for it I've seen, although the Z language isn't really "textbook mathematics." I like this symbol because of its similarity to the familiar "F : A --> B" of df-f, and I was very tempted to use it. The drawback is that it defines a new syntactical structure, not just a new symbol, so we would need a whole mini-development of equality theorems, bound variable hypothesis builders, etc. as we do with df-f. Such a new structure is unavoidable when the arguments could be proper classes, as in the case of many uses of df-f. But in the case of the intended uses of partial functions, the domain and range will always be sets (at least I've never seen a requirement for them in set theory where proper classes sometimes arise). This means that we can define a constant symbol for an operation similar to df-map, making all of the theorems relating to operations immediately available. With that in mind, I chose "^pm" as a generalization of "^m" of df-map. I am not thrilled with it because it doesn't seem intuitive or suggestive of its meaning, but I didn't have any better ideas. I am open to suggestions for a better symbol to use in place of "^pm", and in the meantime I'll continue to use "^pm" for lack of a better alternative. (15-Nov-2007) Baire's Category Theorem bcth was unexpectedly hard to prove. A big problem is that initially I didn't know that acdc5 (Dependent Choice) would be required to prove the existence of g. The textbook proof simply says we conclude the existence of g "by induction," which certainly stretches the meaning of that word. (2-Nov-2007) 0.999... is now proved, so the volunteer request of 30-Sep-2007 below is no longer applicable, although I appreciate the attempts of individuals such as rpenner on the physorg.com forum. The proof was more involved than I thought it would be, requiring new theorems serzmulc1, isummulc1a, and geoisum1. For the proof of 0.999... itself, quantifiers were avoided except for the implicitly quantified summation variable k. Hopefully this will make it possible for more non-mathematicians to follow the proof. (22-Oct-2007) Note that pm3.26bd, pm3.27bd were renamed pm3.26bi, pm3.27bi. (12-Oct-2007) Some of the kmlem* proofs were shortened by restating the lemmas and using yesterday's eldifsn. (30-Sep-2007) 0.999...=1 has been debated for many years on Usenet and elsewhere on the Internet. Example: http://forum.physorg.com/index.php?showtopic=13177 from March 2007 with 267(!) pages of discussion still on-going as of today. Includes a poll where 41% of people disbelieve 0.999...=1. There is even a brief reference to Metamath somewhere in the mess. Example: http://groups.google.com/group/sci.math/browse_frm/thread/3186915e0766f1ca from May 2007, whose last post was September 26. Does someone wish to volunteer to prove $( The repeating decimal 0.999... equals 1. $) 0.999... $p |- sum_k e. NN ( 9 / ( 10 ^ k ) ) = 1 $= ? $. to put an end to it once and for all? (Wishful thinking of course.) At least you'll make a name for yourself. :) Theorem geoisum may be useful for the proof. (28-Sep-2007) The symbol for floor was changed from "floor" to "|_" (L-shaped left bracket) at the suggestion of Paul Chapman. (21-Sep-2007) iccf was moved out of FL's sandbox to make it "official". It was also renamed from the earlier "icof". Compared to the old bl2iooOLD, the bl2ioo proof is shorter because it incorporates Paul Chapman's recent absdifltt. (17-Sep-2007) To help me out, perhaps a reader will volunteer to create Metamath proofs for one or more of the following. I hope I have stated them correctly. They should be fun puzzles, and in the unlikely event that two people submit the same one, the shortest proof will win. :) The tricks provided by these theorems may simplify the use of theorem cnco and relatives, because they have no dummy variables to deal with, unlike class builder representations. If no one responds, I'll prove them myself eventually when I have time. For fpar, note that each operand of i^i is not a function by itself - the intersection cuts them down so that the final set of ordered pairs is single-valued. This should make it interesting to prove. :) I think the other two are relatively straightforward, involving mainly expansions of the definitions. It may be possible to use a special case of fpar for the proof of opr2f, using fconstg, but I'm not sure it would help. In order of increasing difficulty, I would guess fsplit, opr2f, and fpar. If anyone finds a simpler expression for the left-hand side of the equality, let me know. So, paste the below at the end of your set.mm and fire up mmj2... ${ $d x y z A $. $( etc. $) $( Merge two functions in parallel. Use as the second argument of a composition with a (2-place) operation to build compound operations such as ` z = ( ( sqr ` x ) + ( abs ` y ) ) ` . $) fpar $p |- ( ( F Fn A /\ G Fn B ) -> ( ( `' 1st o. ( F o. 1st ) ) i^i ( `' 2nd o. ( G o. 2nd ) ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = <. ( F ` x ) , ( G ` y ) >. ) } ) $= ?$. $} ${ $d x y $. $( A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of ~ fpar in order to build compound functions such as ` y = ( ( sqr ` x ) + ( abs ` x ) ) ` . $) fsplit $p |- `' ( 1st |` I ) = { <. x , y >. | y = <. x , x >. } $= ?$. $} ${ $d x y A $. $( etc. $) $( Turn an operation with a constant second operand into a function of the first operand only, such as ` y = ( x + 5 ) ` . $) opr2f $p |- ( ( F Fn ( A X. B ) /\ C e. B ) -> ( F o. `' ( 1st |` ( V X. { C } ) ) ) = { <. x , y >. | ( x e. A /\ y = ( x F C ) ) } ) $= ?$. $} (13-Sep-2007) The astute reader will notice that df-ims was changed to a more compact version (compare df-imsOLD). imsval3 replaces imsvalOLD for use in reproving the related *OLD theorems, although imsval3 may be phased out with shorter direct proofs from the new imsval. A clever technique was used in Paul Chapman's reret (of 8-Sep-2007) to eliminate a hypothesis by using the if() function directly, without invoking dedth. (8-Sep-2007) hlcom is part of an eventual derivation of the Hilbert Space Explorer axioms using ZFC only. A small change in the Hilbert Space Explorer axiomatization will then allow us to convert all theorems to pure ZFC theorems, with no changes to the theorems themselves, whenever we are dealing with a fixed Hilbert space (such as complex numbers). This axiomatization change is described in the comment of ax-hilex http://us2.metamath.org:8888/mpegif/ax-hilex.html . I probably will not actually make this change in axiomatization but will only describe it. It is very simple to do for anyone interested. I still think it is useful to have the axioms separated out - it makes the Hilbert Space Explorer Home Page easier to describe and it also allows us to see what axioms are used to prove specific theorems. The Hilbert Space Explorer Home Page http://us2.metamath.org:8888/mpegif/mmhil.html was updated to mention this alternate approach (the first 3 paragraphs of "The Axioms" section). (7-Sep-2007) The new cnmet (with Met) that will replace cnms (with MetSp) also replaces the distance function "{ <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( abs ` ( x - y ) ) ) }" with "( abs o. - )", which I think is nicer. A more compact version of cnmet could read simply "( abs o. - ) e. Met", but the D is separated out to integrate more smoothly with other theorems. It also makes the proof a little easier to read. By the way the "Base" extractor (df-ba) for normed metric spaces is capitalized because, once it is fixed for a particular vector space U, it is not a function, unlike e.g. the "norm" extractor (df-nm). This is usually our convention when there is no literature standard. Another example is the set closed subsets "Clsd" (df-clsd) vs. the closure "cls" (df-cls). (4-Sep-2007) The following major changes have been made to set.mm. 1. The token Met (metric space) has been changed to MetSp. A new token called Met is defined as the class of all metrics (df-met), and a metric space (df-ms) is defined as the pair of a base set and metric. To extract the base set X from a metric D, we will usually use "dom dom D". Note that this is consistent with what we now do for topologies (df-top and df-topsp), with "U. J" for the base set of topology J. It is also consistent with groups, which are defined using only the group operation. The advantages of the new convention is that proofs will be often be shorter, and theorems will be shorter to state, e.g. OLD: msf.1 $e |- X = ( 1st ` M ) $. msf.2 $e |- D = ( 2nd ` M ) $. mscl $p |- ( ( M e. MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR ) $= NEW: metf.1 $e |- X = dom dom D $. metcl $p |- ( ( D e. Met /\ A e. X /\ B e. X ) -> ( A D B ) e. RR ) $= 2. Eventually, the theorems involving the old MetSp will be phased out and replaced with equivalent theorems involving the new Met. Note that in topology, the TopSp definition has had little real value since everything can be done more easily with Top, and the same should be true with metric spaces. 3. The definitions making use of the old MetSp have been replaced with ones using Met. The old definitions have been renamed *OLD, e.g. df-bl vs. df-blOLD. You can see the changed ones with 'show statement df-*OLD'. 4. All theorems making use of a df-*OLD will eventually have their labels suffixed with OLD, in the next few days. Some of this has already happened. They will eventually be replaced with non-OLD versions. 5. Based on a suggestion of Frederic Line (see the 16-Apr-2007 comment in http://planetx.cc.vt.edu/AsteroidMeta/set.mm_discussion_replacement ), the cryptic "( 1st ` ( 2nd ` U ) )" etc. will go away in normed vector spaces (including pre-Hilbert spaces, Banach spaces, and Hilbert spaces). Instead, we will phase in the use of the named components df-va, df-sm, df-nm and df-ba to make the theorems more readable as well as shorter to state. In addition, the theorems will become independent of the details of the ordered pairs in the vector space definition. E.g. nvge0 will be changed from ${ nvge0OLD.1 $e |- W = ( 1st ` U ) $. nvge0OLD.2 $e |- G = ( 1st ` W ) $. nvge0OLD.3 $e |- N = ( 2nd ` U ) $. nvge0OLD.4 $e |- X = ran G $. $( The norm of a normed complex vector space is nonnegative. $) nvge0OLD $p |- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) ) $=... $} to the new ${ nvge0.1 $e |- X = ( Base ` U ) $. nvge0.2 $e |- N = ( norm ` U ) $. $( The norm of a normed complex vector space is nonnegative. $) nvge0 $p |- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) ) $=... $} Again, the original versions will be renamed to *OLD. Some of them already have, and this renaming should be completed in a few days. (In the future, I may extended this use of named components to metric spaces, etc. For now I am limiting it to normed vector spaces, which in a way is a "final" application of topologies, metric spaces, groups, and non-normed vector spaces.) Over the next few days, the labels in the current set.mm will unstable, with frequent changes, starting at df-ms, and individual label changes there will not be documented in the "Recent label changes" at the top of set.mm. The labels _before_ df-ms are stable, and any changes will be documented in "Recent label changes" as usual. If you are working with set.mm, it will be safe (and preferred) to use the latest version provided you are using things above df-ms. The last version of set.mm before these changes are available in us.metamath.org/downloads/metamath.zip, for a week or so. (3-Sep-2007) Tomorrow there will be a major change in the notational conventions for metric and vector spaces. Today's version of set.mm is the last version prior to this change. If you are working from the current set.mm, you may want to archive today's version for reference, to compare against the new version if needed. (22-Aug-2007) Interestingly, hbxfr shortens 40 proofs and "pays" for itself several times over in terms of set.mm size reduction. (2-Aug-2007) I wouldn't have guessed a priori that proving addition is continuous (plcn) would be so tedious. Part of the problem might be that we have defined continuity in the very general context of topologies, but in the long run this should pay off. I didn't use the epsilon-delta method, but instead obtained a slightly shorter proof (I think) by using the already available climadd together with cnmet4. This is exactly the method used by Gleason, although his one sentence to that effect expands to a very long proof. (10-Jun-2007) The symbol "Cls" was changed to "Clsd". See the discussion at http://planetx.cc.vt.edu/AsteroidMeta/closed_and_closure (24-May-2007) axnegex and axrecex are now no longer used by any proof, and were renamed to axnegexOLD and axrecexOLD for eventual deletion. The axiom list at http://us2.metamath.org:8888/mpegif/mmcomplex.html#axioms was updated. A note on theorem names like msqgt0: a theorem name such as "msqgt0" with "msq" (m=multiplication) means "A x. A", while a name such as "sqgt0" with just "sq" means "A ^ 2". Since we are working directly with the axioms, we use A x. A rather than A ^ 2 because exponentiation is developed much later. (23-May-2007) Eric Schmidt has solved the long-standing open problem (first posted to Usenet on Apr. 25, 1997) of whether any of the ax*ex axioms for complex numbers are redundant. Here are his proofs: For axnegex: One thing to notice is that both 0re and 1re depend on axnegex for their proofs, potentially a problem if we will need to invoke these statements. However, the proof of 0re only incidentally uses axnegex, mainly because it relies on 1re. Instead, we note that the existence of any complex number implies by axcnre the existence of a real number, from which 0 in R follows from the (by now) usual inverse argument. [So (R, +) is a group.] To prove axnegex, given a complex number a + bi, we would like to find the additive inverse as (-a) + (-b)i. However, proving that this is an additive inverse requires us to know that 0i = 0, which itself depends on axnegex. We can get by with a weaker statement, namely that xi is real for some real x. For there exist x, y in R such that 0 = y + xi, or xi = -y. Having such an x, we know there exists c in R such that b + c = x. Then a + bi + ci is real, and hence has an additive inverse d. Then ci + d is an additive inverse of a + bi, which proves axnegex. We can then prove 1 in R using the current Metamath proof, in case we will need it. For axrecex: For axrecex, (a + bi) * (a - bi)/(a^2 + b^2) = 1 ought now to be provable without any hoops to jump through. The two main points are proving (a + bi) * (a - bi) = a^2 + b^2 and that a^2 + b^2 != 0 if a + bi != 0 (from which, using the now provable 0i = 0, we readily obtain a != 0 or b != 0). I formalized his axnegex proof, which was posted yesterday as negext. The axrecex proof will need a reorganization of set.mm so that some of the ordering theorems come before the reciprocal/division theorems, so it may take a couple of days to formalize. These kinds of proofs tend to be somewhat long, because we can't make use of future theorems that depend on the axioms we are trying to prove. Eventually axnegex and axrecex will be eliminated from the official set of complex number axioms at http://us2.metamath.org:8888/mpegif/mmcomplex.html, reducing the number of axioms from 27 to 25. (19-May-2007) As you can see from its "referenced by" list, 3expia ends up shortening 40 proofs, which was a suprise to me, and shrinks the size of set.mm accordingly. (18-May-2007) Paul Chapman's relatively sophisticated bcxmas was done entirely with mmj2. He writes, "using mmj2, I don't have to remember the names of theorems. What I do with steps like this is try something and see if mmj2 finds a theorem which fits. When I don't, I usually add another step (or very occasionally try a different sequence). For more complex steps I tend to search set.mm for text fragments I expect to find in theorems which I think might fit the problem, eg 'A + B ) e.'." (17-May-2007) ssimaexg and subtop were taken from FL's "sandbox" and made official, with slightly shorter proofs. The originals were renamed ssimaexbOLD, topsublem1OLD, topsublem2OLD, and topsubOLD, and will be deleted eventually. (30-Apr-2007) The definitions of +v, etc. of 26-Apr-2007 have been retired and replaced with new ones. See df-va and the statements following it. (26-Apr-2007) It seems the new symbols +v, etc., described in the 23-Apr-2007 note below, are not a good idea after all. It quadruples the proof size of ncvgcl (compared to ncvgclOLD), and in general is going to lead to longer proofs, especially for theorems brought over from more general theories (like ncvgcl is, from vcgcl). I have several other ideas I'm considering but need to think them over carefully. In the meantime, I'll probably continue to develop new theorems with the "W = ( 1st ` U )" etc. hypotheses, for retrofitting later. (23-Apr-2007) The symbols +v, .s, 0v, -v, norm, and .i were taken from the Hilbert Space Explorer for use by new definitions df-va, df-sm, df-0v, df-vs, df-nm, and df-ip. This will allow us to use the less cryptic "( +v ` U )" for vector addition in a normed complex vector space U (and Banach and Hilbert spaces), instead of the old "( 1st ` ( 1st ` U ) )". This was brought up by fl and discussed in the 16-Apr-2007 entries at http://planetx.cc.vt.edu/AsteroidMeta/set.mm_discussion_replacement . The new definitions will also provide more "generic" theorems in case we decide to change the ordered pair structure of df-ncv, etc. The new definitions df-va and df-ba serve the purpose of fl's proposed df-ahf and df-hilf in http://planetx.cc.vt.edu/AsteroidMeta/fl's_sandbox . The symbols in the Hilbert Space Explorer have been replaced with +h, .h, 0h, -h, .ih, and normh. (18-Apr-2007) The old Hilbert Space Explorer axioms ax-hvaddcl and ax-hvmulcl will be replaced by ax-hfvadd and ax-hfvmul so that the operations can be used with our group, vector space, and metric space theorems. (12-Apr-2007) Eric Schmidt discovered that the old ax1re, 1 e. RR, can be weakened to ax1cn, 1 e. CC. I updated the mmcomplex.html page accordingly. (27-Mar-2007) Maybe this is REALLY REALLY the end of shortening grothprim. At least we broke through the 200 symbol barrier. axgroth3 was used to shorten the previous grothprim. Unfortunately, that one (grothprim-8OLD) is now obsolete, so I'll probably delete axgroth3. (23-Mar-2007) grothprim was shortened a little more by exploiting the Axiom of Choice (via fodom and fodomb). As for shortening grothprim further, this may REALLY be the end of what I am capable of doing. (21-Mar-2007) Paul Chapman revised the proof of 0nn0 (compare 0nn0OLD) to use olci, which he feels is more natural than the old one's use of olc, "which seems to make a complicated wff out of a simple one." (20-Mar-2007) Unlike df-f, dff2 avoids direct or indirect references to df-id, df-rel, df-dm, df-rn, df-co, df-cnv, df-fun, and df-fn (all of which are used when df-f is expanded to primitives) but is still almost as short as df-f. I was surprised at how long and difficult the proof was, given the vast number of theorems about functions that we already have. Perhaps a shorter proof is possible that I'm not seeing. (17-Mar-2007) df-hl was changed to an equivalent one that is slightly easier to use. Compare the old one, df-hlOLD. (15-Mar-2007) dfid2 is the only theorem that makes use of the fact that x and y don't have to be distinct in df-opab. I doubt that dfid2 will be used for anything, but I thought it was interesting to demonstrate this. (12-Mar-2007) This may be it for grothprim for a while. I have stared at this thing for a long time and can't see any way to shorten it further. If anyone has any ideas let me know. (7-Mar-2007) impbid1 and impbid2 occupy 570 bytes in set.mm but reduce other proofs by 1557 bytes, with a 987 byte net size reduction of set.mm. (5-Mar-2007) In spite of its apparent simplicity, abexex is quite powerful and makes essential use of the Axiom of Replacement (and is probably equivalent to it, not sure). Chaining abexex can let us prove the existence of such things as { x | E. y E. z E. w...} that arise from non-trivial class builders (e.g. other than just the subsets of cross products) corresponding to ordered pair abstraction classes, etc. and which can be quite difficult to prove directly. (4-Mar-2007) I found shorter proofs for elnei, neips, ssnei2, innei, and neissex. The previous proofs are in elneiOLD, neipsOLD, ssnei2OLD, inneiOLD, and neissexOLD (which will be deleted in a few days). (1-Mar-2007) The contributions by Frederic Line are new versions provided by him, using the new definition df-nei (see the notes of 15-Feb-2007 below). Compare the *OLD ones starting at df-neiOLD. Most have been renamed, as well, and description for each *OLD version gives the corresponding new name. (20-Feb-2007) I have incorporated new sections at the end of the set theory part of set.mm (before the Hilbert space part), called "sandboxes," that will hold user contributions that are too specialized for the "official" set.mm or that I haven't yet reviewed for official inclusion. Here are the notes in set.mm about these sections. And, to prevent any future misunderstandings, some dire warnings. :) "Sandboxes" are user-contributed sections that are not officially part of set.mm. They are included in the set.mm file in order to ensure that they are kept synchronized with label, definition, and theorem changes in set.mm. Eventually they may be broken out as separate modules, particularly in conjunction with future Ghilbert translations. Notes: 1. I (N. Megill) have not necessarily reviewed definitions for soundness or agreement with the literature. 2. Over time I may decide to make certain definitions and theorems "official," in which case they will be moved to the appropriate section of set.mm and author acknowledgments added to their descriptions. 3. I may rename statement labels and constants at any time. 4. I may revise definitions, theorems, proofs, and statement descriptions at any time. 5. I may add or delete theorems and/or definitions at any time. 6. I may decide to delete part or all of a sandbox at any time, if I feel it will not ultimately be useful or for any other reason. If you want to preserve your original contribution, keep your own copy of it along with the version of set.mm that works with it. Do not depend on set.mm as its permanent archive. Syntax guideline: if at all possible, please use only 0-ary class constants for new definitions, to make soundness checking easier. By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of this file. Today I added sandboxes for Fred Line and Steve Rodriguez. The contents of their sandboxes appear in the Theorem List, at the end of the "Metamath Proof Explorer" part. (15-Feb-2007) The old definition of neighborhood was somewhat awkward to work in some situations. In particular, "the set of all neighborhoods of a point," which occurs when working with limit points, needed a class abstraction. So I have revised the definition of neighborhood to be a function that maps each subset to all of its neighborhoods, rather than a binary relation. This also fits more consistently with some other definitions, I think. The neighborhood theorems will be revised so that N e. ( ( nei ` J ) ` S ) is used instead of N ( nei ` J ) S to mean "N is a neighborhood of subset S". Even though this seems longer, I believe it will make certain future theorems more natural and even have shorter proofs in some cases. For example, "the set of all neighborhoods of S" just becomes ( ( nei ` J ) ` S ) instead of { x | x ( nei ` J ) S } so that working with a dummy variable becomes unnecessary. (We could also use ( ( `' ( nei ` J ) ) " { S } ) to avoid a dummy variable with the old definition, but I don't think many people would enjoy deciphering that!) The old neighborhood is called "neiOLD", with its theorems renamed to *OLD, as in df-neiOLD, etc. These will be deleted once the conversion is complete. (5-Feb-2007) df-10 was added to the database, and the comments under df-2 were revised. Since we don't have an explicit decimal representation of numbers, df-10 will allow more reasonable representations as powers of 10 than just having the digits defined. E.g. (omitting parentheses): old: 456 = 4*(9+1)^2 + 5*(9+1) + 6 new: 456 = 4*10^2 + 5*10 + 6 Previously, I avoided defining 10 since a presumed future decimal representation might have juxtaposed 1 and 0. But such a representation seems far off and low priority at this time, so an explicit definition of 10 will be helpful in the interim. A sample theorem 7p3e10 was added to "test" the new definition; additional simple theorems for the number 10 will be added shortly. (5-Feb-2007) (cont.) A new version of ax-11 was added. The original ax-11 was renamed ax-11o, and all uses of it were replaced with references to the new theorem ax11o (proved from the new ax-11). A new axiomatization was placed on the mmset.html page, and a new table was added that summarizes what is known about various possible subsystems. Theorem ax11a (mentioned yesterday and earlier) was renamed ax11. (2-Feb-2007) ax11a2 proves that ax11a can replace ax-11. I have been wondering off and on for over 10 years whether this is the case, so I am pleased to see it proved. This answers the open question of 22-Jan-2007 below: "I don't know if ax-11 can be recovered from it (that would be nice)..." This now means we can replace ax-11 with the shorter equivalent ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) which I am taking under consideration. However, it would be nicer if ax-11 could be proved from ax11a without relying on ax-16 and ax-17, so that the "predicate calculus without distinct variables" portion ax-1 through ax-15 (+ ax-mp + ax-gen) would have the same metalogical power of proof. Even if we can't prove ax-11 from ax11a without ax-16 and ax-17, the axiom set ax-1 through ax-15 would still be logically complete in the sense described at http://us2.metamath.org:8888/mpegif/mmzfcnd.html#distinctors . The deficiency would be that more theorems would have dummy variables in their distinctor antecedents, in particular the old ax-11 proved as a theorem. However, in a way this is only of cosmetic importance, since no matter how many axioms without distinct variables we have, Andreka's theorem tells us there will always be some theorems with dummy variables in their antecedents. Now, if we could just simplify the long and ugly ax-12... I have attempted that off and on also, trying to find a shorter axiom that captures its "essence" in the presence of the others, but without success. (I don't care that much about ax-15, since it is redundant in the presence of ax-17, as theorem ax15 shows.) The basic statement it makes is an atomic case of ax-17 using distinctors, just like ax-15, and that basic statement should be provable in the same way as theorem ax15 if we have the right support theorems. The problem so far is that those support theorems seem to need ax-12 in a different role. ax11a2 also shows that if we wish we can "weaken" ax11a2 by making $d x y and $d x ph if we wish, and still have completeness. Some people might prefer this as part of an alternate axiomatization that tries to reduce double binding in the axioms by having all set variables distinct. (1-Feb-2007) Interestingly, 3anidm23 will shorten 13 proofs, and adding will result in a net decrease in the size of set.mm. (31-Jan-2007) To prove that ipval has the inner product property ( C x. ( A ( ip ` U ) B ) ) = ( ( C S A ) ( ip ` U ) B ), i.e. C. = in standard notation, for all complex C (in the presence of the parallelogram law) is nonelementary: it involves an induction to show it holds for C e. NN, then we extend it to QQ, then to RR using continuity and the fact that QQ is dense in RR (qbtwnre), then to CC. I think this was proved by Jordan and von Neumann in 1935. The difficulty of the proof may be why most (all?) books define a Hilbert space as not just a special normed space but as having a "new" operation of inner product, from which a norm is derived. I had some misgivings because of the difficulty of the proof, but I think it will pay off: our definition has the nice property that CHil (_ CBan (_ CNrmVec which the standard definition doesn't. This will allow these spaces to share theorems trivially, which isn't the case with the "standard" textbook definition. (Analogous to this is our NN (_ ZZ (_ QQ (_ RR (_ CC. The standard textbook definition of CC as ordered pairs from RR doesn't have this property formally.) We will needed some additional theory about continuous functions for the proof, but that should be useful for other things as well. Anyway, it will be some time before all the inner product properties are proved. I may add pre-Hilbert spaces CPreHil, which is CNrmVec in which the parallelogram law holds. Then we would also have CHil (_ CPreHil (_ CNrmVec. However, CBan and CPreHil are not comparable as subclasses (one is complete; the other has the parallelogram law). CHil would have the trivial definition CHil = ( CBan i^i CPreHil ). (24-Jan-2007) I finally was able to prove a single theorem ax11inda that covers all cases of the quantification induction step simultaneously. It has no restrictions on z and needs no "tricks" to use it (so there no associated uncertainty that some special case hasn't been overlooked). This makes all the other versions obsolete, which have been renamed to *OLD. Part of the problem before is that I didn't even know what it should end up looking like, much less how to prove it. While the previous two evenings of effort were thus wasted, perhaps subconsciously they helped lead me towards this final solution. Although it is unnecessary now, I reproved yesterday's ax11demo (whose old proof is called ax11demoOLD) to show how simple its proof becomes with the new ax11inda. This completes, therefore, all the basis and induction steps needed to derive any wff-variable-free instance of ax-11 without relying on ax-11, thus showing that ax-11 is not logically independent of the other axioms (even though it is metalogically independent). (23-Jan-2007) I was unhappy with yesterday's ax11inda (now ax11indaOLD) because it was deceptively difficult to use for actual examples I tried, and it wasn't clear to me that it could handle all possible cases theoretically (e.g. it wasn't clear that I could derive today's ax11demo with it). The new ax11inda is simple to use, but it only works when z and y are distinct. I added the more powerful ax11inda2 that can be used otherwise. I think ax11inda2 can cover all possible cases, although I'm still working on a convincing argument for that. ax11inda2 is still not as easy to use - the variable renaming to eliminate the 2nd hypothesis can be very tricky. I added ax11demo to show how to use it. ax11inda3 is really a lemma for ax11inda, but I thought it was interesting in its own right because it has no distinct variable restrictions at all, and I made it a separate theorem for now. I might rename it to ax11indalem, though. (22-Jan-2007) The following email excerpt describes the new theorems related to ax-11. Hi Raph, > 4. How important is ax-11? > > Clearly, all theorems of PA can be proved using your axioms, but it's > quite possible that ax-11 makes the statement of certain theorems more > general in a useful way, and thus the resulting proof files would be > shorter and clearer. I'm particularly interested in the quantitative > question: how _much_ shorter? This is more a question for Norm than > for Rob, but in any case it's entirely plausible that the only real > way to answer it would be to try to prove a corpus of nontrivial > theorems both ways. I don't know if I have the answer you seek, but I'll recap what I know about ax-11: ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) http://us2.metamath.org:8888/mpegif/ax-11.html (You may already know some of this.) Before Juha proved its _metalogical_ independence, I spent some time in the other direction, trying to prove it from the others. My main result was proving, without ax-11, the "distinct variable elimination theorem" dvelimf2 (which pleased me at the time): http://us2.metamath.org:8888/mpegif/dvelimf2.html that provides a method for converting "$d x y" to the antecedent "-. A. x x = y ->" in some cases. This theorem can be used to derive, without ax-11, certain instances of ax-11. Theorem ax11el shows an example of the use of dvelimf2 for this. In the remark under ax-11, I say: Interestingly, if the wff expression substituted for ph contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. See ax11el for a simple example of how this can be done. The general case can be shown by induction on formula length. Yesterday I added the theorems needed to make this remark rigorous. For the basis, we have for atomic formulas with equality and membership predicates: http://us2.metamath.org:8888/mpegif/ax11eq.html http://us2.metamath.org:8888/mpegif/ax11el.html (These were tedious to prove. ax11el is the general case that replaces older, more restricted demo example also called ax11el, now obsolete and temporarily renamed ax11elOLD.) As a bonus, we also have the special-case basis for any wff in which x is not free: http://us2.metamath.org:8888/mpegif/ax11f.html For the induction steps, we have for negation, implication, and quantification http://us2.metamath.org:8888/mpegif/ax11indn.html http://us2.metamath.org:8888/mpegif/ax11indi.html http://us2.metamath.org:8888/mpegif/ax11inda.html respectively. I wanted the last one to be prettier (without the implied substitution and dummy variable) but wasn't successful in proving it that way; nonetheless it is hopefully apparent how it would be used for the induction. The "distinctor" antecedent of ax-11 can be eliminated if we assume x and y are distinct: ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) where $d x y http://us2.metamath.org:8888/mpegif/ax11v.html I didn't try to recover ax-11 from this, but my guess is that we can. We can also eliminate the "distinctor" antecedent like this: ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) http://us2.metamath.org:8888/mpegif/ax11a.html which has no distinct variable restriction. This is a curious theorem; I don't know if ax-11 can be recovered from it (that would be nice) or if it can be proved without relying on ax-11. Norm (20-Jan-2007) enrefg, sbthlem10, and sbth have been re-proved so that the Axiom of Replacement is no longer needed. (18-Jan-2007) The replacements for the clim* and climcvg* families are complete. In a few days, the old theorems will be made obsolete, with their replacements indicated in the following list, which will be added to the "Recent Label Changes" section of set.mm. Date Old New Notes 18-Jan-07 climcvgc1 --- obsolete; use clmi1 18-Jan-07 climcvg1 --- obsolete; use clmi2 18-Jan-07 clim1 --- obsolete; use clm2 18-Jan-07 clim1a --- obsolete; use clm3 18-Jan-07 clim2a --- obsolete; use clm2 18-Jan-07 clim2 --- obsolete; use clm4 18-Jan-07 climcvg2 --- obsolete; use clmi2 18-Jan-07 climcvg2z --- obsolete; use clmi2 18-Jan-07 climcvgc2z --- obsolete; use clmi1 18-Jan-07 climcvg2zb --- obsolete; use clmi2 18-Jan-07 clim2az --- obsolete; use clm3 18-Jan-07 clim3az --- obsolete; use clm3 18-Jan-07 clim3a --- obsolete; use clm3 18-Jan-07 clim3 --- obsolete; use clm4 18-Jan-07 clim3b --- obsolete; use clm2 18-Jan-07 climcvg3 --- obsolete; use clmi2 18-Jan-07 climcvg3z --- obsolete; use clmi2 18-Jan-07 clim4a --- obsolete; use clm3 18-Jan-07 clim4 --- obsolete; use clm4 18-Jan-07 climcvg4 --- obsolete; use clmi2 18-Jan-07 climcvgc4z --- obsolete; use clmi1 18-Jan-07 climcvg4z --- obsolete; use clmi2 18-Jan-07 clim0cvg4z --- obsolete; use clm0i 18-Jan-07 climcvgc5z --- obsolete; use clmi1 18-Jan-07 climcvg5z --- obsolete; use clmi2 18-Jan-07 clim0cvg5z --- obsolete; use clm0i 18-Jan-07 climnn0 --- obsolete; use clm4 18-Jan-07 climnn --- obsolete; use clm4 18-Jan-07 clim0nn --- obsolete; use clm0 18-Jan-07 climcvgnn --- obsolete; use clmi2 18-Jan-07 climcvgnn0 --- obsolete; use clmi2 18-Jan-07 clim0cvgnn0 --- obsolete; use clm0i 18-Jan-07 climcvg2nn0 --- obsolete; use clmi2 18-Jan-07 clim0cvg2nn0 --- obsolete; use clm0i 18-Jan-07 climnn0le --- obsolete; use clm4le 18-Jan-07 clim0nn0le --- obsolete; use clm4le and clm0 (14-Jan-2007) The purpose of resiexg is to allow us to re-prove (eventually) the Schroeder-Berstein theorem sbth without invoking the Axiom of Replacement. (11-Jan-2007) Right now there is a confusing mess of about 3 dozen theorems in the clim* and climcvg* families. It appears that these can all be replaced by around 7 theorems that cover all possible cases, and clm1 is the first in this new family. These should allow us to get rid of the old ones, which will probably happen soon. (8-Dec-2006) In the comment of 17-Nov-2006 below, I mentioned "ra4sbcgfOLD used some clever tricks to convert the hypothesis of ra4sbcfOLD to an antecedent." Since ra4sbcgfOLD will soon be deleted, I extracted the "trick" into a neat stand-alone theorem, dedhb. I shortened the proof of ra4sbcfOLD with it to show how dedhb is used. (6-Dec-2006) I put a detailed comment about the hypotheses in imsmslem because it uses them all in one place. I am making note of it here for future reference. I've been roughly trying to keep the variable names consistent. There are a few changes from one theory to the next, e.g. the group theory unit U is changed to Z (zero) in normed vector space because it seems more natural. Even though all these hypotheses are getting cumbersome to drag around, that is what happens when the implicit assumptions of analysis books are made explicit. Fortunately, many of them tend to disappear in final applications, such as imsms or ccims. While it would be theoretically nicer to allow general division rings for the scalar product of vector spaces, I think that restricting it to CC is a reasonable compromise from a practical point of view, since otherwise we'd need up to 5 additional hypotheses to specify the division ring components. In any case, most proofs would be essentially the same if we need that generality in the future, so much of the hard work would already be done. There may even be an additional advantage to doing it with CC first: the CC proofs would tell us the minimal number of ring theorems we would need for the more general development, so that we could get there more quickly. Steve Rodriguez sent in his ncvcn of 4-Dec-2006 at a fortuitous time, because it provided the special case needed for the weak deduction theorem dedth used in the imsms proof. (4-Dec-2006) vcm shows that we can equivalently define the inverse of the underlying group in a complex vector space as either the group inverse or minus 1 times a vector. This shows that the requirement of an underlying Abelian group is not necessary; it could be instead an Abelian monoid (which generalizes an Abelian group by omitting the requirement for inverse elements), although I didn't see any mention of that in the literature. In any case, for future theorems I am thinking of using mostly minus 1 times a vector in order to be compatible with the Hilbert Space Explorer, which does not postulate a negative vector as part of its axioms, since it can be derived from the scalar product in the same way as vcm does. We can use vcm to obtain the other approach. (1-Dec-2006) dvdemo1 and dvdemo2 are discussed at: http://planetx.cc.vt.edu/AsteroidMeta/U2ProofVerificationEngine (17-Nov-2006) ra4sbc eliminates the hypothesis of ra4sbcf, making the latter obsolete (and it will be deleted eventually). It will also make ra4sbcgf - renamed to ra4sbcgfOLD - obsolete, since its first antecedent is now redundant. (Kind of sad, because ra4sbcgfOLD used some clever tricks to convert the hypothesis of ra4sbcfOLD to an antecedent; looking at it again, I don't know if I could ever figure it out again. Oh well.) ra4sbc will also eliminate the distinct variable restriction x,A in ra4sbca and ra4csbela (the preveious versions of which have been renamed to ra4sbcaOLD and ra4csbelaOLD). (15-Nov-2006) The redundant Separation, Empty Set, and Pairing axioms of ZF set theory were separated out so that their uses can be identified more easily. After each one is derived, it is duplicated as a new axiom: Immediately after axsep ($p), we introduce ax-sep ($a) Immediately after axnul ($p), we introduce ax-nul ($a) Immediately after axpr ($p), we introduce ax-pr ($a) To go back to the "old way" that minimizes the number of axioms, we would just delete each $a and replace all references to it with the $p immediately above it. Thus we can easily go back and forth between two approaches, as our preference dictates: a minimal ZF axiomatization or a more traditional one that includes the redundant axioms. (9-Nov-2006) An interesting curiosity: I updated the longest path in the "2+2 trivia" section on the Metamath Proof Explorer home page, and the longest path changed dramatically. The path length increased from 132 to 137 - an occasional increase is to be expected, as over time new theorems (common subproofs) are found that shorten multiple proofs. The curious thing is that in the old path, not a single theorem of predicate calculus was in the list: it jumped over predicate calculus completely with the path: eqeq1 (set theory) <- bibi1d (prop. calc.). However, the new path has 22 theorems of predicate calculus, mostly uniqueness and substitution stuff. This was caused by the change of 12-Sep-2006 (see notes for that date below) that provided a different path for proving 0ex. Here is the old path for comparison: The maximum path length is 132. A longest path is: 2p2e4 <- 2cn <- 2re <- readdcl <- axaddrcl <- addresr <- 0idsr <- addsrpr <- enrer <- addcanpr <- ltapr <- ltaprlem <- ltexpri <- ltexprlem7 <- ltaddpr <- addclpr <- addclprlem2 <- addclprlem1 <- ltrpq <- recclpq <- recidpq <- recmulpq <- mulcompq <- dmmulpq <- mulclpq <- mulpipq <- enqer <- mulasspi <- nnmass <- omass <- odi <- om00el <- om00 <- omword1 <- omwordi <- omword <- omord2 <- omordi <- oaword1 <- oaword <- oacan <- oaord <- oaordi <- oalim <- rdglim2a <- rdglim2 <- rdglimt <- rdglim <- rdgfnon <- tfr1 <- tfrlem13 <- tfrlem12 <- tfrlem11 <- tfrlem9 <- tfrlem7 <- tfrlem5 <- tfrlem2 <- tfrlem1 <- tfis2 <- tfis2f <- tfis <- tfi <- onsst <- ordsson <- ordeleqon <- onprc <- ordon <- ordtri3or <- ordsseleq <- ordelssne <- tz7.7 <- tz7.5 <- wefrc <- epfrc <- epel <- epelc <- brab <- brabg <- opelopabg <- opabid <- opex <- prex <- zfpair <- 0inp0 <- 0nep0 <- snnz <- snid <- snidb <- snidg <- elsncg <- dfsn2 <- unidm <- uneqri <- elun <- elab2g <- elabg <- elabgf <- vtoclgf <- hbeleq <- hbel <- hbeq <- hblem <- eleq1 <- eqeq2 <- eqeq1 <- bibi1d <- bibi2d <- imbi1d <- imbi2d <- pm5.74d <- pm5.74 <- anim12d <- prth <- imp4b <- imp4a <- impexp <- imbi1i <- impbi <- bi3 <- expi <- expt <- pm3.2im <- con2d <- con2 <- nega <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <- id <- mpd <- a2i <- ax-1 (8-Nov-2006) The fact that dtru (and thus ax-16) can be proved without using ax-16 came as something of a surprise. Still open is whether ax-16 can be derived from ax-1 through ax-15 and ax-17. (Later...) Well, it turns out ax-16 can be derived from ax-1 through ax-15 and ax-17! That is a complete surprise. The "secret" lies in aev, which is a nice little theorem in itself. I've updated the mmset.html page - it's not very often that a new result is found about the axiom system. Perhaps I'll still leave in the dtruALT proof since it is an interesting exercise in predicate logic without the luxury of definitions, although I might delete it since it is not very important anymore. (4-Nov-2006) To simplify the notation - which is still quite awkward - I decided specialize vector spaces to complex fields, instead of defining vector spaces on arbitrary division rings, since that is what I expect we will use most frequently. If we need to generalize later, most proofs should be nearly the same. (3-Nov-2006) isgrp and grplidinv replace the older versions, but use the hypothesis "X = ran G" instead of "X = dom dom G". This allows us to eliminate the 5 theorems with the "X = dom dom G" hypothesis, and all theorems with that hypothesis have now been deleted from the database. (31-Oct-2006) All group theory theorems (except the first 5 leading up to grprn) were re-proved with "X = ran G" instead of "X = dom dom G" as the hypothesis. (29-Oct-2006) Steve Rodriguez provided a shorter proof (by 190 bytes in the compressed proof size and by 39377 bytes in the HTML page size) for efnn0valtlem (the lemma for his efnn0valt). (26-Oct-2006) See http://planetx.cc.vt.edu/AsteroidMeta/Translation_Systems for discussion related to isarep1 and isarep2. (25-Oct-2006) Most books (at least the ones I looked at) that define a group with only left identity/inverse elements appear to implicitly assume uniqueness when they derive the right identity/inverse elements, but you need the right identity/inverse elements to prove uniqueness. This makes our proof, which involves careful quantifier manipulations to circumvent circular reasoning, much more complicated than the ones in textbooks. I don't know of a simpler way to do it. (22-Oct-2006) I remind the reader of the entry from (17-May-2006) below called "Dirac bra-ket notation deciphered." kbass6t completes the associative law series kbass1t-kbass6t. I moved them to one place in the database for easier comparison: http://us2.metamath.org:8888/mpegif/mmtheorems80.html#kbass1t (19-Oct-2006) The mmnotes.txt entry of (4-Sep-2006) describes the general philosophy I have settled on for structures like metric spaces, which seems to be working out well: hyp.1 $e |- X = ( 1st ` M ) $. hyp.2 $e |- D = ( 2nd ` M ) $. xxx $p |- (metric space theorem involving M, X, D) $=... For topologies, the "pure" approach analogous to metric spaces would be to work with topological spaces df-topsp, which defines topological structures as ordered pairs S = <. X , J >.. We would then have e.g. (hypothetical example not in the database): 1openA.1 $e |- X = ( 1st ` S ) $. 1openA.2 $e |- J = ( 2nd ` S ) $. 1openA $p |- ( S e. TopSp -> X e. J ) $=... However, I am treating topological spaces in a different way because it is easy to recover the underlying set from the topology on it (just take the union). So theorems can be shortened as follows, still separating the topology from the underlying set in the theorem itself: 1open.1 $e |- X = U. J $. 1open $p |- ( J e. Top -> X e. J ) $=... This last is the standard I am adopting for the special case of topologies. It saves a little bit of space in set.mm. Switching to the "pure" approach in the hypothetical 1openA would be trivial if we ever wanted to do that for aesthetic consistency or whatever. I bring this up because yesterday's grpass shows that we are taking a similar approach for group theory, where the underlying set can be recovered from the domain of the group operation: X = dom dom Grp. Again, it would be trivial to convert all theorems to the "pure" approach if for some reason we wanted to do that in the future. (1-Oct-2006) Note the parsing of ac9s. The infinite Cartesian product X_ x e. A ... takes a class (B in this case) and produces another class (X_ x e. A B). Restricted quantification A. x e. A ..., on the other hand, takes a wff (B =/= (/)) and produces another wff (A. x e. A B =/= (/)). ac9s $p |- ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) ) <-------> <---------> wff class <-----------------> <-----------------> wff wff If we were to use additional parenthesis (which are unnecessary for unambiguous parsing), ac9s would read: ac9s $p |- ( A. x e. A ( B =/= (/) ) <-> ( X_ x e. A B ) =/= (/) ) So far in the database, the following definitions with "restricted" bound variables take a class and produce a class: df-iun U_ x e. A B df-iin |^|_ x e. A B df-ixp X_ x e. A B df-sum sum_ x e. A B If we wanted, we could define these surrounded by parentheses to eliminate any possible confusion. No proofs would have to be changed, only the theorem statements. However, there are already too many parentheses in a lot of theorems. Since the parenthesis-free notation for these is unambiguous, I thought it would be best in the long run. It's just a matter of getting used to it, and if in doubt one can always consult the syntax hints or use "show proof ... /all". A different example of this kind of possible confusion is sbcel1g: ( [ A / x ] B e. C <-> [_ A / x ]_ B e. C ) <----> <-----------> wff class <--------------> <----------------> wff wff which is never ambiguous because of the different brackets: [ A / x ] takes a wff as an argument, and [_ A / x ]_ takes a class as an argument. (29-Sep-2006) eluniima allows us to reduce alephfp from 72 steps to 62 steps. Compare the older version still at http://us.metamath.org/mpegif/alephfp.html . (I revisited alephfp after the discussion on http://planetx.cc.vt.edu/AsteroidMeta/metamath ). eluniima is interesting because there aren't any restrictions on A, which can be completely unrelated to the domain of F. rankxplim and rankxpsuc provide the answer to part of Exercise 14 of Kunen, which asks the reader to "compute" the rank of a cross product. (Some of the other ones can almost be "computed" - you take the previous answer and add 1 - but it is a stretch to call this proof a "computation".) This is a very difficult and rather unfriendly problem to give as a "homework exercise" - at least the answer should have been provided as a clue to work out the proof, which is already hard enough (especially since the answer has two parts, or three if we count the empty cross product). I wasted a lot of time on it, because I had to prove something that I had no clue of what it would be. I wonder how many people have actually worked this out: no one in sci.logic seemed able to answer it. http://groups.google.com/group/sci.logic/browse_frm/thread/41fad0ba18a9dce1 df-ixp is new. I'm somewhat torn about the bold X - a capital Pi is used in many books, but as the comment says I'd prefer to reserve that for products of numbers. I'm open to comments on the notation. (28-Sep-2006) I decided to restore the ancient (12-year-old) proof of pwpw0 for "historical" reasons (see discussion at http://planetx.cc.vt.edu/AsteroidMeta/metamath ). It has actually been modernized slightly, to remove the requirement that the empty set exist. This eliminates the need for the Axiom of Replacement, from which empty set existence is derived. The original can be seen at http://de2.metamath.org/metamath/set.mm . rankuni improves rankuniOLD of 17-Sep by eliminating the unnecessary hypothesis A e. V. Although this will shorten future proofs, I don't know know if such shortening will end up "paying" for the extra 16 steps of overhead needed to eliminate A e. V. But at least rankuni will be easier to use than rankuniOLD, having one less condition to satisfy. (17-Sep-2006) foprab2 is a new version (of foprab2OLD) that no longer requires the "C e. V" hypothesis. The new proof, using the 1st and 2nd functions, is very different from that of foprab2OLD and the other *oprab* theorems. (16-Sep-2006) Steve Rodriguez says about his efnn0valtlem/efnn0valt proof, "It's not short, but it took far less time than I expected, and the result seemed so obvious that I felt nagged to prove it somehow." (15-Sep-2006) opntop is an important theorem, because it connects metric spaces to our earlier work on topology, by showing that a metric space is a special case of a topology. This lets us apply the theorems we have already developed for topologies to metric spaces. (It took some work to get there; many of the theorems in the last few days where towards the goal of proving opntop.) The members of a topology J are called its "open sets" in textbooks, and this theorem provides a motivation for that term. (We do not have a separate definition for the open sets of a topology, since to say that A is an open set of topology J we just say "A e. J".) (12-Sep-2006) A number of proofs (some not shown in the Most Recent list) were modified to better separate the various uses of the Axiom of Replacement, and in particular to show where the Axiom of Extensionality is needed. The old zfaus was renamed to zfauscl, and the current zfaus is new. Some proofs in the axrep1 through axrep5 sequence were modified to remove uses of Extensionality, so that zfaus now uses only Replacement for its derivation. The empty set existence zfnul now uses only zfaus (and thus only Replacement) for its derivation. The new zfnuleu then shows how Extensionality leads to uniqueness (via the very useful bm1.1, which uses only Extensionality for its derivation). Finally, 0ex was changed (with a slightly longer proof) so that it is now derived directly from zfnuleu, to illustrate the path: ax-rep -> zfaus -> zfnul -> zfnuleu -> 0ex ^ | ax-ext Some books try to postpone or avoid the Replacement Axiom when possible, using only the weaker Separation (a.k.a. Subset, a.k.a. Aussonderung). This can now be done in our database, if we wish, by changing zfaus and zfpair from theorems to axioms. (See the new last paragraph in the ax-rep description.) (7-Sep-2006) The set.mm database was reorganized so that the ZFC axioms are introduced more or less as required, as you can see in the new Table of Contents http://us2.metamath.org:8888/mpegif/mmtheorems.html#mmtc . This lets you see what it is possible to prove by omitting certain axioms. For example, we prove almost all of elementary set theory (that covered by Venn diagrams, etc.) using only the Axiom of Extensionality, i.e. without any of the existence axioms. And quite a bit is proved without Infinity - for example, Peano's postulates, finite recursion, and the Schroeder-Bernstein theorem (all of which are proved assuming Infinity in many or most textbooks). (4-Sep-2006) I will be changing the way that the theorems about metric spaces are expressed to address some inconveniences. Consider the following two ways of expressing "the distance function of a metric space is symmetric". In the present database, we use both methods for various theorems. (These examples, though, are hypothetical, except that mssym1v1 = mssymt). (1) mssymv1.1 $e |- D e. V $. mssymv1 $p |- ( ( <. X , D >. e. Met /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) ) $= (2) mssymv2 $p |- ( ( M e. Met /\ A e. ( 1st ` M ) /\ B e. ( 1st ` M ) ) -> ( A ( 2nd ` M ) B ) = ( B ( 2nd ` M ) A ) ) $= The first way, mssymv1, shows the base set and the distance function explicitly with the helpful letters X and D. But often we want to say things about the metric space as a whole, not just its components. The second way, mssymv2, accomplishes that goal, at the expense of readability: it is less reader-friendly and more verbose to say ( 2nd ` M ) rather than just D. Although it is possible to convert from one to the other, it can be awkward, especially converting from mssymv1 to mssymv2. So practically speaking, we will end up creating two versions of the same theorem, neither of which is ideal. A solution to this is provided by the following third version: (3) mssymv3.1 $e |- X = ( 1st ` M ) $. mssymv3.2 $e |- D = ( 2nd ` M ) $. mssymv3 $p |- ( ( M e. Met /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) ) $= The conclusion is simpler than either of the first two versions and clearly indicates the intended meaning of an object with letters M, X, and D. Although the hypotheses are more complex, in the database they will typically be resused by several theorems. To obtain mssymv1 from mssymv3 is trivial: we replace M with <. X , D >., then we use op1st and op2nd to eliminate the hypotheses. To obtain mssymv2 from mssymv3 is trivial: we use eqid to eliminate the hypotheses. So, with this approach, we should never need to prove mssymv1 and mssymv2 separately, since the conversion to either one in a proof is immediate. My plan is to convert everything to this approach and make most of the existing theorems obsolete. msf is the first one using this approach, and it will replace the existing msft. As always, comments are welcome. (3-Sep-2006) Although ax16b is utterly trivial, its purpose is simply to support the statement made in the 7th paragraph of http://us2.metamath.org:8888/mpegif/mmzfcnd.html (29-Aug-2006) The value of the ball function is a two-place function, i.e. it takes in two arguments, a point and a radius, and returns a set of points. I define it as an "operation" in order to make use of the large collection of operation theorems, and also to avoid introducing a new syntactical form. However, we have two choices for expressing "The value of a ball of radius R around a point P". Note that M is a metric space, X is the underlying space of a metric space, and D is a distance function. Operation value notation: ( P ( ball ` M ) R ) ( P ( ball ` <. X , D >. ) R ) when M = <. X , D >. Function value notation: ( ( ball ` M ) ` <. P , R >. ) ( ( ball ` <. X , D >. ) ` <. P , R >. ) when M = <. X , D >. The former is shorter and will result in shorter proofs in general, but I'm not sure that using infix notation like we would for an operation like "+" is the most natural or familiar. There is no standard notation in the literature, which uses English and also does not make the metric space explicit. I am open to comments or suggestions. Since ( ball ` <. X , D >. ) acts like an operation value, we also have a third choice and could say, equivalently, ( P ( X ball D ) R ) when M = <. X , D >. for an even shorter notation, although I'm not sure how odd it looks. But maybe I should use it for efficiency. Note that I am using <. X , D >. e. Met instead of X Met D (via df-br), even though the latter results in shorter proofs (and is shorter to state). It seems that Met feels more like a collection of structures that happen to be ordered pairs of objects, than it does a relation, even though those concepts are technically identical. (28-Aug-2006) Two of the standard axioms for a metric space, that the distance function is nonnegative and that the distance function is reflexive, are redundant, so they have been taken out of the definition df-ms to simplify it. (We will prove the redundant axioms later as theorems.) The first part of the ismsg proof (through step 18) is used to get rid of the antecedent X e. V that occurs in step 43. (If either side of the ismsg biconditional is true, it will imply X e. V, making it redundant as an antecendent.) (26-Aug-2006) Some small items related to yesterday's unctb (with a new version today) were cleaned up: 1. The unused hypothesis B e. V was removed from unictb. 2. unpr was renamed to unipr for naming consistency. 3. The hypotheses A e. V and B e. V eliminated from unctb, with the help of the new theorem uniprg. (22-Aug-2006) csbopeq1a will help make the '1st' and '2nd' function stuff worthwhile; it lets us avoid the existential quantifiers that are used in e.g. copsexg. It is often easier to work with direct computations rather than having to mess around with quantifiers. I was surprised that there are no distinct variable, class existence, or any other restrictions on csbopeq1a. There is no restriction on what B may contain, which could be any random usage of x and y, not just ordered pairs of them; but what we are doing is the logical equivalent of substitution for ordered pairs in B as if it actually contained them. (21-Aug-2006) I made some subtle changes to the little colored numbers. Although this may seem like a trivial topic, and probably is, the problems of obtaining a spectrum of colors with uniform brightness and maximum distinguishability vs. hue changes aren't as easy as they might first appear. Perhaps someone has done it before, but all of the spectrum mappings I could find have brightness that varies with color and aren't suitable for fonts, in particular because yellow is hard to read. They also do not change color (as perceived by the eye) at a uniform rate as you go through the spectrum, such as the color changes crowded into the transition from red to green. This is OK if you want an accurate representation of color vs. wavelength, but our goal is to be able to distinguish different colors visually in an optimal way. Anyway I thought it was an interesting problem, so I thought I'd say something about it. Even though it pales in importance compared to today's announcement of the evidence that dark matter exists. :) The new "rainbow" color scheme now has the following properties: 1. All colors now have 50% grayscale levels. Specifically, all colors now have an L (level) value of 53 in the L*a*b color model (see http://en.wikipedia.org/wiki/Lab_color). This means if you convert a screenshot to grayscale, the colored numbers will all have the same shade of gray. Yellow becomes brown at L=53, with an RGB value of 131-131-0. 2. Within the constraint of the 50% grayscale level, each color has maximum saturation. This is not as simple as it seems: the RGB color for the brightest pure blue, 0-0-255, only has a L value of 30 (because the eye is not as sensitive to blue), so we have to use the 57% saturated 110-110-255 to get L=53. Green, on the other hand, just requires 0-148-0 for L=53, which is 100% saturated. 3. The hues are not equally spaced numerically, but according to how the eye is able to distinguish them. I determined this empirically by comparing the distinguishability of adjacent hues on an LCD monitor, using a program I wrote for that purpose. For example, the eye can distinguish more hues between red and green than between green and blue. This was a problem with the old colors, which seemed to have too many undistinguishable blue-greens. Now, as experimentally determined, the transition from green to blue represents only 21% of the color values. You can see the new color spectrum at the top of a theorem list page such as http://us2.metamath.org:8888/mpegif/mmtheorems.html. The spectrum position to RGB conversion is done by the function spectrumToRGB in mmwtex.c of Metamath version 0.07.21 (20-Aug-2006). (16-Aug-2006) abfii5 is the last in the series, and just chains together the others to obtain the final connection between verion used by subbas and the version of the left-hand side that does not involve equinumerosity. This can allow us to express subbas in more elementary terms, if we wish. (14-Aug-2006) abfii4 is an interesting brainteaser: we show the that |^| { x | ( A (_ x /\ A. y ( ( y (_ x /\ -. y = (/) /\ E. z e. om y ~~ z ) -> |^| y e. x ) ) } is equal to |^| { x | ( A (_ x /\ A. y ( ( y (_ A /\ -. y = (/) /\ E. z e. om y ~~ z ) -> |^| y e. x ) ) } The second differs from the first by only one symbol: the "x" is changed to "A". At first, it superficially looked like this would be an elementary theorem involving set intersection. But the proof turned out quite difficult, not only the proof itself but the fact that it needs some subtheorems that are somewhat difficult or nonintuitive in themselves (fiint, intab via abfii2, abfii3, abexssex [based on the Axiom of Replacement], intmin3), involving the theories of ordinals, equinumerosity, and finite sets. abfii2 and abfii3 are each used twice, for different purposes, in different parts of the proof. I found this quite a challenge to prove and would be most interested if anyone sees a more direct way of proving this. (Note that "E. z e. om y ~~ z" just means "y is finite". A simpler way of stating this is "y ~< om", but that requires the Axiom of Infinity, which I wanted - and was able - to avoid for this proof.) abfii4 arose while looking at equivalent ways to express the collection of finite intersections of a set, which determines a basis for a topology (see theorem subbas). Textbooks never seem to mention the exact formal ways of saying this, but just say, informally, "the collection of finite intersections." (11-Aug-2006) With today's 3bitr4rd, we now have the complete set of all 8 possibilities for each of the 3-chained-biconditional/equality series 3bitr*, 3bitr*d, 3eqtr*, and 3eqtr*d. (9-Aug-2006) If you are wondering why it is "topGen" and not "TopGen", a standard I've been loosely following is to use lowercase for the first letter of classes that are ordinarily used as functions, such as sin, cos, rank, etc. Of course you will see many exceptions, mainly because I try to match the literature when the literature gives something a name. (7-Aug-2006) intab is one of the oddest "elementary" set theory theorems I've seen. It took a while to convince myself it was true before I started to work out the proof, and the proof ended up rather long and difficult for this kind of theorem. Yet the only set theory axiom used is Extensionality. Perhaps I just have a mental block - if anyone sees a simpler proof let me know. I haven't seen this theorem in a book; it arose as part of something else I'm working on. Two new definitions were added to Hilbert space, df-0op and df-iop. The expressions ( H~ X. 0H ) and ( I |` H~ ), which are equivalent to them, have been used frequently enough to justify these definitions. (4-Aug-2006) 3eqtrr, 3eqtr2, 3eqtr2r complete the 8 possibilities for 3 chained equalities, supplementing the existing 3eqtr, 3eqtr3, 3eqtr3r, 3eqtr4, 3eqtr4r. I was disappointed that the 3 new ones reduce the size of only 33 (compressed) proofs, taking away a total of 185 characters from them, whereas the new theorems by themselves increase the database size by 602 characters. So, the database will grow by a net 417 characters, and the new ones don't "pay" for themselves. Nonetheless, O'Cat convinced me that they should be added anyway for completeness. He wrote: I would vote for adding them even though the net change is PLUS 400 some bytes. It just makes unification via utilities like mmj2 much easier -- input the formula and let the program find a matching assertion. Esp. now that you've done the work to analyze them, it is illogical not to make the change: eventually enough theorems will be added to save the added bytes. And within 10 years when we have bigger, faster memories people would think it quaint to be so stingy with theorems that serve a valid purpose. We're going to have PC's with a minimum of 1GB RAM next year as standard, and that will just grow as the new nanotech advances. So, I guess I should also complete the 3eqtr*d, 3bitr*, and 3bitr*d families at some point. (2-Aug-2006) fiint replaces fiintOLD. (24-Jul-2006) Note that the description of today's sucxpdom says it has "a proof using AC", and you can see in the list of axioms below the proof that ax-ac was used. Exercise: How does ax-ac end up getting used? Metamath has no direct command to show you this, but it is usually easy to find by examining the outputs of the following two commands: 1. show trace_back sucxpdom ... numth2 fodom fodomg fnrndomg ccrd($a) df-card($a) cardval cardon cardid cardne carden carddomi carddom cardsdom domtri entri entri2 sucdom unxpdomlem unxpdom ^^^^^^^ 2. show usage ax-ac / recursive ...imadomg fnrndomg unidom unidomg uniimadom uniimadomf iundom cardval cardon cardid oncard cardne carden cardeq0 cardsn carddomi carddom cardsdom domtri entri entri2 entri3 sucdom unxpdomlem unxpdom unxpdom2 sucxpdom... ^^^^^^^ The theorem we want is the last theorem in the first list that appears in the second list. In this case, it is unxpdom. And, indeed, we see that unxpdom appears in proof step 43 of sucxpdom, and we can check that unxpdom uses ax-ac for its proof. Of course, there may be other theorems used by the sucxpdom proof that require ax-ac, and the only way to determine that is to see if any of the other theorems used in the sucxpdom proof appear in the second list. But for a quick indication of what ax-ac is needed for, the method above can be useful. (21-Jul-2006) oev2, etc. are part of Mr. O'Cat's cleanup project for some of the remaining *OLDs. (20-Jul-2006) istps5 is important because it reassures us that our definitions of Top and TopSp match exactly the standard textbook version, even though the latter is more complex when the words are converted to symbols. I don't think istps5 will have an actual practical use, though, because of the simpler theorems we have available. (18-Jul-2006) It is awkward to eliminate the "J e. V" hypothesis from istop and isbasis/isbasis2 when it is redundant (as in most uses) - it requires working with a dummy variable then elevating it to a class variable with vtoclga - so I'm replacing these with "g" versions that have "J e. V" as an antecedent (actually "J e. A" as customary, to allow easy use of ibi when we need only the forward implication). I think the non-g versions will be used so rarely that it's not worth keeping them, so they will be deleted, and it is trivial to use instead the "g" version + ax-mp. [Update: istop, isbasis, and isbasis2 have now been deleted.] I also modified Stefan's 0opn, uniopn to use an antecedent instead of hypothesis. (17-Jul-2006) It is interesting that Munkres' definition of "a basis for a topology" can be shortened considerably. Compare http://us2.metamath.org:8888/mpegif/isbasis3g.html (Munkres' version) with http://us2.metamath.org:8888/mpegif/isbasisg.html (abbreviated version). Munkres' English-language definition is (p. 78): "Definition. If X is a set, a _basis_ for a topology on X is a collection _B_ of subsets of X (called _basis elements_) such that (1) For each x e. X there is at least one basis element B containing x. (2) If x belongs to the intersection of two basis elements B1 and B2, then there is a basis element B3 containing x such that B3 (_ B1 i^i B2." ------- The symbols and statement labels for topology were changed in order to conform more closely to the terminology in Munkres, who calls a member of our (old) Open a "topology" and calls a member of our (old) Top a "topological space". Old symbol New symbol ---------- ---------- Top TopSp Open Top Old label New label --------- --------- ctop ctps cope ctop df-top df-topsp df-open df-top dfopen2 dftop2 optop eltopsp elopen1 istop elopen2 uniopnt op-empty 0opnt empty-op sn0top op-indis indistop ------- If J is a topology on a set X, then X is equal to the union of J. For this reason, the first member of a topological space is redundant. I am doubtful that the topological space definition will offer any real benefit and am considering deleting it. If anyone knows of a good reason to keep it, let me know. (12-Jul-2006) I added definitions for topology (df-open and df-top), and added some theorems that Stefan Allan proved back in Feb. and March. Note that "e. Open" and "e. Top" are equivalent ways of saying something is a topology, which will be shown by the (in progress) theorem "( <. U. A , A >. e. Top <-> A e. Open )", and "e. Open" is often simpler. (7-Jul-2006) Over 100 *OLD's were removed from the database, and 83 remain, 27 of which are in the Hilbert space section. After subtracting the *OLD's, there are 6053 theorems in the non-Hilbert-space part and 1181 for Hilbert space, a total of 7243. This is the first time I have become aware that the Metamath Proof Explorer has officially passed the 6000 theorem "milestone", which happened 53 (green) theorems ago. The 6000th theorem was mt4d, added on 18-Jun-2006. (6-Jul-2006) With the updated projlem31, all uses of ~~>OLD have been eliminated. Soon I will remove the corresponding *OLD theorems from the database. (5-Jul-2006) With ege2le3, we have finally completed the non-Hilbert-space conversion of ~~>OLD based theorems, so that no theorem in the non-Hilbert-space section depends on ~~>OLD anymore. We can't delete their *OLD theorems yet, because ~~>OLD is still used in a few places in the Hilbert space section, but that should happen soon. (If you type "show usage cliOLD/recursive" you will see, before the Hilbert space section, the *OLDs that will be deleted. I will delete them when the Hilbert space stuff is finished being converted to ~~>.) By the way, we can also now delete all uses of sum1oo ("show usage csuOLD /recursive"), which I will do soon. (4-Jul-2006) Currently there are separate derivations of 2 <_ e, e <_ 3, and 2 <_ e /\ e <_ 3. Eventually, I'll probably delete the first two, but for now my immediate goal is to replace the *OLDs. (1-Jul-2006) The proof of class2seteq was shortened. Compare the previous version, class2seteqOLD. (30-Jun-2006) Continuing with the *OLD cleanup project, the future ereALT (to replace the existing ereALTOLD) will be an alternate derivation of ere. The proof of ereALTOLD specifically focuses on the number e and has a much simpler overall derivation than ere, which is a special case of the general exponential function derivation. The lemmas for ereALTOLD are mostly reused to derive the bounds on e (ege2OLD, ele3OLD, ege2le3OLD). Since ereALTOLD ends up being a natural byproduct of those theorems, I have so far kept it even though it is redundant, in order to illustrate a simpler alternate way to prove e is real. By the way, if you are wondering how the mmrecent page can "predict" a future theorem, the web page generation program simply puts "(future)" after the comment markup for any label not found in the database (and also issues a warning to the user running the program). The mmrecent page is refreshed with the "write recent" command in the metamath program. (21-Jun-2006) The conversion of cvgcmp3ce to cvgcmp3cet is one of our most complex uses to date of the Weak Deduction Theorem, involving techniques that convert quantified hypotheses to antecedents. The conversion is performed in stages with 2 lemmas. (Eventually I want to look at proving the theorem form directly, with the hope of reducing the overall proof size. But for now my main goal is to replace the *OLDs.) (20-Jun-2006) As mentioned below, most of the recent convergence stuff like cvgcmp3ce is slowly replacing the *OLDs. My goal is to be able to delete a big batch of *OLDs, used to develop the exponential funtion df-ef, within 2 weeks. We can't get rid of them until the last piece in the chain of proofs is completed. (6-Jun-2006) caucvg will replace caucvgOLD as part of the *OLD elimination project. BTW Prof. Wachsmuth doesn't know where this proof is from; he may have originated it: "I wrote many of the proofs years ago and I don't remember a good reference for this particular one" (email, 6-Jun). It is a nice proof to formalize because it is more elementary than most, in particular avoiding lim sups. (We have df-limsup defined, but it needs to be developed. As you can see, df-limsup is not so trivial. One of its advantages is that it is defined - i.e. is an extended real - for all sequences, no matter how ill-behaved.) (5-Jun-2006) kbass2t is the 2nd bra-ket associative law mentioned in the notes of 17-May-2006. (4-Jun-2006) The description of ax-un was made clearer based on a suggestion from Mel O'Cat. (2-Jun-2006) unierr is our first theorem related to qubits and quantum computing. In a quantum computer, an algorithm is implemented by applying a sequence of unitary operations to the computer's qubit register. A finite number of gates selected from a fixed, finite set cannot implement an arbitrary unitary operation exactly, since the set of unitary operations is continuous. However, there is a small set of quantum gates (unitary operations) that is "universal," analogous to the universal set AND and NOT for classical computers, in the sense that any unitary operation may be approximated to arbitrary accuracy by a quantum circuit involving only those gates. Theorem unierr tells us, importantly, that the worst-case errors involved with such approximations are only additive. This means that small errors won't "blow up" and destroy the result in the way that, say, a tiny perturbation can cause completely unpredictable behavior in weather prediction (the "butterfly effect"). (1-Jun-2006) Someone complained about not being able to understand infpn (now called infpn2), so I decided to make the "official" infpn use only elementary notation. (27-May-2006) The label of the ubiquitous 'exp' (export) was changed to 'ex' to prevent it from matching the math token 'exp' (exponential function), in anticipation of the 24-Jun Metamath language spec change. Normally I don't mention label changes here - they're documented at the top of set.mm - but ex, used 724 times, is the 5th most frequently used theorem, so this change will almost certainly impact any project using set.mm as a base. Although ex is of course not new, I re-dated it to show up in today's "Most Recent Proofs." (25-May-2006) I think csbnest1g is interesting because the first substitution is able to "break through" into the inside of the second one in spite of the "clashing x's". Compare csbnestg, where x and y must be distinct. I found it a little tricky to prove, and I wasn't even sure if it was true at first. (18-May-2006) kbasst proves one of the associative laws mentioned yesterday: Dirac: ( |A> = |A> ( ) Metamath: ( ( A ketbra B ) ` C ) = ( ( ( bra ` B ) ` C ) .s A ) (17-May-2006) Dirac bra-ket notation deciphered Most quantum physics textbooks give a rather unsatisfactory, if not misleading, description of the Dirac bra-ket notation. Many books will just say that is defined as the inner product of A and B, or even say that it _is_ the inner product, then go off and give mechanical rules for formally manipulating its "components" . For physicists, "formally" means "mechanically but without rigorous justification." If the dimensions are finite, there is no problem. A finite-dimensional Hilbert space is essentially linear algebra, and it is possible to prove that any vector and linear operator can be represented by an n-tuple (column vector) and matrix respectively. In finite dimensions, we just define |A> to be a column vector and (the inner product) and |A> is a member of Hilbert space (a vector) and call equals the inner product of A and B. While this solves some of the problems, mysteries remain, such as, what is the "outer product" |A> = |A> ( ) ( ) to be defined as ( B .i A ). So now we have the "best of both worlds" and can choose either (which physicists consider synonymous with inner product) or (A .i B) = , to match whatever text we're working with. There are actually 4 kinds of objects that result from different bra and ket juxtapositions: complex numbers, vectors, functionals, and operators. This is why juxtaposition is not "exactly" a product, because its meaning depends on the kind of objects that the things being juxtaposed represent. The starting operations on vectors are as follows: Finite dim. Operation Notation Metamath Value analogy ket |A> A vector column vector bra ( B .i A ) complex number complex number outer product |A> can also be expressed as ( ( bra ` A ) ` B ) - as today's theorem bravalvalt shows - and this will be needed to use the table below (in line 5). (Lines 3 and 4 in the above table are redundant, since they are special cases of lines 5 and 4 below; line 4 above is computed ( A ketbra ( `' bra ` ( bra ` B ) ) ) = ( A ketbra B ).) We will represent the four kinds of possible results in the "Value" column above as v, f, c, and o respectively. After accounting for the restrictions on juxtaposing bras and kets (e.g., we can never have an inner product followed by a ket), exactly the following cases can occur when two Dirac subexpressions T and U are juxtaposed to produce a new Dirac expression TU: T U TU Metamath operation Description c c c ( T x. U ) Complex number multiplication c f f ( T .fn U ) Scalar product with a functional v c v ( U .s T ) Scalar product (note T & U swap) v f* o ( T ketbra ( `' bra ` U ) ) Outer product (with converse bra) f v c ( T ` U ) Inner product (bra value) f o f ( T o. U ) Functional composed with operator o v v ( T ` U ) Value of an operator o o o ( T o. U ) Composition of two operators *Note: In line 4, U must be a continuous linear functional (which will happen automatically if U results from a string of kets and bras). This is needed by the Riesz theorem riesz2t, which allows the inverse bra to work. The other lines have no restriction. See df-hfmul for ".fn", df-co for "o.", and df-cnv for "`'". Line 5 can be stated equivalently: f* v c ( U .i ( `' bra ` T ) ) Inner product (with converse bra) So, the "operation" of juxtaposition of two Dirac subexpressions can actually be any one of 8 different operations! This is why we can't easily express the Dirac notation directly in Metamath, since a class symbol for an operation is supposed to represent only one object. Supplementary note: Physics textbooks will often have equations with an operator sandwiched between a bra and a ket. Its juxtaposition with a bra or ket also now becomes easy to formalize: match an entry from the table above where the operator corresponds to an "o" input. As an example of the use of the above table, consider the associative laws above and their set-theoretical (Metamath) translations, which we will eventually prove as theorems in the database. Dirac: ( |A> = |A> ( ) Metamath: ( ( A ketbra B ) ` C ) = ( ( ( bra ` B ) ` C ) .s A ) Dirac: ( ) . <. B | ) ( | C >. <. D | ) = | A >. ( <. B | ( | C >. <. D | ) ) Metamath: ( ( A ketbra B ) o. ( C ketbra D ) ) = ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) ) There you have it, a complete formalization of Dirac notation in infinite dimensional Hilbert space! I've never seen this published before. For an intuitive feel for the table above, it can be useful to compare the finite dimensional case using vectors and matrices. Suppose A and B are column vectors of complex numbers [a_1] [b_1] [a_2] [b_2] Then |B> is the same as B, and becomes the inner product a_1* x. b_1 + a_2* x. b_2, and |B> y = x and A. x A. y ph <-> A. y A. x ph. To accomodate this, we could have a notation representing the opposite of a $d that says two variables are not necessarily distinct. Alternately, we could adopt the approach of restating the axiom system so that set variables are always distinct, as described on http://planetx.cc.vt.edu/AsteroidMeta//mmj2Feedback (search for "Here is an idea"). However, in set theory and beyond, situations where set variables are not required to be distinct are not very common. (10-May-06) A reader comments at http://www.jaredwoodard.com/blog/?p=5 that he wishes I'd spend less time on Hilbert space and more on cleaning up *OLDs. The cleaning up of *OLDs has actually been happening "behind the scenes" even though people may not notice it. Almost 200 *OLDs have been eliminated since January (there were 380 then; now there are 185). Yesterday's geoser and expcnv will eliminate their corresponding *OLDs, for example. Mel O'Cat is also working on a list of 27 of the *OLDs. I realize hardly anyone cares about the Hilbert space stuff, and regular visitors are probably bored to tears seeing the dreary purple theorems day after day. :) (I do try not to go too long without a pretty green one now and then.) My long term goal is to build a foundation that will let me explore rigorously some new ideas I have for Hilbert lattice equations that may lead to writing a new paper. I also want to build up a foundation for theorems related to quantum computing. In a few days hopefully we will have a theorem related to error growth in qubits (quantum gates). (9-May-06) Compare geoser to the old one, geoserOLD, that it replaces. Wikipedia entry: http://en.wikipedia.org/wiki/Geometric_series (5-May-06) The Riesz representation theorem is used to justify the existence and uniqueness of the adjoint of an operator. In particular, the rigorous justification of Dirac bra-ket notation in quantum mechanics is dependent on this theorem. See also Wikipedia: http://en.wikipedia.org/wiki/Riesz_representation_theorem (13-Apr-06) One thing to watch out for in the literature is how the author defines "operator". I put some notes at http://us2.metamath.org:8888/mpegif/df-lnop.html on the various definitions: for some they are arbitrary mappings from H to H, for others they are linear, for still others they are linear and bounded. In set.mm, "operator" means an arbitrary mapping. Today's goal is: a linear operator is continuous iff it is bounded. This will be called "lncnbd" when it is completed later today. lnopcon provides the basic proof of this: it is not a trivial proof, 220 steps long, and to me it is non-intuitive. Many authors forget about the case of the trivial Hilbert space, where sometimes a result holds and other times not. lnopcon does hold, but we have to prove the trivial case separately, and in step 219 we combine the nontrivial case of step 194 with trivial case of step 218. (12-Apr-06) The astute observer may have noticed that the dates on the "Recent Additions to the Metamath Proof Explorer" now have 4-digit years, e.g. 12-Apr-2006 instead of 12-Apr-06. Version 0.07.15 of the metamath program implements 4-digit date stamps, and set.mm has been updated with 4-digit years. The program still recognizes 2-digit years (for the 'write recent' command) but assumes they fall between 1993 and 2092. (10-Apr-06) The reason the xrub proof is long is that it involves 9 cases: 3 cases for B (real, -oo, and +oo), and for each B, 3 cases for x. (We handle some of them simultaneously in the proof.) This theorem means we only have to "scan" over the reals, rather than all of the extended reals, in order to assert that B is an upper bound for set A. This is true even if A contains non-reals or if B is non-real (+oo or -oo). When we quantify over all extended reals, often we have to consider the 3 cases of real, -oo, +oo separately. The advantage of this theorem is that we don't have to handle the last two cases anymore, so some proofs will become significantly shorter as a result. (6-Apr-06) The proof of unictb is very different from Enderton's, which I found somewhat awkward to formalize. Instead, it is effectively a special case of Takeuti/Zaring's much more general uniimadom. It is also interesting how simple it is to go from the indexed union to the regular union version of a theorem, whereas it can be rather difficult in the other direction. For example, iunctb to unictb is trivial through the use of uniiun. But for the finite version of this theorem, compare the difficulty of going from the regular union version, unifi to iunfi, requiring the not-so-trivial fodomfi, which was proved for this purpose. The conversion of unifi to iunfi involved substituting z for x and { y | E. x e. A y = B } for A in unifi, using dfiun2 on the consequent, and doing stuff to get the antecedents right. The "doing stuff" ends up being not so simple. Perhaps if I had to do it over, it might have been simpler to prove iunfi first, then trivially obtain unifi via uniiun, although I'm not really sure. Both iunctb and iunfi are intended ultimately to be used by a Metamath development of topology, which Stefan Allan has started to look at. (1-Apr-06) Today's avril1 http://us2.metamath.org:8888/mpegif/avril1.html is a repeat of last year's, except for a small change in the description. But I bring it up again in order to reply to last year's skeptics. Unlike what some people have thought, there is nothing fake about this theorem or its proof! Yes, it does resemble an April Fool's prank, but the mathematics behind it are perfectly rigorous and sound, as you can verify for yourself if you wish. It is very much a valid theorem of ZFC set theory, even if some might debate its relative importance in the overall scheme of things. The only thing fake is that Prof. Lirpa uses a pseudonym, since he or she wishes to remain anonymous. Tarski really did prove that x=x in his 1965 paper. While it is possible he wasn't the first to do so, he did not attribute the theorem to anyone else. The theorem -. ( A P~ RR ( i ` 1 ) /\ F (/) ( 0 x. 1 ) ) importantly tells us we cannot prove, for example, ( A P~ RR ( i ` 1 ) /\ F (/) ( 0 x. 1 ) ) if ZFC is consistent. If we utter the latter statement, that will indeed be a hilarious joke (assuming ZFC is consistent) for anyone who enjoys irony and contradiction! But anyone who could prove the latter statement would achieve instant notoriety by upsetting the very foundation that essentially all of mathematics is built on, causing it to collapse like a house of cards, into a pile of (Cantor's) dust that would blow away in the wind. That assumes, of course, that the paradox is not hushed by the established mathematical community, whose very livelihoods would be at stake. In that case, the discoverer might achieve wealth instead of fame. So, in effect the theorem, being preceded by the "not" sign, really tells us: "I am _not_ an April Fool's joke." Thus we are reminded of the Liar Paradox, "this sentence is not true," but with an important difference: paradoxically, avril1 is not a paradox. For those whose Latin is rusty, "quidquid germanus dictum sit, altum viditur" means "anything in German sounds profound." Just as logicians have done with Latin ("modus ponens" and so on), set theorists have chosen German as their primary obfuscating language. For example, set theory texts lend great importance and mystery to the otherwise trivial subset axiom by calling it "Aussonderung." This helps keep the number of set theorists at a comfortable level by scaring away all but a few newcomers, just enough to replace those retiring. To derive avril1, we have used an interdisciplinary approach that combines concepts that are ordinarily considered to be unrelated. We have also used various definitions outside of their normal domains. This is called "thinking outside of the box." For example, the imaginary constant i is certainly not a function. But the definition of a function value, df-fv, allows us to substitute any legal class expression for its class variable F, and i is a legal class expression. Therefore ( i ` 1 ) is also a legal class expression, and in fact it can be shown to be equal the empty set, which is the value of "meaningless" instances of df-fv, as shown for example by theorem ndmfv. http://us2.metamath.org:8888/mpegif/df-fv.html http://us2.metamath.org:8888/mpegif/ndmfv.html Now that the technique has been revealed, I hope that next year someone else will make a contribution. You have a year to work on it. (28-Mar-06) sspr eliminates the hypotheses of the older version, which has been renamed to ssprOLD. (27-Mar-06) As of today's version of set.mm, 183 out of the 315 theorems with names ending "OLD" were removed, so there are only 132 *OLDs left. This has made set.mm about 300KB smaller. (The 132 remaining can't just be deleted, since they currently are referenced by other proofs, which will have to be revised to eliminate their references. Mel O'Cat has started working on some of them.) (20-Mar-06) Stefan has done the "impossible," which is find an even shorter proof of id. (See the note of 18-Oct-05 below.) His new proof strictly meets the criteria I use for accepting shorter proofs (described at the top of the set.mm file). He writes, "Too bad you don't get a special prize for shortening this one!" I agree; any suggestions? About a1d, he writes, "[a1d] is not a shorter proof in compressed format, and is in fact the same size as the old one. However it has fewer steps if expanded out into axioms, so you might want to include it in set.mm anyway." (24-Feb-06) Stefan's sylcom proof has 1 fewer character in set.mm than the previous, and 9 fewer characters in its HTML file. I think we may be approaching the theoretical limit. :) (22-Feb-06) The proof of efcj uses some obsolete theorems with the old convergence ~~>OLD, but I don't have the updated ones ready yet and just wanted to get efcj out of the way since we will need it for more trignometry. Eventually the proof of efcj will be updated. Note that "obsolete" doesn't mean "unsound"; the proof is perfectly rigorous. The purpose of the new notation is to make proofs more efficient (shorter) once everything is updated with it. (17-Feb-06) efadd was completed a little sooner than I thought. Here are some statistics: the set.mm proof (efadd + 28 lemmas) takes 47KB (out of 4.5MB for set.mm). The HTML pages take 4.7MB (out of 372MB total for mpegif). (13-Feb-06) Over the next couple of weeks, we will be proving what has turned out to be a difficult theorem - the sum of exponents law for the exponential function with complex arguments, i.e. e^(a+b)=e^a.e^b. Even though textbook proofs can seem relatively short, the ones I've seen gloss over many of the tedious details. After several false starts I came up with a proof using explicit partial sums of product series and explicit comparisons for the factorial growth (we will use the recent fsum0diag and faclbnd4 for this). The whole proof will have around 30 lemmas. (12-Feb-06) nonbool demonstrates that the Hilbert lattice is non-Boolean. This proves that quantum logic is not classical. Of course this is well known, but I've only seen it stated without proof, so I came up with a formal demonstration. It seems the dimension must be at least 2 to demonstrate non-Boolean behavior. Note that we have already shown that it is orthomodular (in pjoml4), but Boolean is a special case of orthomodular, so that in itself doesn't demonstrate that quantum logic is not classical. (11-Feb-06) Even though the climmul proof is long, I'm not unhappy about it, since Gleason dedicates over 2 pages to the proof (although some of it is an informal discussion of how one goes about coming up with such a proof). While our proof roughly follows Gleason, our trick of constructing a new positive number less than both A and 1, given a positive number A, is not in Gleason - he uses the infimum of A and 1 (bottom of page 170), which would be more awkward (for us at least) to deal with. This trick is proved by recrecltt and is used in climmullem5. (9-Feb-06) I found a slightly shorter equivalent for ax-groth expanded to primitives. The idea was to use fun11 at step 42, so that the old steps 42-60 become 42-48. But the result was a little disappointing. I had higher hopes for the idea but it only ended up removing one binary connective. At least the proof is 59 instead of 71 steps. (The old one has been kept temporarily as grothprimOLD.) Probably the biggest problem is the repeated use of grothlem (4 times) to expand binary relations. I wonder if there is a shorter way to effectively express this concept. (8-Feb-06) dummylink was added for a project to interface O'Cat's mmj2 Proof Assistant GUI with the metamath program's Proof Assistant, but I've discovered that it can be quite handy on its own as suggested by its description. For more background see "Combining PA GUI and CLI - an interim solution?" at the bottom of web page http://planetx.cc.vt.edu/AsteroidMeta/mmj2ProofAssistantFeedback (Downloaders - the Metamath download containing this proof will be in tomorrow's download. In general, the Most Recent Proofs usually take about a day to propagate to the downloads.) (4-Feb-06) More shorter proofs by O'Cat - pm2.43d, pm2.43a. rcla4cv ended up shortening 26 proofs by combining rcla4v and com12. The result was a net reduction in the database size, even after accounting for the new space taken by rcla4cv. (3-Feb-06) Mel O'Cat found shorter proofs for sylcom, syl5d, and syl6d while having fun with his new toy, the Proof Assistant GUI. Note: the new proofs of of syl5d and syl6d have the same number of logical steps, but proofs are shorter if we include the unseen wff-building steps. Out of curiosity I restored the original syl5d proof, since it had already been shortened by Josh Purinton, and called it syl5OLDOLD. Here are the complete proofs for the syl5d versions: syl5d: 14 steps wph wps wta wch wth wph wta wch wi wps syl5d.2 a1d syl5d.1 syldd $. syl5dOLD: 16 steps wph wps wch wth wi wta wth wi syl5d.1 wph wta wch wth syl5d.2 imim1d syld $. syl5dOLDOLD: 19 steps wph wta wps wth wph wta wch wps wth wi syl5d.2 wph wps wch wth syl5d.1 com23 syld com23 $. (30-Jan-06) Today we start a brand new proof of the binomial theorem that will be much shorter than the old one. It should also be much more readable. This is what the new one will look like (A e. CC, B e. CC): ( N e. NN0 -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N C. k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) ) Compare to the old, binomOLD: ( ( N e. NN0 /\ A. k e. ( 0 ... N ) ( F ` k ) = ( ( N C. k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) ) ) ) -> ( ( A + B ) ^ N ) = ( <. 0 , N >. sumOLD F ) ) (24-Jan-06) (Compare note of 22-Oct-05.) Per the request of Mel O'Cat, I eliminated all connective overloading in set.mm by making weq, wel, and wsb "theorems" so that he can use set.mm with his GUI Proof Assistant. This involved moving set theory's wceq, wcel, and wsbc up into the predicate calculus section, which is somewhat confusing, so I added extensive commenting to explain it hopefully. Note that the web page "proofs" of weq, wel, and wsb have only one step: this is because they are syntax proofs, and all syntax building steps are suppressed by the web-page generation algorithm, which doesn't distinguish weq, etc. from "real" theorems. I'm not yet sure if it's worth changing the algorithm for this special case. To see the actual steps, in the Metamath program type "show proof weq /all". (20-Jan-06) supxrcl shows the usefulness of the extended reals: the supremum of any subset always exists. Compare the non-extended real version suprcl, which has a complicated antecedent that must be satisfied. (19-Jan-06) A new set theory axiom, ax-groth, was added to the database. This axiom is used by Mizar http://mizar.org to do category theory (that ZFC alone cannot do), and I think it is appropriate to add it to set.mm. One of the negative aspects of this axiom (aesthetically speaking) is that it is "non-elementary" and very ugly when expanded to primitives, unlike the ZFC axioms. I worked out grothprim because I was curious to see what it actually looks like. I don't think grothprim will actually be used for anything since it is impractical; instead, ax-groth would be the starting point. However, grothprim can provide a benchmark for anyone seeking a shorter version. There may be a theoretical reason why it can't be as short as say ax-ac, but I don't think anyone knows what the shortest possible equivalent is. mmset.html has also been updated to include ax-groth below the ZFC axioms. I wrote to Jeff Hankins: I added ax-groth partly in response to your email on Mycielski's ST set theory,* although it's been on my backburner for a while. In my mind, ax-groth "completes" set theory for all practical purposes. (The Mizar people, who use this axiom, also think so.) Unlike the controversial assertions of ST, ax-groth is relatively mild and uncontroversial - I don't know of any debate over it, unlike the debate on the Continuum Hypothesis. I am pretty sure that Mycielski's Axiom SC implies ax-groth from his comments, although I haven't worked out a proof. So ZFC+ax-groth is most likely a subset of ST. * http://www.ams.org/notices/200602/fea-mycielski.pdf - free AMS sign-up required to view article (12-Jan-06) The exponential function definition df-ef is new. Yesterday's version of df-ef was reproved as theorem dfefOLD that will eventually be deleted after the old infinite summation notation is phased out. Compare the new exponential function value formula, efvalt, with the old one, efvaltOLD. Don't you agree that it is much easier to read? This kind of thing makes me believe that the effort to introduce the new summation notation was worthwhile. :) In addition, will have a much nicer version of the binomial theorem (whose old version has already been renamed to binomOLD), with a much shorter proof - stay tuned! (11-Jan-06) isumvalOLDnew links the old and new definitions of infinite sum, allowing us to temporarily reuse theorems in the old notation until they are phased out. See comments below of 1-Nov-05, 2-Nov-05, 20-Dec-05, and 21-Dec-05 regarding the new finite/infinite sum notation df-sum. The present definition of the exponential function, df-ef, makes use of the obsolete infinite sum notation. dfefOLDnew will replace df-ef in the next few days and become its new official definition. The old df-ef will become a (temporary) theorem that will be used to support the old infinite sum notation until it is phased out. gch-kn was updated with new hyperlinks. (10-Jan-06) Regarding the 9-Jan-06 item in "Also new", the primary reason I added the "/except" switch to "minimize_with" was to exclude 3syl. While 3syl may shorten the uncompressed normal proof, it often makes compressed proofs grow longer. This happens when the intermediate result of two chained syl's is used more than once. When the intermediate result disappears due to 3syl, two formerly common subproofs have to be repeated separately in the compressed proof - part of the compression is achieved by not repeating common subproofs. So, typically I exclude 3syl then minimize with it separately to see if the compressed proof shortens or lengthens. Maybe I'll add an option to also check the compressed proof length instead of or in addition to the normal proof length, but the "/exclude" was easier to program, and curiously 3syl is the only problematic theorem I'm aware of. (9-Jan-06) climOLDnew is a temporary theorem that links the old and new limit relations, ~~>OLD and ~~>. This will let us "jump ahead" and work on exponentiation, etc. with the new notation before cleaning up all the ~~>OLD stuff (which I will still clean up eventually). The linkage is needed to avoid any gaps in the released set.mm. (The metamath command "verify proof *" should always pass for the daily releases of set.mm, ensuring absolute correctness of its contents - even the stuff that's obsolete.) The main difference between ~~>OLD and ~~> is that ~~>OLD has the rigid constraint that the sequence F be a function from NN to CC, whereas ~~> allows F to be any set with lots of irrelevant garbage in it as long as it eventually has function values in CC beyond some arbitrary point. This can make ~~> much more flexible and easier to use. The uppercase "OLD" in climOLDnew means the theorem will go away; for my cleanup I will be phasing out and deleting all theorems matching *OLD*. Currently there are 380 *OLD* theorems due to be phased out. They can be enumerated by counting the lines of output of the metamath command "show label *OLD*/linear". (6-Jan-06) syl*el* are all possible combinations of syl5,syl6 analogs for membership and equality. I added them to shorten many proofs, since these patterns occur frequently. (Since 1999 I've added the syl*br* versions of these for binary relations and found them useful, so I decided to add the syl*el* versions.) There is a curious asymmetry in which ones ended up being useful: syl5eqel got used over 30 times, whereas syl5eleq isn't used at all so far. I don't know if this is because I wrote the original proofs with certain patterns subconsciously repeated, or if there is something more fundamental. (3-Jan-06) r19.21aiva adds 319 bytes to the database, but it reduces the size of about 50 (compressed) proofs by 765 bytes total, for a net reduction in database size of 466 bytes. (21-Dec-05) All theorems that involved df-fsum have been updated to use the dual-purpose (finite and infinite) df-sum instead. So, we now have: Definition Token Symbol Yesterday Today Yesterday Today Yesterday Today df-sum df-sum sum_NEW sum_ \Sigma_NEW \Sigma df-fsum df-fsum sum_ sum_OLD \Sigma \Sigma_OLD df-fsumOLD df-fsumOLD sumOLD sumOLD \Sigma_OLD \Sigma_OLDOLD The names with "OLD" are now kind of oddly inconsistent, but everything with "OLD" in it (whether label or token) will eventually be deleted so it doesn't really matter. (20-Dec-05) The new finite sum stuff looks like it will be very useful, and we will need an infinite sum version to replace the current df-isum. Rather than repeat the whole development with new equality, bound variable, etc. utility theorems, I decided to combine the two definitions. The new combined definition is called df-sum, which is basically the union of two definitions. The index range (finite or infinite) determines whether the sum is finite or infinite. See the comments in df-sum. We need about half a dozen utility theorems. Then, after changing the "sigmaNEW" to "sigma", we can "plug in" the new definition and re-use the theorems we have already developed for finite sums without further modification. fzneuzt is the basic theorem that lets us distinguish the finite half vs. the infinite half of df-sum. (14-Dec-05) fsum1sNEW (to be renamed fsum1s) exploits class2set to eliminate the hypothesis of fsum1slem, so that we require only existence of A(M) as a member of some arbitrary class B, rather than requiring that it be a complex number (as yesterday's fsum1s requires). This will shorten future proofs by allowing us to apply fsum1sNEW directly when A is a real, rational, etc. I had almost forgotten about class2set, which I think is a neat trick. Yesterday's fsum1s will be renamed to fsum1sOLD and eventually deleted. I'm not sure if fsum1s2 will be useful, but it lets us show off an application of the interesting fz1sbct. (13-Dec-05) fsum1slem shows an example of a use for the new substitution-for-a-class notation. Compare it to the implicit substitition version fsum1. fsum1s turns the hypothesis A e. V of fsum1slem into an antecedent. Since A is quantified, we have to work a little harder than usual to accomplish this. (4-Dec-05) See http://planetx.cc.vt.edu/AsteroidMeta//metamathMathQuestions for comments on equsb3. (30-Nov-05) csbnestg is the same as csbnestglem except that it has fewer distinct variable restrictions. Its proof provides another example of a way to get rid of them; the key is using a dummy variable that is eliminated with csbcog. I think it is a neat theorem and was pleasantly surprised that so few distinct variable restrictions were needed. The antecedents just say