:: by Yuzhong Ding and Zhiyong Pang

::

:: Received August 28, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

definition

let X be BCI-algebra;

let x, y be Element of X;

let n be Nat;

ex b_{1} being Element of X ex f being sequence of the carrier of X st

( b_{1} = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) )

for b_{1}, b_{2} being Element of X st ex f being sequence of the carrier of X st

( b_{1} = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) ) & ex f being sequence of the carrier of X st

( b_{2} = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) ) holds

b_{1} = b_{2}

end;
let x, y be Element of X;

let n be Nat;

func (x,y) to_power n -> Element of X means :Def1: :: BCIALG_2:def 1

ex f being sequence of the carrier of X st

( it = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) );

existence ex f being sequence of the carrier of X st

( it = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) );

ex b

( b

f . (j + 1) = (f . j) \ y ) )

proof end;

uniqueness for b

( b

f . (j + 1) = (f . j) \ y ) ) & ex f being sequence of the carrier of X st

( b

f . (j + 1) = (f . j) \ y ) ) holds

b

proof end;

:: deftheorem Def1 defines to_power BCIALG_2:def 1 :

for X being BCI-algebra

for x, y being Element of X

for n being Nat

for b_{5} being Element of X holds

( b_{5} = (x,y) to_power n iff ex f being sequence of the carrier of X st

( b_{5} = f . n & f . 0 = x & ( for j being Nat st j < n holds

f . (j + 1) = (f . j) \ y ) ) );

for X being BCI-algebra

for x, y being Element of X

for n being Nat

for b

( b

( b

f . (j + 1) = (f . j) \ y ) ) );

theorem Th4: :: BCIALG_2:4

for X being BCI-algebra

for x, y being Element of X

for n being Nat holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y

for x, y being Element of X

for n being Nat holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y

proof end;

theorem Th5: :: BCIALG_2:5

for X being BCI-algebra

for x being Element of X

for n being Nat holds (x,(0. X)) to_power (n + 1) = x

for x being Element of X

for n being Nat holds (x,(0. X)) to_power (n + 1) = x

proof end;

theorem Th7: :: BCIALG_2:7

for X being BCI-algebra

for x, y, z being Element of X

for n being Nat holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n

for x, y, z being Element of X

for n being Nat holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n

proof end;

theorem :: BCIALG_2:8

for X being BCI-algebra

for x, y being Element of X

for n being Nat holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n

for x, y being Element of X

for n being Nat holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n

proof end;

theorem Th9: :: BCIALG_2:9

for X being BCI-algebra

for x being Element of X

for n being Nat holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n

for x being Element of X

for n being Nat holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n

proof end;

theorem Th10: :: BCIALG_2:10

for X being BCI-algebra

for x, y being Element of X

for n, m being Nat holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)

for x, y being Element of X

for n, m being Nat holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)

proof end;

theorem :: BCIALG_2:11

for X being BCI-algebra

for x, y, z being Element of X

for n, m being Nat holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n

for x, y, z being Element of X

for n, m being Nat holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n

proof end;

theorem Th12: :: BCIALG_2:12

for X being BCI-algebra

for x being Element of X

for n being Nat holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n

for x being Element of X

for n being Nat holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n

proof end;

theorem Th13: :: BCIALG_2:13

for X being BCI-algebra

for x being Element of X

for n, m being Nat holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)

for x being Element of X

for n, m being Nat holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)

proof end;

theorem :: BCIALG_2:14

for X being BCI-algebra

for x being Element of X

for n, m being Nat holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)

for x being Element of X

for n, m being Nat holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)

proof end;

theorem :: BCIALG_2:15

for X being BCI-algebra

for x being Element of X

for n, m being Nat holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)

for x being Element of X

for n, m being Nat holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)

proof end;

theorem :: BCIALG_2:16

for X being BCI-algebra

for x being Element of X

for n, m being Nat st ((0. X),x) to_power m = 0. X holds

((0. X),x) to_power (m * n) = 0. X

