<s>[INST] Proof Verification : Prove -(-a)=a using only ordered field axioms I need to prove for all real numbers $a$, $-(-a) = a$ using only the following axioms:


Thanks to many members of the Mathematics Stackexchange Community, I have the following proof worked out:
Theorem: The Additive Inverse Identity is Unique
$
( \forall a,b,c \in \mathbb{R} )(a+b=0) \land (a+c=0) \\
( \forall a,b,c \in \mathbb{R} )(a+b=a+c) \\
( \forall a,b,c \in \mathbb{R} )(b=c) \\
\text{QED} \\
$
Theorem $\textbf{a} \cdot \textbf{0 = 0}$
$
\begin{align}
a \cdot 0 &= a \cdot 0 \\
a \cdot (0 + 0) &= a \cdot 0 \\
a \cdot 0 + a \cdot 0 &= a \cdot 0 \\
a \cdot 0 + a \cdot 0 + (-a) \cdot 0 &= a \cdot 0 + (-a) \cdot 0 \\
a \cdot 0 &= 0 \\
&\text{QED} \\
\end{align}
$
Theorem: $-\textbf{1} \cdot \textbf{(a) = (}-\textbf{a)}$
$
\begin{align}
a \cdot 0 &= 0 \\
a \cdot \left[ 1 + (-1) \right] &= a + (-a) \\
1 \cdot a + (-1) \cdot a &= a + (-a) \\
-1 \cdot (a) &= (-a) \\
&\text{QED} \\
\end{align}
$
Theorem: $-\textbf{(}-\textbf{a) = a}$
$
\begin{align}
0 &= 0 \\
-a \cdot 0 &= 0 \\
-a \cdot \left[ 1 + (-1) \right] &= 0 \\
-a \cdot 1 + -a \cdot (-1) &= 0 \\
-a + \left[ -(-a) \right] &= 0 \\
-(-a) &= a \\
\text{QED} \\
\end{align}
$
Does everything look alright? Have I missed anything?
Also--why is it necessary to show that the additive inverse is unique?
Many thanks in advance.
 [/INST] An extended comment:


*

*If you want a proof verification it make sense that you number your equations so that they are easy to reference. You can use \$\tag{1}\$ in the equation code and reference it as \$(1)\$. 

*Start end end your LaTeX blocks wiht \$\$ and not with \$.


Lets make
$$
\begin{align}
a \cdot 0 + a \cdot 0 &= a \cdot 0 \tag{1.1}\\
a \cdot 0 + a \cdot 0 + (-a) \cdot 0 &= a \cdot 0 + (-a) \cdot 0 \tag{1.2}\\
a \cdot 0 &= 0 \tag{1.3}\\
\end{align}
$$
more precise, then you have
$$
\begin{align}
a \cdot 0 + a \cdot 0 &= a \cdot 0 \tag{2.1}\\
(a \cdot 0 + a \cdot 0 )+ (-a) \cdot 0 &= a \cdot 0 + (-a) \cdot 0 &\text{(you have to use parantheses)}\tag{2.2}\\
a \cdot 0 + (a \cdot 0 + (-a) \cdot 0) &= a \cdot 0 + (-a) \cdot 0 & \text{(by associativity of +)} \tag{2.3}\\
a \cdot 0 + ((a+(-a)) \cdot 0  &= ((a+(-a)) \cdot 0 &\text{(by distributive law)}\tag{2.4}\\
a \cdot 0 + 0 \cdot 0  &= 0 \cdot 0 &\text{(by law of inverse)}\tag{2.5}\\
a \cdot 0 +0&= 0 &  \text{(because }0\cdot0=0 \text{)}\tag{2.6}\\
a \cdot 0 &= 0& \text{0 is identity element of +} \tag{2.7}\\
\end{align}
$$
To get $(6)$  you use still an unproven identity: 
$$0\cdot 0=0 \tag{3.1}$$
It is simpler you proceed in the following way
$$
\begin{align}
a \cdot 0 + a \cdot 0 &= a \cdot 0 \tag{4.1}\\
(a \cdot 0 + a \cdot 0) + (-( a \cdot 0)) &= a \cdot 0 + (-( a \cdot 0))  &\text{(you have to use parantheses)}\tag{4.2}\\
a \cdot 0 + (a \cdot 0 + (-( a \cdot 0))) &= a \cdot 0 + (-( a \cdot 0))  & \text{(by associativity of +)}\tag{4.3}\\
a \cdot 0 + 0 &= 0 & \text{(inverse element)}\tag{4.4}\\
a \cdot 0 &= 0& \text{(0 is identity element of +)} \tag{4.5}\\
\end{align}
$$
The latter proof is shorter and complete. The first proof lacks the proof of 
$(3.1)$.
Edit
I forgot the most important part of my answer.
You showed that in a field with operations + and $\cdot$ we have 
$$-(-a)=a$$
by using the distributive law. 
But we have
$$
\begin{align}
a+(-a)&=0 &\text{right inverse of }a\tag{5.1}\\
(-(-a))+(-a)&=0& \text{left inverse of }(-a) \tag{5.2}\\
a+(-a)&=(-(-a))+(-a) &\tag{5.3}\\
(a+(-a))+a&=((-(-a))+(-a))+a & \tag{5.4}\\
a+((-a)+a)&=-(-a)+((-a)+a) & \text{associativity}\tag{5.5}\\
a+0&=-(-a)+0 & \text{left inverse}\tag{5.6} \\
a &= -(-a) & \text{identity}\tag{5.7} \\
\end{align}$$
So you do not need a $\cdot$ operation to show this property of the inverse of th $+$ operator. We can say therefore

If $(G,+)$ is a group and $-g$ the inverse of $g \in G$ then $-(-g)=g$

And from this immediately follows

If $(G,\cdot)$ is a group and $g^{-1}$ the inverse of $g \in G$ then $(g^{-1})^{-1}=g$

So from your Axioms follows:
$$-(-a))=a,\; (a^{-1})^{-1}=a\tag{6.1}$$
$(6.1)$ already follows from P1,P2,P3,P5,P6,P7
</s>