:: Ideals of BCI-Algebras and Their Properties
:: by Chenglong Wu and Yuzhong Ding
::
:: Received March 3, 2008
:: Copyright (c) 2008-2018 Association of Mizar Users

::P20
theorem :: BCIIDEAL:1
for X being BCI-algebra
for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
proof end;

theorem :: BCIIDEAL:2
for X being BCI-algebra
for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
proof end;

theorem :: BCIIDEAL:3
for X being BCI-algebra
for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
proof end;

theorem :: BCIIDEAL:4
for X being BCI-algebra
for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
proof end;

::P26
definition
let X be BCI-algebra;
let a be Element of X;
func initial_section a -> set equals :: BCIIDEAL:def 1
{ x where x is Element of X : x <= a } ;
coherence
{ x where x is Element of X : x <= a } is set
;
end;

:: deftheorem defines initial_section BCIIDEAL:def 1 :
for X being BCI-algebra
for a being Element of X holds initial_section a = { x where x is Element of X : x <= a } ;

theorem Th5: :: BCIIDEAL:5
for X being BCI-algebra
for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
proof end;

::P37
theorem :: BCIIDEAL:6
for X being BCI-algebra
for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof end;

theorem :: BCIIDEAL:7
for X being BCI-algebra
for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof end;

theorem :: BCIIDEAL:8
for X being BCI-algebra
for A being Ideal of X
for a being Element of A holds initial_section a c= A
proof end;

theorem :: BCIIDEAL:9
for X being BCI-algebra st AtomSet X is Ideal of X holds
for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
proof end;

theorem :: BCIIDEAL:10
for X being BCI-algebra st AtomSet X is Ideal of X holds
AtomSet X is closed Ideal of X
proof end;

::p47
definition
let X be BCI-algebra;
let I be Ideal of X;
attr I is positive means :: BCIIDEAL:def 2
for x being Element of I holds x is positive ;
end;

:: deftheorem defines positive BCIIDEAL:def 2 :
for X being BCI-algebra
for I being Ideal of X holds
( I is positive iff for x being Element of I holds x is positive );

::P48
theorem :: BCIIDEAL:11
for X being BCK-algebra
for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
proof end;

::P50
theorem :: BCIIDEAL:12
for X being associative BCI-algebra
for A being Ideal of X holds A is closed
proof end;

theorem :: BCIIDEAL:13
for X being BCI-algebra
for A being Ideal of X st X is quasi-associative holds
A is closed by ;

definition
let X be BCI-algebra;
let IT be Ideal of X;
attr IT is associative means :Def3: :: BCIIDEAL:def 3
( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) );
end;

:: deftheorem Def3 defines associative BCIIDEAL:def 3 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is associative iff ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) ) );

registration
let X be BCI-algebra;
cluster non empty associative for Ideal of X;
existence
ex b1 being Ideal of X st b1 is associative
proof end;
end;

definition
let X be BCI-algebra;
mode associative-ideal of X -> non empty Subset of X means :Def4: :: BCIIDEAL:def 4
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
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 & y \ z in b1 holds
x in b1 ) )
proof end;
end;

:: deftheorem Def4 defines associative-ideal BCIIDEAL:def 4 :
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is associative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x in b2 ) ) );

theorem :: BCIIDEAL:14
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X
proof end;

theorem Th15: :: BCIIDEAL:15
for X being BCI-algebra
for I being Ideal of X holds
( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
proof end;

theorem :: BCIIDEAL:16
for X being BCI-algebra
for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
proof end;

theorem :: BCIIDEAL:17
for X being BCI-algebra
for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
proof end;

definition
let X be BCI-algebra;
mode p-ideal of X -> non empty Subset of X means :Def5: :: BCIIDEAL:def 5
( 0. X in it & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in it & y in it holds
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 \ z) \ (y \ z) in b1 & y in b1 holds
x in b1 ) )
proof end;
end;

:: deftheorem Def5 defines p-ideal BCIIDEAL:def 5 :
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is p-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b2 & y in b2 holds
x in b2 ) ) );

theorem :: BCIIDEAL:18
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
proof end;

theorem Th19: :: BCIIDEAL:19
for X being BCI-algebra
for I being Ideal of X st I is p-ideal of X holds
BCK-part X c= I
proof end;

