Question on definition of magma

[bil...@gmail.com]

The given definition of magma is:

df-mgm |- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }

Would it be ok to define magma as follows:

df-mgm  |-  Mgm = { g | A. x e. ( Base ` g ) A. y e. ( Base ` g ) ( x ( +g ` g ) y ) e. ( Base ` g ) }

If so, what problems would result ?

In other words, why was the given definition chosen over the more explicit definition ?

[Mario Carneiro]

Those two definitions are the same except you have removed the substitutions b := ( Base ` g ) and o := ( +g ` g ) . The substitutions are there to make the definition more readable (and usually shorter, although it might be a wash in a short definition like this one). For a more elaborate example check out https://us.metamath.org/mpeuni/df-lmod.html .

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3e26ed0a-5b15-4c29-adf5-434fb591eb96n%40googlegroups.com.

[bil...@gmail.com]

You say that the definitions are the same, but to me "substitution" needs to be proved in a roundabout way: that is, it is not just substituting "( Base ` g )" for "b".

The theorem ismgm that immediately follows the definition for Mgm requires 19 steps, whereas only 8 steps are needed for the revised definition.

I guess you answered my question that the revised definition is valid.

[Mario Carneiro]

Usually we prioritize minimizing the length of the definition (number of symbols) over the length of the extraction theorem, because the former is an axiom and the latter is not.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/726a9570-1c6f-47ea-86af-ba553f89690fn%40googlegroups.com.

[bil...@gmail.com]

I am at a more basic level than what you are trying to address. My goal is to learn how to prove theorems in metamath.

My current task is to do the follow: given B = { x | ph }, how would I prove that A e. B. This is beginning level stuff.

I see that there is  theorem elab2g that would be useful: I just need to show the following: x = A -> ( ph <-> ps )

For substitution: df-sb: [t/x] phi  <->  Ay ( y = t -> Ax ( x = y -> phi ))

I find this more intuitive: sb5 |- ( [. y / x ]. ph <-> E. x (  x = y /\ ph )

Since I was having trouble with proving things with the substitution notation, I was trying to see if I could get by without using it.

Again, I understand that the substitution notation is working at a higher conceptual level. But, I am trying to learn that conceptual level.

My original question was whether the definition of Mgm required the substitution notation. Your answer was that it was not required. Also, my revised definition would not produce problems later on.

[Mario Carneiro]

On Thu, Oct 12, 2023 at 1:46 AM bil...@gmail.com <bil...@gmail.com> wrote:

I am at a more basic level than what you are trying to address. My goal is to learn how to prove theorems in metamath.

My current task is to do the follow: given B = { x | ph }, how would I prove that A e. B. This is beginning level stuff.

I see that there is  theorem elab2g that would be useful: I just need to show the following: x = A -> ( ph <-> ps )

Yes that's the right theorem to apply when this is your goal. Normally you would take ps to be ph with all occurrences of x replaced by A, and use equality theorems to prove it.

 

For substitution: df-sb: [t/x] phi  <->  Ay ( y = t -> Ax ( x = y -> phi ))

I find this more intuitive: sb5 |- ( [. y / x ]. ph <-> E. x (  x = y /\ ph )

Generally you should not need to deal with the definitions of basic functions like this (in fact, even in advanced definitions you almost never use the definition directly, you prove an extraction lemma and use the lemma instead of the definition). It is defined in a slightly weird way to deal with some edge cases involving when t is x or an expression containing x, but generally you can just choose it to not overlap and then the definition simplifies. The usual way to unpack a substitution is using sbie or one of its many variants (such as sbcied2 which shows up in the ismgm theorem you referenced).