On Mon, Jun 14, 2021 at 3:43 AM Kunhao Zheng <[email protected]> wrote:
> One more question somehow irrelevant: While I was jumping around
> different pages of metamath, I found some of definitions (df-mulr) is like
> .r = Slot 3, do you know what it means by Slot?
>
That has to do with the encoding of structures. "Slot N" defines a function
whose action is like ( .r ` S ) = ( S ` 3 ), that is, .r acts on
structures, viewed as functions, to extract the element labelled "3". This
is then paired with the ndx "structure", which is just the identity
function, so that ( .r ` ndx ) = ( ndx ` 3 ) = 3, so you will usually see (
.r ` ndx ) used instead of 3 (because we want to encapsulate the actual
integer being used here). Finally, a concrete structure will have something
like
MyRing = { <. 1 , B >. , <. 2 , + >. , <. 3 , * >. }
which defines a finite function with value "B" at 1, "+" at 2 and "*" at 3.
In order to make it more clear which component is which we use that ndx
trick:
MyRing = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , + >. , <. ( .r `
ndx ) , * >. }
and now when you write ( .r ` MyRing ) it evaluates to ( MyRing ` 3 ) which
is *. So this is all just to extract the ring multiplication operation from
a structure which specifies what the base set, addition, and multiplication
of that structure is. The class "Ring" is the collection of all structures
whose addition and multiplication operations extracted in this way adhere
to the ring axioms, so we would have a theorem like "MyRing e. Ring" and
then use it together with lemmas like "( .r ` MyRing ) = * " to apply ring
theorems.
Mario
--
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/CAFXXJSvJpU2choctgJg-C0Hc8y1FtiEtqqfxXZXj7tHzgcBVNA%40mail.gmail.com.
