let X be BCI-Algebra_with_Condition(S); :: thesis: ( X is p-Semisimple implies for x, y being Element of X holds x * y = x \ ((0. X) \ y) )

assume A1: X is p-Semisimple ; :: thesis: for x, y being Element of X holds x * y = x \ ((0. X) \ y)

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

assume A1: X is p-Semisimple ; :: thesis: for x, y being Element of X holds x * y = x \ ((0. X) \ y)

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

proof

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

set z1 = x \ ((0. X) \ y);

set z2 = x * y;

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

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

.= ((0. X) \ y) \ ((0. X) \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then (x \ ((0. X) \ y)) \ x <= y ;

then x \ ((0. X) \ y) <= x * y by Lm2;

then A2: (x \ ((0. X) \ y)) \ (x * y) = 0. X ;

A3: for t being Element of X st t \ x <= y holds

t <= x \ ((0. X) \ y)

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

then (x * y) \ (x \ ((0. X) \ y)) = 0. X ;

hence x * y = x \ ((0. X) \ y) by A2, BCIALG_1:def 7; :: thesis: verum

end;set z1 = x \ ((0. X) \ y);

set z2 = x * y;

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

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

.= ((0. X) \ y) \ ((0. X) \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then (x \ ((0. X) \ y)) \ x <= y ;

then x \ ((0. X) \ y) <= x * y by Lm2;

then A2: (x \ ((0. X) \ y)) \ (x * y) = 0. X ;

A3: for t being Element of X st t \ x <= y holds

t <= x \ ((0. X) \ y)

proof

(x * y) \ x <= y
by Lm2;
let t be Element of X; :: thesis: ( t \ x <= y implies t <= x \ ((0. X) \ y) )

assume t \ x <= y ; :: thesis: t <= x \ ((0. X) \ y)

then (t \ x) \ y = 0. X ;

then t \ (x \ ((0. X) \ y)) = t \ (x \ ((0. X) \ (t \ x))) by A1, Th4

.= t \ (x \ (x \ (t \ (0. X)))) by A1, BCIALG_1:57

.= t \ (t \ (0. X)) by A1

.= t \ t by BCIALG_1:2

.= 0. X by BCIALG_1:def 5 ;

hence t <= x \ ((0. X) \ y) ; :: thesis: verum

end;assume t \ x <= y ; :: thesis: t <= x \ ((0. X) \ y)

then (t \ x) \ y = 0. X ;

then t \ (x \ ((0. X) \ y)) = t \ (x \ ((0. X) \ (t \ x))) by A1, Th4

.= t \ (x \ (x \ (t \ (0. X)))) by A1, BCIALG_1:57

.= t \ (t \ (0. X)) by A1

.= t \ t by BCIALG_1:2

.= 0. X by BCIALG_1:def 5 ;

hence t <= x \ ((0. X) \ y) ; :: thesis: verum

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

then (x * y) \ (x \ ((0. X) \ y)) = 0. X ;

hence x * y = x \ ((0. X) \ y) by A2, BCIALG_1:def 7; :: thesis: verum