let X be non empty BCIStr_0 ; :: thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )

thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) :: thesis: ( ( for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) :: thesis: verum

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )

thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) :: thesis: ( ( for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )

proof

thus
( ( for x, y, z being Element of X holds
assume A1:
X is associative BCI-algebra
; :: thesis: for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )

let x, y, z be Element of X; :: thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )

(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x) by A1, Def20;

then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x) by A1, Th7;

then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y) by A1, Th48;

then A2: (z \ y) \ ((y \ x) \ (z \ x)) = 0. X by A1, Th1;

((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z) by A1, Th48;

then ((y \ x) \ (z \ x)) \ (z \ y) = 0. X by A1, Def3;

hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A1, A2, Def7, Th2; :: thesis: verum

end;( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )

let x, y, z be Element of X; :: thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )

(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x) by A1, Def20;

then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x) by A1, Th7;

then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y) by A1, Th48;

then A2: (z \ y) \ ((y \ x) \ (z \ x)) = 0. X by A1, Th1;

((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z) by A1, Th48;

then ((y \ x) \ (z \ x)) \ (z \ y) = 0. X by A1, Def3;

hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A1, A2, Def7, Th2; :: thesis: verum

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) :: thesis: verum

proof

assume A3:
for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ; :: thesis: X is associative BCI-algebra

A4: for x, y being Element of X holds y \ x = x \ y

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

x = y

X is being_I by A5;

then reconsider Y = X as BCI-algebra by A6, A8, Th1;

Y is associative by A4, Th48;

hence X is associative BCI-algebra ; :: thesis: verum

end;( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ; :: thesis: X is associative BCI-algebra

A4: for x, y being Element of X holds y \ x = x \ y

proof

A5:
for a being Element of X holds a \ a = 0. X
let x, y be Element of X; :: thesis: y \ x = x \ y

(y \ (0. X)) \ (x \ (0. X)) = x \ y by A3;

then y \ (x \ (0. X)) = x \ y by A3;

hence y \ x = x \ y by A3; :: thesis: verum

end;(y \ (0. X)) \ (x \ (0. X)) = x \ y by A3;

then y \ (x \ (0. X)) = x \ y by A3;

hence y \ x = x \ y by A3; :: thesis: verum

proof

A6:
for x, y, z being Element of X holds
let a be Element of X; :: thesis: a \ a = 0. X

(a `) \ (a `) = (0. X) ` by A3;

then (a \ (0. X)) \ (a `) = (0. X) ` by A4;

then (a \ (0. X)) \ (a \ (0. X)) = (0. X) ` by A4;

then a \ a = (0. X) ` by A3;

hence a \ a = 0. X by A3; :: thesis: verum

end;(a `) \ (a `) = (0. X) ` by A3;

then (a \ (0. X)) \ (a `) = (0. X) ` by A4;

then (a \ (0. X)) \ (a \ (0. X)) = (0. X) ` by A4;

then a \ a = (0. X) ` by A3;

hence a \ a = 0. X by A3; :: thesis: verum

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

proof

for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
let x, y, z be Element of X; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

((x \ y) \ (x \ z)) \ (z \ y) = ((y \ x) \ (x \ z)) \ (z \ y) by A4

.= ((y \ x) \ (z \ x)) \ (z \ y) by A4

.= (z \ y) \ (z \ y) by A3 ;

hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A5; :: thesis: (x \ (x \ y)) \ y = 0. X

(x `) \ (y \ x) = y \ (0. X) by A3;

then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;

then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;

then x \ (x \ y) = y \ (0. X) by A3;

then (x \ (x \ y)) \ y = y \ y by A3;

hence (x \ (x \ y)) \ y = 0. X by A5; :: thesis: verum

end;((x \ y) \ (x \ z)) \ (z \ y) = ((y \ x) \ (x \ z)) \ (z \ y) by A4

.= ((y \ x) \ (z \ x)) \ (z \ y) by A4

.= (z \ y) \ (z \ y) by A3 ;

hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A5; :: thesis: (x \ (x \ y)) \ y = 0. X

(x `) \ (y \ x) = y \ (0. X) by A3;

then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;

then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;

then x \ (x \ y) = y \ (0. X) by A3;

then (x \ (x \ y)) \ y = y \ y by A3;

hence (x \ (x \ y)) \ y = 0. X by A5; :: thesis: verum

x = y

proof

then A8:
X is being_BCI-4
;
let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )

assume that

A7: x \ y = 0. X and

y \ x = 0. X ; :: thesis: x = y

(x `) \ (y \ x) = y \ (0. X) by A3;

then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;

then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;

then x \ (x \ y) = y \ (0. X) by A3;

then y = x \ (x \ y) by A3

.= x by A3, A7 ;

hence x = y ; :: thesis: verum

end;assume that

A7: x \ y = 0. X and

y \ x = 0. X ; :: thesis: x = y

(x `) \ (y \ x) = y \ (0. X) by A3;

then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;

then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;

then x \ (x \ y) = y \ (0. X) by A3;

then y = x \ (x \ y) by A3

.= x by A3, A7 ;

hence x = y ; :: thesis: verum

X is being_I by A5;

then reconsider Y = X as BCI-algebra by A6, A8, Th1;

Y is associative by A4, Th48;

hence X is associative BCI-algebra ; :: thesis: verum