Prove properties of abelian groups

A group is a non-empty set G together with a binary operation on G, here denoted “\(\cdot\)”, that combines any two elements a and b of G to form an element of G, denoted \(a\cdot b\), such that the three requirements, known as “group axioms”, are satisfied: Associativity, left and right Identity element, left and right Inverse element. Further, the last two axioms can be relaxed by only requiring left identity and left inverse because right identity and right inverse can be deduced.

In a nutshell, a group satisfies the following properties:

\begin{gather}
\forall x. 1\cdot x=x & \label{left-identity} \\
\forall x. x^{-1}\cdot x=1 & \label{inverse} \\
\forall x \forall y \forall z. (x\cdot y)\cdot z=x\cdot (y\cdot z) & \label{associative}
\end{gather}

An abelian group is also called a commutative group. It has the property \(\forall x \forall y. x\cdot y=y\cdot z\). So, if there is a group, of which all elements has order 2, ie. \eqref{assumption}, is this group abelian?

\begin{equation}
\forall x. x\cdot x=1 \label{assumption}
\end{equation}

Lemma: \(\forall x \forall y. x\cdot y\cdot x=y^{-1}\cdot 1\).

Let’s prove the lemma.

\begin{align*}
& x\cdot y\cdot x &\\
=& 1\cdot x \cdot y \cdot x & \eqref{left-identity}\\
=& y^{-1}\cdot y \cdot x \cdot y \cdot x & \eqref{inverse}\\
=& y^{-1}\cdot (y \cdot x) \cdot (y \cdot x) & \eqref{associative}\\
=& y^{-1}\cdot 1 & \eqref{assumption}\\
\end{align*}

Q.E.D.

Now let’s prove the original statement.

\begin{align*}
& x\cdot x=1 & \eqref{assumption}\\
\Rightarrow & (x\cdot y) \cdot (x \cdot y) = 1 & \\
\Rightarrow & (x\cdot y) \cdot (x \cdot y) = x^{-1} \cdot x & \eqref{inverse} \\
\Rightarrow & x\cdot (y \cdot x) \cdot y = x^{-1} \cdot x & \eqref{associative} \\
\Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = x^{-1} \cdot x \cdot x & \\
\Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = x^{-1} \cdot 1 & \eqref{assumption} \\
\Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = y\cdot x \cdot y & \text{lemma} \\
\Rightarrow & y \cdot x\cdot (y \cdot x) \cdot y \cdot x = y \cdot y\cdot x \cdot y & \\
\Rightarrow & (y \cdot x) \cdot (y \cdot x) \cdot y \cdot x = y \cdot y\cdot x \cdot y & \eqref{associative} \\
\Rightarrow & 1 \cdot y \cdot x = 1 \cdot x \cdot y & \eqref{assumption} \\
\Rightarrow & y \cdot x = x \cdot y & \eqref{left-identity} \\
\end{align*}

We get the desired property. Q.E.D.