Theorem TC-10. TC basis for double inversion in Abelian groups (2).

\{ \begin{matrix}TC \\ e · e = e \\ e · x = x · e \\ x · (x · y) = y \end{matrix} \} ⇒ \{(x · (((x · y) · z) · (y · e))) · (e · e) = z\}.

The conclusion is a single axiom for Abelian groups in terms of −x − y.

Proof (found by Otter 3.0.4 on gyro at 0.64 seconds).

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 4,3 e · e = e 5 e · x = x · e 6 x · (y · x) = y 8 (A · (((A · B) · C) · (B · e))) · (e · e) = C → □

9  (A · (((A · B) · C) · (B · e))) · e = C → □  [copy,8 :4]
11  x · y = y · x  [2,5,1,5,1]
19  (x · y) · x = y  [6 → 6]
36,35  (x · y) · y = x  [6 → 11, flip]
38,37  x · (x · y) = y  [11 → 6]
77,76  ((x · y) · z) · (x · u) = y · (z · u)  [2,6,6,6,19, flip]
132  C = C → □  [11 → 9 :77,38,36]
133  □  [132,1]