theorem :: BCIIDEAL:20
for X being BCI-algebra holds BCK-part X is p-ideal of X
proof end;

theorem Th21: :: BCIIDEAL:21
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
proof end;

theorem :: BCIIDEAL:22
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
proof end;

definition
let X be BCK-algebra;
let IT be Ideal of X;
attr IT is commutative means :Def6: :: BCIIDEAL:def 6
for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT;
end;

:: deftheorem Def6 defines commutative BCIIDEAL:def 6 :
for X being BCK-algebra
for IT being Ideal of X holds
( IT is commutative iff for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT );

registration
let X be BCK-algebra;
cluster non empty commutative for Ideal of X;
existence
ex b1 being Ideal of X st b1 is commutative
proof end;
end;

theorem :: BCIIDEAL:23
for X being BCK-algebra holds BCK-part X is commutative Ideal of X
proof end;

theorem :: BCIIDEAL:24
for X being BCK-algebra st X is p-Semisimple BCI-algebra holds
{(0. X)} is commutative Ideal of X
proof end;

Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part X
proof end;

theorem Th25: :: BCIIDEAL:25
for X being BCK-algebra holds BCK-part X = the carrier of X by Lm1;

theorem :: BCIIDEAL:26
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:27
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:28
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:29
for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:30
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:31
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
the carrier of X = BCK-part X
proof end;

theorem :: BCIIDEAL:32
for X being BCK-algebra holds the carrier of X is commutative Ideal of X
proof end;

theorem Th33: :: BCIIDEAL:33
for X being BCK-algebra
for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
proof end;

theorem Th34: :: BCIIDEAL:34
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds
A is commutative Ideal of X
proof end;

theorem Th35: :: BCIIDEAL:35
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
proof end;

theorem Th36: :: BCIIDEAL:36
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
proof end;

theorem Th37: :: BCIIDEAL:37
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
proof end;

theorem :: BCIIDEAL:38
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X ) by ;

theorem :: BCIIDEAL:39
for X being BCK-algebra
for I being Ideal of X
for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
proof end;

theorem :: BCIIDEAL:40
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) by ;

theorem :: BCIIDEAL:41
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) by ;

theorem :: BCIIDEAL:42
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) by ;

theorem :: BCIIDEAL:43
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) by ;

theorem :: BCIIDEAL:44
for X being BCK-algebra st {(0. X)} is commutative Ideal of X holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof end;

theorem :: BCIIDEAL:45
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) by ;

theorem :: BCIIDEAL:46
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) by ;

theorem :: BCIIDEAL:47
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) by ;

theorem :: BCIIDEAL:48
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) by ;

theorem :: BCIIDEAL:49
for X being BCK-algebra st ( for I being Ideal of X holds I is commutative Ideal of X ) holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof end;

definition
let X be BCK-algebra;
mode implicative-ideal of X -> non empty Subset of X means :Def7: :: BCIIDEAL:def 7
( 0. X in it & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in it & z in it holds
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 \ x)) \ z in b1 & z in b1 holds
x in b1 ) )
proof end;
end;

:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def 7 :
for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b2 & z in b2 holds
x in b2 ) ) );

theorem Th50: :: BCIIDEAL:50
for X being BCK-algebra
for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
proof end;

definition
let X be BCK-algebra;
mode positive-implicative-ideal of X -> non empty Subset of X means :Def8: :: BCIIDEAL:def 8
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
x \ z 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 & y \ z in b1 holds
x \ z in b1 ) )
proof end;
end;

:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def 8 :
for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is positive-implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x \ z in b2 ) ) );

theorem Th51: :: BCIIDEAL:51
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
proof end;

theorem Th52: :: BCIIDEAL:52
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
proof end;

theorem Th53: :: BCIIDEAL:53
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) holds
I is positive-implicative-ideal of X
proof end;

theorem :: BCIIDEAL:54
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
proof end;

theorem :: BCIIDEAL:55
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
proof end;

theorem :: BCIIDEAL:56
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X
proof end;

theorem :: BCIIDEAL:57
for X being BCK-algebra
for I being Ideal of X st I is implicative-ideal of X holds
( I is commutative Ideal of X & I is positive-implicative-ideal of X )
proof end;