:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

definition

let IT be non empty BCIStr_0 ;
attr IT is commutative means :Def1: :: BCIALG_3:def 1
for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);

end;

:: deftheorem Def1 defines commutative BCIALG_3:def 1 :
for IT being non empty BCIStr_0 holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

registration

cluster BCI-EXAMPLE -> commutative ;
coherence
BCI-EXAMPLE is commutative

proof end;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative BCIStr_0 ;
existence
ex b₁ being BCK-algebra st b₁ is commutative

proof end;

end;

theorem Th1: :: BCIALG_3:1

for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )

proof end;

theorem Th2: :: BCIALG_3:2

for X being BCK-algebra
for x, y being Element of X holds
( x \ (x \ y) <= y & x \ (x \ y) <= x )

proof end;

theorem Th3: :: BCIALG_3:3

for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

proof end;

theorem Th4: :: BCIALG_3:4

for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th5: :: BCIALG_3:5

for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )

proof end;

theorem Th6: :: BCIALG_3:6

for X being non empty BCIStr_0 holds
( X is commutative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )

proof end;

theorem :: BCIALG_3:7

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X st x \ y = x holds
y \ x = y

proof end;

theorem Th8: :: BCIALG_3:8

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x

proof end;

theorem :: BCIALG_3:9

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X )

proof end;

theorem :: BCIALG_3:10

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )

proof end;

theorem :: BCIALG_3:11

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;

definition

let X be BCI-algebra;
let a be Element of X;
attr a is being_greatest means :Def2: :: BCIALG_3:def 2
for x being Element of X holds x \ a = 0. X;
attr a is being_positive means :: BCIALG_3:def 3
(0. X) \ a = 0. X;

end;

:: deftheorem Def2 defines being_greatest BCIALG_3:def 2 :
for X being BCI-algebra
for a being Element of X holds
( a is being_greatest iff for x being Element of X holds x \ a = 0. X );

:: deftheorem defines being_positive BCIALG_3:def 3 :
for X being BCI-algebra
for a being Element of X holds
( a is being_positive iff (0. X) \ a = 0. X );

begin

definition

let IT be BCI-algebra;
attr IT is BCI-commutative means :Def4: :: BCIALG_3:def 4
for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x);
attr IT is BCI-weakly-commutative means :Def5: :: BCIALG_3:def 5
for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x);

end;

:: deftheorem Def4 defines BCI-commutative BCIALG_3:def 4 :
for IT being BCI-algebra holds
( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x) );

:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def 5 :
for IT being BCI-algebra holds
( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );

registration

cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative ;
coherence
( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative )

proof end;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative BCIStr_0 ;
existence
ex b₁ being BCI-algebra st
( b₁ is BCI-commutative & b₁ is BCI-weakly-commutative )

proof end;

end;

theorem :: BCIALG_3:12

for X being BCI-algebra st ex a being Element of X st a is being_greatest holds
X is BCK-algebra

proof end;

theorem :: BCIALG_3:13

for X being BCI-algebra st X is p-Semisimple holds
( X is BCI-commutative & X is BCI-weakly-commutative )

proof end;

theorem :: BCIALG_3:14

for X being commutative BCK-algebra holds
( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )

proof end;

theorem :: BCIALG_3:15

for X being BCK-algebra st X is BCI-weakly-commutative BCI-algebra holds
X is BCI-commutative

proof end;

theorem Th16: :: BCIALG_3:16

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th17: :: BCIALG_3:17

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )

proof end;

theorem :: BCIALG_3:18

for X being BCI-algebra holds
( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )

proof end;

theorem :: BCIALG_3:19

for X being non empty BCIStr_0 holds
( X is BCI-commutative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) )

proof end;

theorem :: BCIALG_3:20

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y )

proof end;

theorem :: BCIALG_3:21

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) )

proof end;

begin

definition

let IT be BCK-algebra;
attr IT is bounded means :: BCIALG_3:def 6
ex a being Element of IT st a is being_greatest ;

end;

:: deftheorem defines bounded BCIALG_3:def 6 :
for IT being BCK-algebra holds
( IT is bounded iff ex a being Element of IT st a is being_greatest );

registration

cluster BCI-EXAMPLE -> bounded ;
coherence
BCI-EXAMPLE is bounded

proof end;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded BCIStr_0 ;
existence
ex b₁ being BCK-algebra st
( b₁ is bounded & b₁ is commutative )

proof end;

end;

definition

let IT be bounded BCK-algebra;
attr IT is involutory means :Def7: :: BCIALG_3:def 7
for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x;