for x being Element of X

for n, m being Nat st ((0. X),x) to_power m = 0. X holds

((0. X),x) to_power (m * n) = 0. X

proof end;

theorem :: BCIALG_2:17

for X being BCI-algebra

for x, y being Element of X

for n being Nat st x \ y = x holds

(x,y) to_power n = x

for x, y being Element of X

for n being Nat st x \ y = x holds

(x,y) to_power n = x

proof end;

theorem :: BCIALG_2:18

for X being BCI-algebra

for x, y being Element of X

for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)

for x, y being Element of X

for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)

proof end;

::P20-P22

theorem :: BCIALG_2:19

for X being BCI-algebra

for x, y, z being Element of X

for n being Nat st x <= y holds

(x,z) to_power n <= (y,z) to_power n

for x, y, z being Element of X

for n being Nat st x <= y holds

(x,z) to_power n <= (y,z) to_power n

proof end;

theorem :: BCIALG_2:20

for X being BCI-algebra

for x, y, z being Element of X

for n being Nat st x <= y holds

(z,y) to_power n <= (z,x) to_power n

for x, y, z being Element of X

for n being Nat st x <= y holds

(z,y) to_power n <= (z,x) to_power n

proof end;

theorem :: BCIALG_2:21

for X being BCI-algebra

for x, y, z being Element of X

for n being Nat holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y

for x, y, z being Element of X

for n being Nat holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y

proof end;

theorem :: BCIALG_2:22

for X being BCI-algebra

for x, y being Element of X

for n being Nat holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x

for x, y being Element of X

for n being Nat holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x

proof end;

::P17 proposition 1.1.10

:: deftheorem Def2 defines positive BCIALG_2:def 2 :

for X being BCI-algebra

for a being Element of X holds

( a is positive iff 0. X <= a );

for X being BCI-algebra

for a being Element of X holds

( a is positive iff 0. X <= a );

:: deftheorem defines least BCIALG_2:def 3 :

for X being BCI-algebra

for a being Element of X holds

( a is least iff for x being Element of X holds a <= x );

for X being BCI-algebra

for a being Element of X holds

( a is least iff for x being Element of X holds a <= x );

:: deftheorem defines maximal BCIALG_2:def 4 :

for X being BCI-algebra

for a being Element of X holds

( a is maximal iff for x being Element of X st a <= x holds

x = a );

for X being BCI-algebra

for a being Element of X holds

( a is maximal iff for x being Element of X st a <= x holds

x = a );

:: deftheorem defines greatest BCIALG_2:def 5 :

for X being BCI-algebra

for a being Element of X holds

( a is greatest iff for x being Element of X holds x <= a );

for X being BCI-algebra

for a being Element of X holds

( a is greatest iff for x being Element of X holds x <= a );

Lm1: for X being BCI-algebra

for a being Element of X holds

( a is minimal iff for x being Element of X st x <= a holds

x = a )

by BCIALG_1:def 11;

Lm2: for X being BCI-algebra holds 0. X is positive

proof end;

registration
end;

Lm3: for X being BCI-algebra holds 0. X is minimal

by BCIALG_1:2;

registration
end;

theorem :: BCIALG_2:23

for X being BCI-algebra

for a being Element of X holds

( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )

for a being Element of X holds

( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )

proof end;

theorem :: BCIALG_2:24

for X being BCI-algebra

for x being Element of X holds

( x ` is minimal iff for y being Element of X st y <= x holds

x ` = y ` )

for x being Element of X holds

( x ` is minimal iff for y being Element of X st y <= x holds

x ` = y ` )

proof end;

theorem :: BCIALG_2:25

for X being BCI-algebra

for x being Element of X holds

( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )

for x being Element of X holds

( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )

proof end;

theorem :: BCIALG_2:27

for X being BCI-algebra st ex x being Element of X st x is greatest holds

for a being Element of X holds a is positive

for a being Element of X holds a is positive

proof end;

theorem Th30: :: BCIALG_2:30

