Problem in abstract algebra concerning $x \div y := x \cdot y^{-1}$ Seth Warner, in his "Modern Algebra" (1965) sets the following question as exercise $7.7$ in the chapter introducing groups:
"Let $\div$ be a composition on [a set] $E$ and $e$ an element of $E$ such that for all $x, y, z \in E$ the equalities $1^\circ$ to $4^\circ$ hold.
(As follows:
$$1^\circ: \quad x \div x = e$$
$$2^\circ: \quad x \div e = x$$
$$3^\circ: \quad e \div (x \div y) = y \div x$$
$$4^\circ: \quad (x \div z) \div (y \div z) = x \div y$$)
Let $\cdot$ be the composition on $E$ defined as:
$$x \cdot y = x \div (e \div y)$$
Prove that $(E, \cdot)$ is a group."
(A previous part of this exercise has derived the above criteria by defining the $\div$ operation as $x \div y = x \cdot y^{-1}$ on a general group $(E, \cdot)$. This was easy to do. Hence it is of course clear that Warner is establishing that having posited a "divides" operation which fulfil the above criteria, one can then recover the original group operation.)
Closedness is trivial.
Proving the identity is easy, no bother to reproduce it here.
Proving the inverse of $x$ is $e \div x$ is straightforwardly done by evaluating $x \cdot (e \div x)$ and $(e \div x) \cdot x$ and showing you get $e$ both times, but directly solving the equation $x \cdot y = e$ and thence demonstrating that $y = e \div x$ is not so obvious.
The challenging task, which I have not achieved, is demonstrating associativity of $\cdot$.
Warner gives the following suggestion:
Show successively that:

*

*$(1): \quad (x \cdot z) \div (y \cdot z) = x \div y$

*$(2): \quad (x \div z) \cdot (z \div y) = x \div y$

*$(3): \quad x \div y = e$ implies that $x = y$

*$(4): \quad x \div z = y \div z$ implies that $x = y$

*$(5): \quad (x \cdot y) \div y = x$
EDIT: .... all of which have now been demonstrated, thanks to a comment froM Podiki which gave me the hint I needed.
Having done all that, apparently you go from there to demonstrate that $\cdot$ is associative. And again, that is something I have not been able to achieve.
I have tried a number of approaches, by manipulating the above expressions according to the rules given, but everything I do leads ever more complicated expressions which cannot be obviously simplified. The non-associative nature of $\div$ of course prevents the usual semigroup results from being used.
I did try directly evaluating $x \cdot (y \cdot z)$ and $(x \cdot y) \cdot z$ to see what would happen:
$$x \cdot (y \cdot z) = x \div (e \div (y \div (e \div z)))$$
$$(x \cdot y) \cdot z = (x \div (e \div y)) \div (e \div z)$$
and indeed, the expressions are not obviously simplifiable.

I have worked out the following:
$x \cdot (y \cdot z)$
$=((x \cdot y) \div y) \cdot (y \cdot z)$ ... from bullet point $5$
$=((x \cdot y) \div y) \cdot (y \div (e \div z))$ ... by definition of $\cdot$
$=(x \cdot y) \div (e \div z)$ ... from bullet point $(2)$
$=(x \cdot y) \cdot z$ ... by definition of $\cdot$
All achieved, without needing $(1)$ , $(3)$ or $(4)$, which makes you wonder why Warner suggests you derive them.
