I have not grasped what I wanted (yet). But Thanks to your 3 answers, I think that I understand a bit your point. I will now have to ponder your answers a lot. There is a lot to think about in here for me. I'll try to get it (real hard, because I really really need this knowledge)
Many thanks for your answers and for the kind help :) Le mardi 29 octobre 2019 22:46:39 UTC+1, Norman Megill a écrit : > > fsumshft.5 doesn't have a "ph ->" antecedent because its purpose is simply > to specify that B is a substitution instance of A. We sometimes call this > "implicit substitution" as opposed to "explicit substitution", which would > be B = [. ( k - K ) / j ]. A (or just using [. ( k - K ) / j ]. A in place > of B instead of having a separate hypothesis). > > Compare, for example, the implicit substitutions in first 4 hypotheses of > the deduction form nn0indd. > > In order to use a theorem with implicit substitution, the proof usually > eliminates the implicit substitution hypotheses with a chain of equality > and/or biconditional theorems. The hypotheses are then completely > eliminated, and ph is hardly ever needed to achieve that (if ever). So we > rarely bother to add a ph antecedent. Offhand I can't recall a case where > it would have helped in practice. > > The primary reason we tend to use implicit substitution rather than > explicit substitution is to obtain shorter proofs. Note that (in this > case) the variable j doesn't appear in B i.e. $d j B. If instead we used > [. ( k - K ) / j ]. A, we might have to use say reximd in place of reximdv, > requiring a chain of nf* theorems to eliminate the "not free in" hypotheses > and maybe making the proof longer. Or, alternately, we could use > intermediate dummy variables with cbv* + reximdv, also making the proof > longer. > > There are also theorems like sbcie to convert implicit to explicit. > Occasionally we have both versions of a theorem such as finds1 (implicit) > vs. findes (explicit). Note that the latter hasn't found a use yet. > > Norm > > On Monday, October 28, 2019 at 5:18:40 PM UTC-4, Olivier Binda wrote: >> >> Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? >> >> fsumshft.5 [image: |-] [image: (][image: j] [image: =] [image: (][image: >> k] [image: -] [image: K][image: )] [image: ->] [image: A] [image: =] [image: >> B][image: )] >> Is the same theorem with ( ph -> ( j = ( k-K ) -> A = B ) ) false ? or >> stupid ? or unnecessary ? >> >> It looks stronger to me as I probably cannot prove it easily from fsumshtf >> >> I am still grasping at all the subtleties of Metamath, so I may not >> understand something important here. >> >> Could someone please enlighten me ? >> >> Best regards, >> Olivier >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/95c4e196-87b2-4fc4-9667-7b2199c13ae7%40googlegroups.com.