end;

:: deftheorem Def7 defines involutory BCIALG_3:def 7 :
for IT being bounded BCK-algebra holds
( IT is involutory iff for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x );

theorem Th22: :: BCIALG_3:22

for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )

proof end;

theorem Th23: :: BCIALG_3:23

for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) )

proof end;

theorem :: BCIALG_3:24

for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x )

proof end;

definition

let IT be BCK-algebra;
let a be Element of IT;
attr a is being_Iseki means :Def8: :: BCIALG_3:def 8
for x being Element of IT holds
( x \ a = 0. IT & a \ x = a );

end;

:: deftheorem Def8 defines being_Iseki BCIALG_3:def 8 :
for IT being BCK-algebra
for a being Element of IT holds
( a is being_Iseki iff for x being Element of IT holds
( x \ a = 0. IT & a \ x = a ) );

definition

let IT be BCK-algebra;
attr IT is Iseki_extension means :: BCIALG_3:def 9
ex a being Element of IT st a is being_Iseki ;

end;

:: deftheorem defines Iseki_extension BCIALG_3:def 9 :
for IT being BCK-algebra holds
( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );

registration

cluster BCI-EXAMPLE -> Iseki_extension ;
coherence
BCI-EXAMPLE is Iseki_extension

proof end;

end;

definition

let X be BCK-algebra;
mode Commutative-Ideal of X -> non empty Subset of X means :Def10: :: BCIALG_3:def 10
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & z in it holds
x \ (y \ (y \ x)) in it ) );
existence
ex b₁ being non empty Subset of X st
( 0. X in b₁ & ( for x, y, z being Element of X st (x \ y) \ z in b₁ & z in b₁ holds
x \ (y \ (y \ x)) in b₁ ) )

proof end;

end;

:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def 10 :
for X being BCK-algebra
for b₂ being non empty Subset of X holds
( b₂ is Commutative-Ideal of X iff ( 0. X in b₂ & ( for x, y, z being Element of X st (x \ y) \ z in b₂ & z in b₂ holds
x \ (y \ (y \ x)) in b₂ ) ) );

theorem :: BCIALG_3:25

for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT

proof end;

theorem Th26: :: BCIALG_3:26

for X being BCK-algebra
for IT being non empty Subset of X
for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X

proof end;

theorem :: BCIALG_3:27

for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT

proof end;

begin

definition

let IT be BCK-algebra;
attr IT is BCK-positive-implicative means :Def11: :: BCIALG_3:def 11
for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z);
attr IT is BCK-implicative means :Def12: :: BCIALG_3:def 12
for x, y being Element of IT holds x \ (y \ x) = x;

end;

:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def 11 :
for IT being BCK-algebra holds
( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );

:: deftheorem Def12 defines BCK-implicative BCIALG_3:def 12 :
for IT being BCK-algebra holds
( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

registration

cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative ;
coherence
( BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative )

proof end;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative BCIStr_0 ;
existence
ex b₁ being BCK-algebra st
( b₁ is Iseki_extension & b₁ is BCK-positive-implicative & b₁ is BCK-implicative & b₁ is bounded & b₁ is commutative )

proof end;

end;

theorem Th28: :: BCIALG_3:28

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )

proof end;

theorem Th29: :: BCIALG_3:29

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )

proof end;

theorem :: BCIALG_3:30

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )

proof end;

theorem :: BCIALG_3:31

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )

proof end;

theorem :: BCIALG_3:32

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )

proof end;

theorem :: BCIALG_3:33

for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )

proof end;

theorem Th34: :: BCIALG_3:34

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )

proof end;

theorem Th35: :: BCIALG_3:35

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )

proof end;

theorem :: BCIALG_3:36

for X being non empty BCIStr_0 holds
( X is BCK-implicative BCK-algebra 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) ) )

proof end;

Lm1: for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x

proof end;

theorem Th37: :: BCIALG_3:37

for X being bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )

proof end;

theorem :: BCIALG_3:38

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )

proof end;

theorem :: BCIALG_3:39

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th40: :: BCIALG_3:40

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )

proof end;

theorem :: BCIALG_3:41

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )

proof end;

theorem :: BCIALG_3:42

for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )

proof end;

theorem Th43: :: BCIALG_3:43

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )

proof end;

theorem :: BCIALG_3:44

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )

proof end;

theorem :: BCIALG_3:45

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )

proof end;

theorem Th46: :: BCIALG_3:46

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )

proof end;

theorem Th47: :: BCIALG_3:47

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )

proof end;

theorem :: BCIALG_3:48

for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )

proof end;