for X being BCI-algebra

for a being Element of X holds

( a is minimal iff ex x being Element of X st a = x ` )

for a being Element of X holds

( a is minimal iff ex x being Element of X st a = x ` )

proof end;

:: p38

:: deftheorem defines nilpotent BCIALG_2:def 6 :

for X being BCI-algebra

for x being Element of X holds

( x is nilpotent iff ex k being non zero Nat st ((0. X),x) to_power k = 0. X );

for X being BCI-algebra

for x being Element of X holds

( x is nilpotent iff ex k being non zero Nat st ((0. X),x) to_power k = 0. X );

:: deftheorem defines nilpotent BCIALG_2:def 7 :

for X being BCI-algebra holds

( X is nilpotent iff for x being Element of X holds x is nilpotent );

for X being BCI-algebra holds

( X is nilpotent iff for x being Element of X holds x is nilpotent );

definition

let X be BCI-algebra;

let x be Element of X;

assume A1: x is nilpotent ;

ex b_{1} being non zero Nat st

( ((0. X),x) to_power b_{1} = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

b_{1} <= m ) )

for b_{1}, b_{2} being non zero Nat st ((0. X),x) to_power b_{1} = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

b_{1} <= m ) & ((0. X),x) to_power b_{2} = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

b_{2} <= m ) holds

b_{1} = b_{2}

;

end;
let x be Element of X;

assume A1: x is nilpotent ;

func ord x -> non zero Nat means :Def8: :: BCIALG_2:def 8

( ((0. X),x) to_power it = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

it <= m ) );

existence ( ((0. X),x) to_power it = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

it <= m ) );

ex b

( ((0. X),x) to_power b

b

proof end;

uniqueness for b

b

b

b

proof end;

correctness ;

:: deftheorem Def8 defines ord BCIALG_2:def 8 :

for X being BCI-algebra

for x being Element of X st x is nilpotent holds

for b_{3} being non zero Nat holds

( b_{3} = ord x iff ( ((0. X),x) to_power b_{3} = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds

b_{3} <= m ) ) );

for X being BCI-algebra

for x being Element of X st x is nilpotent holds

for b

