Thank you all for your helpful suggestions. Thierry's proof of brepval is similar to my "workarounds": building-up equalities or equivalences in lieu of actual substitution.
Alexander's proofs of sbiei and sbieg are so simple and elegant, I'm sorry I didn't try it myself. The challenge will be establishing ( [ y / x ] ph <-> ps ). Given a distinct variable hypothesis $d y ph $. there should be some (easy?) way to show that ps is the same as ph having y substituted for x. I will look more closely at David's algebra helpers. --Brian On Tuesday, December 28, 2021 at 1:46:19 PM UTC-6 David A. Wheeler wrote: > > > > On Dec 27, 2021, at 9:08 PM, Brian Larson <[email protected]> wrote: > > > > I often want to use substitution to do something like this: > > |- ph & |- x = y |- ( [ y / x ] ph <-> ps ) ==> |- ps > > But I'm having trouble showing that ps results from the proper > substitution of y for x in ph. > > > > Mario wrote some hints: > > > > In Conversation: Trying to generalize David Wheeler's Algebra helpers: > > > > "This isn't the way we usually prove substitutions. df-sb is not really > a substitution operator, it is more like a "deferred substitution", a term > that is equivalent to the result of the substitution without actually > performing it. To actually perform a substitution, we use so-called > "equality theorems". These theorems usually end in *eq, *eq1,*eq1i, *eq1d > and so on, and prove A = B -> P(A) = P(B) for different values of P. By > cobbling them together you can subtitute into any expression." > > Perhaps another way to understand it is that you have to start by showing > that two > simple expressions are equivalent, then use other theorems to build up & > prove that the > larger expressions including them are equivalent. > > My "Algebra helpers" were intended to make it easier to skip those steps > in common cases. > I made samples & stopped because I didn't know if anyone would use them. > Also, I made both deduction form (ph -> ... ) & non-deduction form > versions; > if the deduction forms are all that would be used, well, let's focus on > that. > > If someone *does* find them useful, let me know, that work could be > continued > if there were actual users :-). > > --- David A. Wheeler > > > > > In Conversation: Breaking news: LTL section valid: > > > > "This kind of statement does not work for metamath, because we don't > have a general proper substitution mechanism. The one we have (df-sb) > reduces to the metatheorem ( x = y -> F(x) = F(y) ) which still must be > provided separately, which is why we need equality theorems or axioms for > every primitive operation." > > > > MM> sh st *eq > > (and *eq1, *eq1i, and *eq1d) > > return scads of interesting theorems, but I don't understand how to use > the "equality theorems" to perform proper substitution. > > > > Please describe the general principle, and give a simple example. > > > > --Brian > > > > > > > > -- > > 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/c7d4d8a3-b112-43cd-b154-5fcf816d978dn%40googlegroups.com > . > > -- 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/14743288-c78f-46e2-bdd1-afe9b26aecbdn%40googlegroups.com.
