let X be BCI-algebra; :: thesis: for B being non empty Subset of X

for X being BCI-algebra st B = BCK-part X holds

( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

let B be non empty Subset of X; :: thesis: for X being BCI-algebra st B = BCK-part X holds

( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

let X be BCI-algebra; :: thesis: ( B = BCK-part X implies ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) )

assume A1: B = BCK-part X ; :: thesis: ( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

thus ( X is p-Semisimple BCI-algebra implies B = {(0. X)} ) :: thesis: ( B = {(0. X)} implies X is p-Semisimple BCI-algebra )

for x being Element of X holds (x `) ` = x

for X being BCI-algebra st B = BCK-part X holds

( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

let B be non empty Subset of X; :: thesis: for X being BCI-algebra st B = BCK-part X holds

( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

let X be BCI-algebra; :: thesis: ( B = BCK-part X implies ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) )

assume A1: B = BCK-part X ; :: thesis: ( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

thus ( X is p-Semisimple BCI-algebra implies B = {(0. X)} ) :: thesis: ( B = {(0. X)} implies X is p-Semisimple BCI-algebra )

proof

assume A6:
B = {(0. X)}
; :: thesis: X is p-Semisimple BCI-algebra
assume A2:
X is p-Semisimple BCI-algebra
; :: thesis: B = {(0. X)}

thus B c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= B

assume A5: x in {(0. X)} ; :: thesis: x in B

then reconsider x = x as Element of X by TARSKI:def 1;

x = 0. X by A5, TARSKI:def 1;

then x ` = 0. X by BCIALG_1:def 5;

then 0. X <= x ;

hence x in B by A1; :: thesis: verum

end;thus B c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in B )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in {(0. X)} )

assume A3: x in B ; :: thesis: x in {(0. X)}

then A4: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) by A1;

reconsider x = x as Element of X by A1, A3;

(x `) ` = x by A2, BCIALG_1:def 26;

then (0. X) ` = x by A4;

then x = 0. X by BCIALG_1:def 5;

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

end;assume A3: x in B ; :: thesis: x in {(0. X)}

then A4: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) by A1;

reconsider x = x as Element of X by A1, A3;

(x `) ` = x by A2, BCIALG_1:def 26;

then (0. X) ` = x by A4;

then x = 0. X by BCIALG_1:def 5;

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

assume A5: x in {(0. X)} ; :: thesis: x in B

then reconsider x = x as Element of X by TARSKI:def 1;

x = 0. X by A5, TARSKI:def 1;

then x ` = 0. X by BCIALG_1:def 5;

then 0. X <= x ;

hence x in B by A1; :: thesis: verum

for x being Element of X holds (x `) ` = x

proof

hence
X is p-Semisimple BCI-algebra
by BCIALG_1:54; :: thesis: verum
let x be Element of X; :: thesis: (x `) ` = x

(0. X) \ (x \ ((0. X) \ ((0. X) \ x))) = ((0. X),(x \ ((0. X) \ ((0. X) \ x)))) to_power 1 by BCIALG_2:2

.= (((0. X),x) to_power 1) \ (((0. X),((0. X) \ ((0. X) \ x))) to_power 1) by BCIALG_2:18

.= (((0. X),x) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:8

.= 0. X by BCIALG_1:def 5 ;

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

then x \ ((0. X) \ ((0. X) \ x)) in B by A1;

then A7: x \ ((0. X) \ ((0. X) \ x)) = 0. X by A6, TARSKI:def 1;

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

.= 0. X by BCIALG_1:def 5 ;

hence (x `) ` = x by A7, BCIALG_1:def 7; :: thesis: verum

end;(0. X) \ (x \ ((0. X) \ ((0. X) \ x))) = ((0. X),(x \ ((0. X) \ ((0. X) \ x)))) to_power 1 by BCIALG_2:2

.= (((0. X),x) to_power 1) \ (((0. X),((0. X) \ ((0. X) \ x))) to_power 1) by BCIALG_2:18

.= (((0. X),x) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:8

.= 0. X by BCIALG_1:def 5 ;

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

then x \ ((0. X) \ ((0. X) \ x)) in B by A1;

then A7: x \ ((0. X) \ ((0. X) \ x)) = 0. X by A6, TARSKI:def 1;

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

.= 0. X by BCIALG_1:def 5 ;

hence (x `) ` = x by A7, BCIALG_1:def 7; :: thesis: verum