let X be BCI-algebra; :: thesis: ( X is alternative iff X is associative )
thus
( X is alternative implies X is associative )
:: thesis: ( X is associative implies X is alternative )proof
assume A1:
X is
alternative
;
:: thesis: X is associative
for
x,
y,
z being
Element of
X holds
(x \ y) \ z = x \ (y \ z)
proof
let x,
y,
z be
Element of
X;
:: thesis: (x \ y) \ z = x \ (y \ z)
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z
by Th7;
then
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ (x \ (y \ z))) \ y) \ z
by Th7;
then
((x \ y) \ z) \ (x \ (y \ z)) = (((x \ x) \ (y \ z)) \ y) \ z
by A1, Def27;
then
((x \ y) \ z) \ (x \ (y \ z)) = (((y \ z) ` ) \ y) \ z
by Def5;
then
((x \ y) \ z) \ (x \ (y \ z)) = ((y \ z) \ y) \ z
by A1, Th76;
then
((x \ y) \ z) \ (x \ (y \ z)) = ((y \ y) \ z) \ z
by Th7;
then
((x \ y) \ z) \ (x \ (y \ z)) = (z ` ) \ z
by Def5;
then A2:
((x \ y) \ z) \ (x \ (y \ z)) = 0. X
by A1, Th76;
A3:
(x \ (y \ z)) \ ((x \ y) \ z) =
(((x \ y) \ y) \ (y \ z)) \ ((x \ y) \ z)
by A1, Th76
.=
(((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)
by Th7
;
(((x \ y) \ y) \ ((x \ y) \ z)) \ (z \ y) = 0. X
by Th1;
then
((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ y) \ (y \ z)) = 0. X
by Th4;
then
((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ (y \ z)) \ y) = 0. X
by Th7;
then
((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z ` ) \ (y \ z)) \ y) = 0. X
by A1, Th76;
then
((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z ` ) \ (y \ z)) \ (y ` )) = 0. X
by A1, Th76;
then
((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X
by Def3;
then
(x \ (y \ z)) \ ((x \ y) \ z) = 0. X
by A3, Th2;
hence
(x \ y) \ z = x \ (y \ z)
by A2, Def7;
:: thesis: verum
end;
hence
X is
associative
by Def20;
:: thesis: verum
end;
assume
X is associative
; :: thesis: X is alternative
then
for x, y being Element of X holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) )
by Def20;
hence
X is alternative
by Def27; :: thesis: verum