let X be BCK-algebra; :: thesis: ( X is p-Semisimple BCI-algebra implies {(0. X)} is commutative Ideal of X )

set X1 = {(0. X)};

A1: {(0. X)} c= the carrier of X

x in {(0. X)}

then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def 18;

assume A3: X is p-Semisimple BCI-algebra ; :: thesis: {(0. X)} is commutative Ideal of X

for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds

x \ (y \ (y \ x)) in X1

set X1 = {(0. X)};

A1: {(0. X)} c= the carrier of X

proof

A2:
for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in {(0. X)} or xx in the carrier of X )

assume xx in {(0. X)} ; :: thesis: xx in the carrier of X

then xx = 0. X by TARSKI:def 1;

hence xx in the carrier of X ; :: thesis: verum

end;assume xx in {(0. X)} ; :: thesis: xx in the carrier of X

then xx = 0. X by TARSKI:def 1;

hence xx in the carrier of X ; :: thesis: verum

x in {(0. X)}

proof

0. X in {(0. X)}
by TARSKI:def 1;
set X1 = {(0. X)};

let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )

assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}

then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;

then x = 0. X by BCIALG_1:2;

hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )

assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}

then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;

then x = 0. X by BCIALG_1:2;

hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def 18;

assume A3: X is p-Semisimple BCI-algebra ; :: thesis: {(0. X)} is commutative Ideal of X

for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds

x \ (y \ (y \ x)) in X1

proof

hence
{(0. X)} is commutative Ideal of X
by Def6; :: thesis: verum
let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in X1 & z in X1 implies x \ (y \ (y \ x)) in X1 )

assume ( (x \ y) \ z in X1 & z in X1 ) ; :: thesis: x \ (y \ (y \ x)) in X1

then ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def 1;

then A4: x \ y = 0. X by BCIALG_1:2;

y is atom by A3, BCIALG_1:52;

then x = y by A4;

then x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def 5;

then x \ (y \ (y \ x)) = x \ x by BCIALG_1:2;

then x \ (y \ (y \ x)) = 0. X by BCIALG_1:def 5;

hence x \ (y \ (y \ x)) in X1 by TARSKI:def 1; :: thesis: verum

end;assume ( (x \ y) \ z in X1 & z in X1 ) ; :: thesis: x \ (y \ (y \ x)) in X1

then ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def 1;

then A4: x \ y = 0. X by BCIALG_1:2;

y is atom by A3, BCIALG_1:52;

then x = y by A4;

then x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def 5;

then x \ (y \ (y \ x)) = x \ x by BCIALG_1:2;

then x \ (y \ (y \ x)) = 0. X by BCIALG_1:def 5;

hence x \ (y \ (y \ x)) in X1 by TARSKI:def 1; :: thesis: verum