:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2012 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 for BCIStr_0 ;
existence
ex b1 being BCK-algebra st b1 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 for BCIStr_0 ;
existence
ex b1 being BCI-algebra st
( b1 is BCI-commutative & b1 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 for BCIStr_0 ;
existence
ex b1 being BCK-algebra st
( b1 is bounded & b1 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;

:: Commutative Ideal
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 b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & z in b1 holds
x \ (y \ (y \ x)) in b1 ) )
proof end;
end;

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

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 for BCIStr_0 ;
existence
ex b1 being BCK-algebra st
( b1 is Iseki_extension & b1 is BCK-positive-implicative & b1 is BCK-implicative & b1 is bounded & b1 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;