let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies ( X is BCI-commutative & X is BCI-weakly-commutative ) )

assume A1: X is p-Semisimple ; :: thesis: ( X is BCI-commutative & X is BCI-weakly-commutative )

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

x = y \ (y \ x) by A1;

hence ( X is BCI-commutative & X is BCI-weakly-commutative ) by A2; :: thesis: verum

assume A1: X is p-Semisimple ; :: thesis: ( X is BCI-commutative & X is BCI-weakly-commutative )

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

proof

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

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

.= ((0. X) \ x) \ ((0. X) \ y) by A1, BCIALG_1:64

.= (y \ x) \ ((0. X) \ (0. X)) by A1, BCIALG_1:58

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

.= y \ x by BCIALG_1:2 ;

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

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

.= ((0. X) \ x) \ ((0. X) \ y) by A1, BCIALG_1:64

.= (y \ x) \ ((0. X) \ (0. X)) by A1, BCIALG_1:58

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

.= y \ x by BCIALG_1:2 ;

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

x = y \ (y \ x) by A1;

hence ( X is BCI-commutative & X is BCI-weakly-commutative ) by A2; :: thesis: verum