On Thu, Oct 12, 2023 at 1:46 AM 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
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
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.
On Thu, Oct 12, 2023 at 12:46 AM bil...@gmail.com wrote:
> You say that the definitions are the same, but to me
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
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
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,
