Hi Brian, As you found out, equality theorems end in `eq`. They prove the equality for an expression, given equality for one term of that expression. For example, ~ sumeq1d states |- ( ph -> A = B ) ==> ( ph -> sum_ k e. A C = sum_ k e. B C ) . Here we have effectively substituted ` A ` for ` B ` in the sum expression.
There is another theorem ~ sumeq2dv, for equality of the other term (the summand ` C `). There is also a related family of theorems for changing the bound variable ` k ` into another variable (for my sum example, that would be ~ cbvsum). Change bound variable theorems are not equality theorems per se, but they also allow a substitution of a part of the formula, namely, the bound (set) variables. You can for example have a look at http://us2.metamath.org:88/mpeuni/breprval.html, step 3~8 for how several equality theorems are used together to prove a more complex substitution. What we end up with is an equality, or an equivalence, if you look at the result of step 6, ~ eqeq1d, which we can then chain with more equalities to get the desired result. I hope this helps! Maybe if you could give the actual case you'd like to solve, we could help you prove it or rewrite it in a way which is easier to prove. BR, _ Thierry On 28/12/2021 10:08, Brian Larson 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." 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 <https://groups.google.com/d/msgid/metamath/c7d4d8a3-b112-43cd-b154-5fcf816d978dn%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/6327d514-5410-e7e3-17ca-5201d23b6573%40gmx.net.
