On Tue, Dec 28, 2021 at 4:11 PM Brian Larson <[email protected]> wrote:
> 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. > An equivalent way to write that hypothesis, and by far preferred in set.mm, is ( x = y -> ( ph <-> ps ) ). Since we still have $d y ph $., you can't just take ps to be ph; if ph contains any occurrences of x you are forced to go and replace the x by something else, and the obvious thing is to use the equality hypothesis to replace each x with a y. The *eq theorems are the means by which we do this. For example, suppose ph was ( x + 2 ) < 5. Then when you apply this theorem, you will get a subgoal of the form 1: |- ( x = y -> ( ( x + 2 ) < 5 <-> ?ps ) ) where ?ps is a placeholder to say that we don't know what to put in place of it yet. In this case, we want to prove it for ?ps := ( y + 2 ) < 5, because this is the result of proper substitution of y for x in ph. But anything equivalent to ( y + 2 ) < 5, like ( ( y + 2 ) < 5 /\ T. ) would also be provable in this position. 1: |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) ) To simplify this goal, we notice that the head expression in ph is a binary relation df-br (applied to three arguments "( x + 2 )", "<", and "5"), and only the first one needs to change, the other two are constants. So we apply http://us.metamath.org/mpeuni/breq1d.html , which yields: 2: |- ( x = y -> ( x + 2 ) = ( y + 2 ) ) 1:2:breq1d |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) ) Now the head term of the LHS is df-ov applied to "x", "+" and "2", and again only the first term needs to change. In fact, the first term is actually the x we want to replace, so we can use oveq1 instead of oveq1d here: 2::oveq1 |- ( x = y -> ( x + 2 ) = ( y + 2 ) ) 1:2:breq1d |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) ) and now we're done. This is a small example but hopefully it shows you how these *eq theorems can be used to prove theorems of the form ( x = y -> P(x) = P(y) ) where P(x) is any class or wff expression with one or more x's in it, and P(y) is the corresponding expression with the x's replaced by y. If you have a more pertinent example for your use case, please speak up. Mario On Tue, Dec 28, 2021 at 4:50 PM David A. Wheeler <[email protected]> wrote: > > > > On Dec 28, 2021, at 4:11 PM, Brian Larson <[email protected]> > wrote: > > > > I will look more closely at David's algebra helpers. > > Enjoy. You won't find any cleverness or elegance in them. > Their purpose is to prove "obvious" things, generally from the outside in, > so you don't have to do them. > > --- David A. Wheeler > > -- > 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/E5BB092F-3464-4B61-BBF2-DD170628896E%40dwheeler.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/CAFXXJStZ%3Dvcu09-mY6YVf7Pr%2Bbg997X6yy1fqtQyTYz3UXKR-A%40mail.gmail.com.
