let X be non empty BCIStr_1 ; :: thesis: ( X is commutative BCK-Algebra_with_Condition(S) iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) )
thus ( X is commutative BCK-Algebra_with_Condition(S) implies for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) :: thesis: ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) )
proof
assume A1: X is commutative BCK-Algebra_with_Condition(S) ; :: thesis: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) )
let x, y, z be Element of X; :: thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) )
(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def9;
then A2: (x \ z) \ (x \ y) = (y \ (y \ x)) \ z by A1, BCIALG_1:7
.= (y \ z) \ (y \ x) by A1, BCIALG_1:7 ;
(0. X) \ y = y `
.= 0. X by A1, BCIALG_1:def 8 ;
hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) by A1, A2, Th11, BCIALG_1:2; :: thesis: verum
end;
thus ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) :: thesis: verum
proof
assume A3: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ; :: thesis: X is commutative BCK-Algebra_with_Condition(S)
A4: for x, y being Element of X holds x \ (0. X) = x
proof
let x, y be Element of X; :: thesis: x \ (0. X) = x
(0. X) \ ((0. X) \ (0. X)) = 0. X by A3;
hence x \ (0. X) = x by A3; :: thesis: verum
end;
A5: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y
proof
let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y
then (x \ (0. X)) \ (0. X) = (y \ (0. X)) \ (0. X) by A3;
then x \ (0. X) = (y \ (0. X)) \ (0. X) by A4
.= y \ (0. X) by A4 ;
hence x = y \ (0. X) by A4
.= y by A4 ;
:: thesis: verum
end;
A6: for x being Element of X holds x \ x = 0. X
proof
let x be Element of X; :: thesis: x \ x = 0. X
x = x \ (0. X) by A4;
then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3
.= (0. X) \ ((0. X) \ x) by A4
.= 0. X by A3 ;
hence x \ x = 0. X ; :: thesis: verum
end;
A7: for x being Element of X holds (0. X) \ x = 0. X
proof
let x be Element of X; :: thesis: (0. X) \ x = 0. X
0. X = ((0. X) \ x) \ ((0. X) \ x) by A6
.= (0. X) \ x by A3 ;
hence (0. X) \ x = 0. X ; :: thesis: verum
end;
A8: for x, y, z being Element of X holds ((x \ y) \ (x \ z)) \ (z \ y) = 0. X
proof
let x, y, z be Element of X; :: thesis: ((x \ y) \ (x \ z)) \ (z \ y) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3
.= ((z \ y) \ (z \ x)) \ ((z \ y) \ (0. X)) by A4
.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3
.= (0. X) \ ((0. X) \ (z \ y)) by A7
.= 0. X by A7 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; :: thesis: verum
end;
A9: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof
let x, y, z be Element of X; :: thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X )
assume that
A10: x \ y = 0. X and
A11: y \ z = 0. X ; :: thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A8;
then (x \ z) \ (x \ y) = 0. X by A4, A11;
hence x \ z = 0. X by A4, A10; :: thesis: verum
end;
A12: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
proof
let x, y, z be Element of X; :: thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
(((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ z) = 0. X by A8;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ (z \ (0. X))) = 0. X by A4;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (((x \ (0. X)) \ (x \ z)) \ (z \ (0. X))) = 0. X by A4;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A8;
then A13: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A4;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A8;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A9, A13; :: thesis: verum
end;
A14: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ x)
x \ (x \ y) = (x \ ((0. X) \ y)) \ (x \ y) by A3
.= (y \ ((0. X) \ y)) \ (y \ x) by A3
.= y \ (y \ x) by A3 ;
hence x \ (x \ y) = y \ (y \ x) ; :: thesis: verum
end;
A15: for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof
let x, y, z be Element of X; :: thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) )
assume A16: x \ y = 0. X ; :: thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by A8;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A4, A16; :: thesis: verum
end;
A17: for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
proof
let x, y, z be Element of X; :: thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A8;
then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A15;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A15;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A4;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ ((x \ z) \ (0. X))) = 0. X by A4;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A8;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A4; :: thesis: verum
end;
for x being Element of X holds x ` = 0. X by A7;
hence X is commutative BCK-Algebra_with_Condition(S) by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7, BCIALG_1:def 8; :: thesis: verum
end;