Theorem TC-9. TC basis for double inversion in Abelian groups (1).

\{ \begin{matrix}TC \\ e · e = e \\ (x · e) · e = x \\ 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 1.04 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 6,5 (x · e) · e = x 7 x · (y · x) = y 9 (A · (((A · B) · C) · (B · e))) · (e · e) = C → □

10  (A · (((A · B) · C) · (B · e))) · e = C → □  [copy,9 :4]
30  e · x = x · e  [2,5,3,7,1 :4,6]
39,38  (x · y) · x = y  [7 → 7]
50  x · y = y · x  [2,30,5,30,5 :6,6]
55,54  (x · y) · y = x  [2,38,38,5,38 :6, flip]
180,179 (((x · y) · z) · u) · x = z · (u · y)  [2,7,38,50,7]
195  C = C → □  [50 → 10 :180,39,55]
196  □  [195,1]