Need opinion on proof (if $ax=a$, then $x=1$) I haven't written a lot of proofs so I need the opinion of the experts on my proof of a simple proposition.
Here's the various properties I used:
(P10) (Trichotomy law) For every number $a$, one and only one of the
following holds:
(i) $a = 0$,
(ii) $a$ is in the collection $P$,
(iii) $—a$ is in the collection $P$.
(P7) For every number $a$ not equal to $0$, there is a number $a^{-1}$ such that
$a \cdot a^{-1} = a^{-1} \cdot a = 1$.
(P6) If $a$ is any number, then
$a \cdot 1 = 1 \cdot a = a$.
If $ax=a$ for some number $a$ different from $0$, then $x=1$.(Spivak's calculus.)
I consider two cases: $a>0$ or $a<0$.
By definition (Given in Spivak's calculus):
$a>b$ if $a-b$ is in the collection $P$ ($P$ being the collection of all positive numbers.)
$a>0$ because $a-0$ is in collection $P$ by trichotomy law (P10)
So $ax=a$
by P7 $aa^{-1}x= aa^{-1}$
$1x=1$
by P6 $x=1$
Second case:
By definition:
$a< b$ if $b>a$
$a<0$ because $0>a$
Now, we do the same thing as the previous case.
Proposition proven!
Here's Spivak's answer
$1=a^{-1}a=a^{-1}(ax)=(a^{-1}a)x=1x=x$
I guess he does his proof by "construction", beginning by $a=a$, then $aa^{-1}= a*a^{-1}$, etc.
Any opinions? Thank you!
 A: To explain Spivak's proof rigorously, here it is step by step:
Hypothesis: Let $ax = a$, and let $1$ be the identity such that $1a = a = a1$ for all $a$.
Then,
$$\begin{align*}
1 &= a^{-1}a \tag{by definition of inverse}\\
  &= a^{-1}(ax) \tag{since $ax = a$, and symmetry of $=$} \\
  &= (a^{-1}a)x \tag{by associativity} \\
  &= 1x \tag{by definition of inverse} \\
  &= x.  \tag{by definition of identity}
\end{align*}
$$
Therefore, $x=1$.
A: Your approach is okay, but there are a few things that can/should be improved. For one thing, unless you wish to use commutativity of multiplication, then you should be more careful in the step where you multiply by $a^{-1}.$ Note also that you are using associativity of multiplication without mention there. Being cautious, we can take the following steps: $$a\cdot x=a,$$ and so $$a^{-1}\cdot(a\cdot x)=a^{-1}\cdot a\\a^{-1}\cdot(a\cdot x)=1\\(a^{-1}\cdot a)\cdot x=1\\1\cdot x=1\\x=1$$
Another thing to observe is that there is no need to split by cases, as we never used the hypothesis that $a\in P$ at any point in the reasoning above. The existence of $a^{-1}$ depends only on $a$ being non-zero.
The above is effectively the same as Spivak's proof, in less condensed form.

To my mind, even Spivak's proof could use a bit of improvement. I would instead have proceeded as follows (with the condensed form of my proof above):
$$x=1\cdot x=\left(a^{-1}\cdot a\right)\cdot x=a^{-1}\cdot(a\cdot x)=a^{-1}\cdot a=1.$$
At first glance, they look exactly the same, except that I inserted the multiplication symbol and went in reverse order. Due to the fact that equality is a symmetric relation (as Arkamis mentioned), they in fact are equivalent in this case. So what's the big deal? Let me see if I can illustrate why this is an improvement. First, I will use a specific example, and then move on to an analogous abstract example.
Specific Example: Suppose that $P$ is the set of positive real numbers (hereinafter referred to as "positives"), and let $\cdot$ and $\le$ (respectively) be the usual multiplication operation and non-strict order relation on the real numbers, and recall that there is a particular positive that we call $1$. Note that the following properties are satisfied:


*

*For all positives $r,s,$ we have that $r\cdot s$ is a positive.

*For all positives $r,s,t,$ if $r\le s$ and $s\le t,$ then $r\le t.$

*For all positives $r,$ we have $r\le 1\cdot r.$

*For all positives $r,s,t,$ if $s\le t,$ then $r\cdot s\le r\cdot t.$

*For all positives $r,$ there is a positive $r^{-1}$ such that $1\le r^{-1}\cdot r$ and $r^{-1}\cdot r\le 1.$

*For all positives $r,s,t,$ we have $(r\cdot s)\cdot t\le r\cdot(s\cdot t).$


Of course, there are many more basic properties satisfied by the positives under the operation $\cdot$ and the relation $\le,$ but they are irrelevant to my point.
Now, I make the following claim:

If $a,x$ are positives such that $a\cdot x\le a,$ then $x\le 1.$

This, of course, is related to the claim in your question rather closely, but on their own, neither claim implies the other. More important is the fact that they have the same form, in a sense. To explain what I mean by that, let me switch to my...
Abstract Example: Suppose that we have a set $S$ of objects. Perhaps these objects are numbers of some kind, or perhaps not, but it doesn't matter. (Hereinafter, whenever I refer to "objects," I will specifically be referring to objects in the set $S$.) Let us further suppose that we have an operation $\star$ and a relation $\nearrow$ on $S,$ and that there is a particular object called $e.$ Moreover, suppose that the following properties are satisfied:


*

*For all objects $r,s,$ we have that $r\star s$ is an object.

*For all objects $r,s,t,$ if $r\nearrow s$ and $s\nearrow t,$ then $r\nearrow t.$

*For all objects $r,$ we have $r\nearrow e\star r.$

*For all objects $r,s,t,$ if $s\nearrow t,$ then $r\star s\nearrow r\star t.$

*For all objects $r,$ there is an object $\overline r$ such that $e\nearrow \overline r\star r$ and $\overline r\star r\nearrow e.$

*For all objects $r,s,t,$ we have $(r\star s)\star t\nearrow r\star(s\star t).$


Now, I make the following claim:

If $a,x$ are objects such that $a\star x\nearrow a,$ then $x\nearrow e.$

Observe that properties 1-6 and the claim match up precisely with properties 1-6 and the claim from above, simply by interchanging "object" with "positive," $\star$ with $\cdot,$ $\nearrow$ with $\le,$ $\overline r$ with $r^{-1},$ and $e$ with $1.$ In this case, though, we know much less than we did before. For example, it is possible that $e\star r$ and $r\star e$ may be different objects for some object $r,$ but there is no positive $r$ for which $r\cdot 1$ and $1\cdot r$ are distinct. However, those extra properties are completely extraneous assumptions. We will not need them at all to prove our claim--indeed, properties 1-6 will be all we need. Property 1 comes into play so that we can make statements involving both $\star$ and $\nearrow$ in the first place, and beyond that, since $a\star x\nearrow a,$ then $$x\overset{3}{\nearrow}e\star x\overset{5,4}{\nearrow}\left(\overline a\star a\right)\star x\overset{6}{\nearrow}\overline a\star\left(a\star x\right)\overset{4}{\nearrow}\overline a\star a\overset{5}{\nearrow} e,$$ at which point repeated applications of property 2 show us that $x\nearrow e,$ as desired.
The same proof scheme will work for the earlier claim I made, simply by making the interchanges mentioned above. Likewise, the same proof scheme will work for the claim in your post, interchanging "object" with "non-zero number,"$\star$ with $\cdot,$ $\nearrow$ with $=,$ $\overline r$ with $r^{-1},$ and $e$ with $1.$ In that case: the analogs to 1 and 4 follow from the fact that $\cdot$ is an operation on the (non-zero) reals; to 2, from transitivity of $=$; to 3, from P5, P7, and symmetry of $=$; to 5, from P8; to 6, from P6.
This is what I mean when I say that rigorous proofs, together with minimal assumptions and hypotheses, are most useful. The less that is required for a particular proof scheme, the more broadly generalizable the scheme will be.
Spivak's proof, on the other hand, needs a few additional formal assumptions (beyond the 1-6 scheme) in order to draw the desired formal conclusion.
A: Spivak essentially scales by $a^{-1}$ the equation $\,a\ =\ ax\,$ to deduce $\,1\ =\ x.$
$$\ \begin{eqnarray} a^{-1}\ (a\! &&  =\ \ \ ax)\ \ \ \ \rightarrow\ \ \ \ \color{#c00}1\ =\ x\\
{\rm i.e.}\ \ \ \color{#c00}1\ =\ a^{-1{\phantom{I^I}}}\!\!\! a &=& a^{-1}(ax) = (a^{-1}a)x = x
\end{eqnarray}$$
This can be viewed as a special case of the uniqueness of solutions to $\, ax = b.$
For if $x',x$ are solutions $\ ax' = b = ax\,\Rightarrow x' = x\ $ by scaling by $a^{-1}$ to cancel $a,\,$ as above.  
Spivak's proof is the special case $\ x' = 1,\,\ b = a.$
