# Metamath unification example

Basic question

Suppose we define a point and some related stuff:

1. x , y are reals
2. Point ( x , y )
3. Abscissa ( Point ( x , y ) ) = x
4. Ordinate ( Point ( x , y ) ) = y

And we want to have/prove:

1. Point ( Abscissa ( P ) , Ordinate ( P ) ) = P

Question: How can this be defined in metamath?

I'm guessing 5 as a provable 'p' and the others as 'a' and 'f' !?

In 5, do we need a hypothesis saying P = Point ( x, y ) ?

When I ask about unification is for having expression 5 as qed, and defining prior statements in stack that can unify with it, and eventually solving it.

PS: might be good to have a tag for dumb questions

• We have a tag beginner, but there are no dumb questions as long as you made an effort yourself to think about the question, even if it is very simple!
– Trebor
Sep 7 at 14:04
• @Trebor thanks for feedback. And for what I guess its a gentle approval. It's hard to guess what effort is enough/acceptable, and what base (math) knowledge is ok. Sep 7 at 14:36

I'm assuming you want to achieve this in the set.mm database for set theory with classical logic. In that case, everything is a set (or a class), and therefore we have to look for sets which can represent your points.

I see at least three ways to do that:

## Using ordered pairs

This is probably the most simple and natural way. In this case abscissa would be the first component of the pair, which can be extracted with 1st, and ordinate would be the second component of the pair, which can be extracted with 2nd.

Your points would then be elements of the cartesian product of the set of the real numbers, RR, with itself: ( RR X. RR )

Given X and Y, one would build a point by constructing an ordered pair, noted as <. X , Y >..

Your theorem would then be written something like:

|- ( P e. ( RR X. RR ) -> <. ( 1st  P ) , ( 2nd  P ) .> = P )


This is a special case of the theorem 1st2nd2 which is already in the set.mm database.

## Using complex numbers

These are naturally well suited for representing points on the plane, so you will be able to apply e.g. translations/rotations. In this case you extract the abscissa by using the Re function, which gives the real part of the complex number, and the ordinate using the Im function, which gives the imaginary part.

Your points will be elements of the complex number, noted CC.

Given X and Y, to build back the corresponding complex number, one multiplies the imaginary part with the imaginary unit _i and add the real part, so ( X + ( _i x. Y ) ).

So your theorem will then be stated as:

|- ( P e. CC -> P = ( ( Re  P ) + ( _i x. ( Im  P ) ) ) )


This is the theorem replim which is already in the set.mm database.

## Using a function

This is nearer the usual concept of (computer science) class, and the notation you've used. In this case the points will be functions, with for example the abscissa being the function evaluated at 0, ( P  0 ), and the ordinate being the function evaluated at 1, ( P  1 ). Note that instead of 0 and 1, any two values could have been used, those are just possible choices as an example.

In this case your points will be function from the unordered pair { 0 , 1 } into the real numbers RR. This set can be written using the power notation: ( RR ^m { 0 , 1 } ). We could also have used the notation  P : { 0 , 1 } --> RR.

Behind the scenes, functions are collections of ordered pairs, so in order to build back "point object" from X and Y, its values at 0 and 1, you will build a set containing those two function evaluations.

This is written { <. 0 , X >. , <. 1 , Y >. }.

Your theorem will look like this:

|- ( P e. ( RR ^m { 0 , 1 } ) -> F = { <. 0 , ( P  0 ) >. , <. 1 , ( P  1 ) >. } )


This formulation is not directly in the database, but could easily be derived from e.g. fnpr2g

This last option would be similar to the way points of the Euclidean vector space / Hilbert space of two dimensions is encoded in set.mm, see ehlbase for N = 2.