( b

b

registration
end;

theorem :: BCIALG_2:31

for X being BCI-algebra

for x being Element of X holds

( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )

for x being Element of X holds

( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )

proof end;

theorem :: BCIALG_2:32

for X being BCI-algebra holds

( X is BCK-algebra iff for x being Element of X holds

( ord x = 1 & x is nilpotent ) )

( X is BCK-algebra iff for x being Element of X holds

( ord x = 1 & x is nilpotent ) )

proof end;

theorem :: BCIALG_2:33

for X being BCI-algebra

for x being Element of X

for n being Nat holds ((0. X),(x `)) to_power n is minimal

for x being Element of X

for n being Nat holds ((0. X),(x `)) to_power n is minimal

proof end;

definition

let X be BCI-algebra;

ex b_{1} being Equivalence_Relation of X st

for x, y, u, v being Element of X st [x,y] in b_{1} & [u,v] in b_{1} holds

[(x \ u),(y \ v)] in b_{1}

end;
mode Congruence of X -> Equivalence_Relation of X means :Def9: :: BCIALG_2:def 9

for x, y, u, v being Element of X st [x,y] in it & [u,v] in it holds

[(x \ u),(y \ v)] in it;

existence for x, y, u, v being Element of X st [x,y] in it & [u,v] in it holds

[(x \ u),(y \ v)] in it;

ex b

for x, y, u, v being Element of X st [x,y] in b

[(x \ u),(y \ v)] in b

proof end;

:: deftheorem Def9 defines Congruence BCIALG_2:def 9 :

for X being BCI-algebra

for b_{2} being Equivalence_Relation of X holds

( b_{2} is Congruence of X iff for x, y, u, v being Element of X st [x,y] in b_{2} & [u,v] in b_{2} holds

[(x \ u),(y \ v)] in b_{2} );

for X being BCI-algebra

for b

( b

[(x \ u),(y \ v)] in b

:: Left Congruence

definition

let X be BCI-algebra;

ex b_{1} being Equivalence_Relation of X st

for x, y being Element of X st [x,y] in b_{1} holds

for u being Element of X holds [(u \ x),(u \ y)] in b_{1}

end;
mode L-congruence of X -> Equivalence_Relation of X means :Def10: :: BCIALG_2:def 10

for x, y being Element of X st [x,y] in it holds

for u being Element of X holds [(u \ x),(u \ y)] in it;

existence for x, y being Element of X st [x,y] in it holds

for u being Element of X holds [(u \ x),(u \ y)] in it;

ex b

for x, y being Element of X st [x,y] in b

for u being Element of X holds [(u \ x),(u \ y)] in b

proof end;

:: deftheorem Def10 defines L-congruence BCIALG_2:def 10 :

for X being BCI-algebra

for b_{2} being Equivalence_Relation of X holds

( b_{2} is L-congruence of X iff for x, y being Element of X st [x,y] in b_{2} holds

for u being Element of X holds [(u \ x),(u \ y)] in b_{2} );

for X being BCI-algebra

for b

( b

for u being Element of X holds [(u \ x),(u \ y)] in b

:: Right Congruence

definition

let X be BCI-algebra;

ex b_{1} being Equivalence_Relation of X st

for x, y being Element of X st [x,y] in b_{1} holds

for u being Element of X holds [(x \ u),(y \ u)] in b_{1}

end;
mode R-congruence of X -> Equivalence_Relation of X means :Def11: :: BCIALG_2:def 11

for x, y being Element of X st [x,y] in it holds

for u being Element of X holds [(x \ u),(y \ u)] in it;

existence for x, y being Element of X st [x,y] in it holds

for u being Element of X holds [(x \ u),(y \ u)] in it;

ex b

for x, y being Element of X st [x,y] in b

for u being Element of X holds [(x \ u),(y \ u)] in b

proof end;

:: deftheorem Def11 defines R-congruence BCIALG_2:def 11 :

for X being BCI-algebra

for b_{2} being Equivalence_Relation of X holds

( b_{2} is R-congruence of X iff for x, y being Element of X st [x,y] in b_{2} holds

for u being Element of X holds [(x \ u),(y \ u)] in b_{2} );

for X being BCI-algebra

for b

( b

for u being Element of X holds [(x \ u),(y \ u)] in b

::Ideal Congruence

definition

let X be BCI-algebra;

let A be Ideal of X;

ex b_{1} being Relation of X st

for x, y being Element of X holds

( [x,y] in b_{1} iff ( x \ y in A & y \ x in A ) )

end;
let A be Ideal of X;

mode I-congruence of X,A -> Relation of X means :Def12: :: BCIALG_2:def 12

for x, y being Element of X holds

( [x,y] in it iff ( x \ y in A & y \ x in A ) );

existence for x, y being Element of X holds

( [x,y] in it iff ( x \ y in A & y \ x in A ) );

ex b

for x, y being Element of X holds

( [x,y] in b

proof end;

:: deftheorem Def12 defines I-congruence BCIALG_2:def 12 :

for X being BCI-algebra

for A being Ideal of X

for b_{3} being Relation of X holds

( b_{3} is I-congruence of X,A iff for x, y being Element of X holds

( [x,y] in b_{3} iff ( x \ y in A & y \ x in A ) ) );

for X being BCI-algebra

for A being Ideal of X

for b

( b

( [x,y] in b

registration

let X be BCI-algebra;

let A be Ideal of X;

coherence

for b_{1} being I-congruence of X,A holds

( b_{1} is total & b_{1} is symmetric & b_{1} is transitive )

end;
let A be Ideal of X;

coherence

for b

( b

proof end;

definition

let X be BCI-algebra;

ex b_{1} being set st

for A1 being set holds

( A1 in b_{1} iff ex I being Ideal of X st A1 is I-congruence of X,I )

for b_{1}, b_{2} being set st ( for A1 being set holds

( A1 in b_{1} iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds

( A1 in b_{2} iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) holds

b_{1} = b_{2}

end;
func IConSet X -> set means :Def13: :: BCIALG_2:def 13

for A1 being set holds

( A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I );

existence for A1 being set holds

( A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I );

ex b

for A1 being set holds

( A1 in b

proof end;

uniqueness for b

( A1 in b

( A1 in b

b

proof end;

:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :

for X being BCI-algebra

for b_{2} being set holds

( b_{2} = IConSet X iff for A1 being set holds

( A1 in b_{2} iff ex I being Ideal of X st A1 is I-congruence of X,I ) );

for X being BCI-algebra

for b

( b

( A1 in b

definition

let X be BCI-algebra;

coherence

{ R where R is Congruence of X : verum } is set ;

coherence

{ R where R is L-congruence of X : verum } is set ;

coherence

{ R where R is R-congruence of X : verum } is set ;

end;
coherence

{ R where R is Congruence of X : verum } is set ;

coherence

{ R where R is L-congruence of X : verum } is set ;

coherence

{ R where R is R-congruence of X : verum } is set ;

:: deftheorem defines ConSet BCIALG_2:def 14 :

for X being BCI-algebra holds ConSet X = { R where R is Congruence of X : verum } ;

for X being BCI-algebra holds ConSet X = { R where R is Congruence of X : verum } ;

:: deftheorem defines LConSet BCIALG_2:def 15 :

for X being BCI-algebra holds LConSet X = { R where R is L-congruence of X : verum } ;

for X being BCI-algebra holds LConSet X = { R where R is L-congruence of X : verum } ;

:: deftheorem defines RConSet BCIALG_2:def 16 :

for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;

for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;

:: huang-P58:P1.5.1

theorem Th36: :: BCIALG_2:36

for X being BCI-algebra

for R being Equivalence_Relation of X holds

( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )

for R being Equivalence_Relation of X holds

( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )

proof end;

theorem Th37: :: BCIALG_2:37

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I holds RI is Congruence of X

for I being Ideal of X

for RI being I-congruence of X,I holds RI is Congruence of X

proof end;

definition

let X be BCI-algebra;

let I be Ideal of X;

:: original: I-congruence

redefine mode I-congruence of X,I -> Congruence of X;

coherence

for b_{1} being I-congruence of X,I holds b_{1} is Congruence of X
by Th37;

end;
let I be Ideal of X;

:: original: I-congruence

redefine mode I-congruence of X,I -> Congruence of X;

coherence

for b

theorem Th38: :: BCIALG_2:38

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I

for I being Ideal of X

for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I

proof end;

theorem :: BCIALG_2:39

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I holds

( I is closed iff I = Class (RI,(0. X)) )

for I being Ideal of X

for RI being I-congruence of X,I holds

( I is closed iff I = Class (RI,(0. X)) )

proof end;

theorem Th40: :: BCIALG_2:40

for X being BCI-algebra

for x, y being Element of X

for E being Congruence of X st [x,y] in E holds

( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )

for x, y being Element of X

for E being Congruence of X st [x,y] in E holds

( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )

proof end;

theorem :: BCIALG_2:41

for X being BCI-algebra

for A, I being Ideal of X

for IA being I-congruence of X,A

for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds

IA = II

for A, I being Ideal of X

for IA being I-congruence of X,A

for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds

IA = II

proof end;

theorem Th42: :: BCIALG_2:42

for X being BCI-algebra

for x, y, u being Element of X

for k being Nat

for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds

[x,((y,u) to_power k)] in E

for x, y, u being Element of X

for k being Nat

for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds

[x,((y,u) to_power k)] in E

proof end;

theorem :: BCIALG_2:43

for X being BCI-algebra st ( for X being BCI-algebra

for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) holds

for E being Congruence of X

for I being Ideal of X st I = Class (E,(0. X)) holds

E is I-congruence of X,I

for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) holds

for E being Congruence of X

for I being Ideal of X st I = Class (E,(0. X)) holds

E is I-congruence of X,I

proof end;

theorem :: BCIALG_2:48

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds

E = RI

for I being Ideal of X

for RI being I-congruence of X,I

for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds

E = RI

proof end;

theorem :: BCIALG_2:49

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds

E = RI

for I being Ideal of X

for RI being I-congruence of X,I

for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds

E = RI

proof end;

registration
end;

definition

let X be BCI-algebra;

let E be Congruence of X;

ex b_{1} being BinOp of (Class E) st

for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b_{1} . (W1,W2) = Class (E,(x \ y))

for b_{1}, b_{2} being BinOp of (Class E) st ( for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b_{1} . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b_{2} . (W1,W2) = Class (E,(x \ y)) ) holds

b_{1} = b_{2}

end;
let E be Congruence of X;

func EqClaOp E -> BinOp of (Class E) means :Def17: :: BCIALG_2:def 17

for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

it . (W1,W2) = Class (E,(x \ y));

existence for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

it . (W1,W2) = Class (E,(x \ y));

ex b

for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b

proof end;

uniqueness for b

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b

b

proof end;

:: deftheorem Def17 defines EqClaOp BCIALG_2:def 17 :

for X being BCI-algebra

for E being Congruence of X

for b_{3} being BinOp of (Class E) holds

( b_{3} = EqClaOp E iff for W1, W2 being Element of Class E

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b_{3} . (W1,W2) = Class (E,(x \ y)) );

for X being BCI-algebra

for E being Congruence of X

for b

( b

for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds

b

definition

let X be BCI-algebra;

let E be Congruence of X;

coherence

Class (E,(0. X)) is Element of Class E by EQREL_1:def 3;

end;
let E be Congruence of X;

coherence

Class (E,(0. X)) is Element of Class E by EQREL_1:def 3;

:: deftheorem defines zeroEqC BCIALG_2:def 18 :

for X being BCI-algebra

for E being Congruence of X holds zeroEqC E = Class (E,(0. X));

for X being BCI-algebra

for E being Congruence of X holds zeroEqC E = Class (E,(0. X));

::Quotient Algebras

definition

let X be BCI-algebra;

let E be Congruence of X;

coherence

BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #) is BCIStr_0 ;

end;
let E be Congruence of X;

coherence

BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #) is BCIStr_0 ;

:: deftheorem defines ./. BCIALG_2:def 19 :

for X being BCI-algebra

for E being Congruence of X holds X ./. E = BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);

for X being BCI-algebra

for E being Congruence of X holds X ./. E = BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);

definition

let X be BCI-algebra;

let E be Congruence of X;

let W1, W2 be Element of Class E;

coherence

(EqClaOp E) . (W1,W2) is Element of Class E ;

end;
let E be Congruence of X;

let W1, W2 be Element of Class E;

coherence

(EqClaOp E) . (W1,W2) is Element of Class E ;

:: deftheorem defines \ BCIALG_2:def 20 :

for X being BCI-algebra

for E being Congruence of X

for W1, W2 being Element of Class E holds W1 \ W2 = (EqClaOp E) . (W1,W2);

for X being BCI-algebra

for E being Congruence of X

for W1, W2 being Element of Class E holds W1 \ W2 = (EqClaOp E) . (W1,W2);

theorem Th51: :: BCIALG_2:51

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I holds X ./. RI is BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I holds X ./. RI is BCI-algebra

proof end;

registration

let X be BCI-algebra;

let I be Ideal of X;

let RI be I-congruence of X,I;

coherence

( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) by Th51;

end;
let I be Ideal of X;

let RI be I-congruence of X,I;

coherence

( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) by Th51;

theorem :: BCIALG_2:52

for X being BCI-algebra

for I being Ideal of X st I = BCK-part X holds

for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra

for I being Ideal of X st I = BCK-part X holds

for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra

proof end;

:: n=0: it=x; n=1:it =x*y; n=2:it=(x*y)*y...