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

begin

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;

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;

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;

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 );

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;

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

proof end;

begin

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 Ideal of X;
existence
ex b₁ being Ideal of X st b₁ 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 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₁ & y \ z in b₁ holds
x in b₁ ) )

proof end;

end;

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

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 b₁ being non empty Subset of X st
( 0. X in b₁ & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b₁ & y in b₁ holds
x in b₁ ) )

proof end;

end;

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

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;

begin

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 Ideal of X;
existence
ex b₁ being Ideal of X st b₁ 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

proof end;

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 )

proof end;

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) )

proof end;

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)) )

proof end;

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))) )

proof end;

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) )

proof end;

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) )

proof end;

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)) )

proof end;

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))) )

proof end;

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) )

proof end;

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;

begin

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 b₁ being non empty Subset of X st
( 0. X in b₁ & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b₁ & z in b₁ holds
x in b₁ ) )

proof end;

end;

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

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 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₁ & y \ z in b₁ holds
x \ z in b₁ ) )

proof end;

end;

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

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;