:: Congruences and Quotient Algebras of {BCI}-algebras
:: by Yuzhong Ding and Zhiyong Pang
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users

:: BCIALG_2 semantic presentation

definition
let X be BCI-algebra;
let x, y be Element of X;
let n be Element of NAT ;
func x,y to_power n -> Element of X means :Def1: :: BCIALG_2:def 1
 ex f being Function of NAT ,the carrier of X st
( it = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) );
existence
ex b1 being Element of X ex f being Function of NAT ,the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) )
proof end;
uniqueness
for b1, b2 being Element of X st ex f being Function of NAT ,the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being Function of NAT ,the carrier of X st
( b2 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) holds
b1 = b2
proof end;
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 Element of NAT
for b5 being Element of X holds
( b5 = x,y to_power n iff ex f being Function of NAT ,the carrier of X st
( b5 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) );

theorem Th1: :: BCIALG_2:1
for X being BCI-algebra
for x, y being Element of X holds x,y to_power 0 = x
proof end;

theorem Th2: :: BCIALG_2:2
for X being BCI-algebra
for x, y being Element of X holds x,y to_power 1 = x \ y
proof end;

theorem :: BCIALG_2:3
for X being BCI-algebra
for x, y being Element of X holds x,y to_power 2 = (x \ y) \ y
proof end;

theorem Th4: :: BCIALG_2:4
for X being BCI-algebra
for x, y being Element of X
for n being Element of 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 Element of NAT holds x,(0. X) to_power (n + 1) = x
proof end;

theorem Th6: :: BCIALG_2:6
for X being BCI-algebra
for n being Element of NAT holds (0. X),(0. X) to_power n = 0. X
proof end;

theorem Th7: :: BCIALG_2:7
for X being BCI-algebra
for x, y, z being Element of X
for n being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 m, n being Element of 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 m, n being Element of 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 m, n being Element of 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 Element of 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 Element of NAT holds (0. X),(x \ y) to_power n = ((0. X),x to_power n) \ ((0. X),y to_power n)
proof end;

theorem :: BCIALG_2:19
for X being BCI-algebra
for x, y, z being Element of X
for n being Element of 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 Element of 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, z, y being Element of X
for n being Element of 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 Element of NAT holds (x,(x \ y) to_power n),(y \ x) to_power n <= x
proof end;

notation
let X be BCI-algebra;
let a be Element of X;
synonym minimal a for atom a;
end;

definition
let X be BCI-algebra;
let a be Element of X;
attr a is positive means :Def2: :: BCIALG_2:def 2
 0. X <= a;
attr a is least means :: BCIALG_2:def 3
for x being Element of X holds a <= x;
attr a is maximal means :Def4: :: BCIALG_2:def 4
for x being Element of X st a <= x holds
x = a;
attr a is greatest means :Def5: :: BCIALG_2:def 5
for x being Element of X holds x <= a;
end;

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

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

:: deftheorem Def4 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 );

:: deftheorem Def5 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 );

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

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

registration
let X be BCI-algebra;
cluster positive Element of the carrier of X;
existence
ex b1 being Element of X st b1 is positive
proof end;
end;

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

registration
let X be BCI-algebra;
cluster 0. X -> minimal positive ;
coherence
( 0. X is positive & 0. X is minimal ) by Lm2, Lm3;
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 ` ) )
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 ` )
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 ` ) )
proof end;

theorem :: BCIALG_2:26
for X being BCI-algebra st 0. X is maximal holds
for a being Element of X holds a is minimal
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
proof end;

theorem Th28: :: BCIALG_2:28
for X being BCI-algebra
for x being Element of X holds x \ ((x ` ) ` ) is positive Element of X
proof end;

theorem :: BCIALG_2:29
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff (a ` ) ` = a )
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 ` )
proof end;

definition
let X be BCI-algebra;
let x be Element of X;
attr x is nilpotent means :Def6: :: BCIALG_2:def 6
 ex k being non empty Element of NAT st (0. X),x to_power k = 0. X;
end;

:: deftheorem Def6 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 empty Element of NAT st (0. X),x to_power k = 0. X );

definition
let X be BCI-algebra;
attr X is nilpotent means :: BCIALG_2:def 7
for x being Element of X holds x is nilpotent;
end;

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

definition
let X be BCI-algebra;
let x be Element of X;
assume A1: x is nilpotent ;
func ord x -> non empty Element of NAT means :Def8: :: BCIALG_2:def 8
( (0. X),x to_power it = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
it <= m ) );
existence
ex b1 being non empty Element of NAT st
( (0. X),x to_power b1 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
b1 <= m ) )
proof end;
uniqueness
for b1, b2 being non empty Element of NAT st (0. X),x to_power b1 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
b1 <= m ) & (0. X),x to_power b2 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
b2 <= m ) holds
b1 = b2
proof end;
correctness
;
end;

:: 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 b3 being non empty Element of NAT holds
( b3 = ord x iff ( (0. X),x to_power b3 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
b3 <= m ) ) );

registration
let X be BCI-algebra;
cluster 0. X -> nilpotent ;
coherence
0. X is nilpotent
proof end;
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 ) )
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 ) )
proof end;

theorem :: BCIALG_2:33
for X being BCI-algebra
for x being Element of X
for n being Element of NAT holds (0. X),(x ` ) to_power n is minimal
proof end;

theorem :: BCIALG_2:34
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
ord x = ord (x ` )
proof end;

definition
let X be BCI-algebra;
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
ex b1 being Equivalence_Relation of X st
for x, y, u, v being Element of X st [x,y] in b1 & [u,v] in b1 holds
[(x \ u),(y \ v)] in b1
proof end;
end;

:: deftheorem Def9 defines Congruence BCIALG_2:def 9 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is Congruence of X iff for x, y, u, v being Element of X st [x,y] in b2 & [u,v] in b2 holds
[(x \ u),(y \ v)] in b2 );

definition
let X be BCI-algebra;
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
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(u \ x),(u \ y)] in b1
proof end;
end;

:: deftheorem Def10 defines L-congruence BCIALG_2:def 10 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is L-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(u \ x),(u \ y)] in b2 );

definition
let X be BCI-algebra;
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
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(x \ u),(y \ u)] in b1
proof end;
end;

:: deftheorem Def11 defines R-congruence BCIALG_2:def 11 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is R-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(x \ u),(y \ u)] in b2 );

definition
let X be BCI-algebra;
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
ex b1 being Relation of X st
for x, y being Element of X holds
( [x,y] in b1 iff ( x \ y in A & y \ x in A ) )
proof end;
end;

:: deftheorem Def12 defines I-congruence BCIALG_2:def 12 :
for X being BCI-algebra
for A being Ideal of X
for b3 being Relation of X holds
( b3 is I-congruence of X,A iff for x, y being Element of X holds
( [x,y] in b3 iff ( x \ y in A & y \ x in A ) ) );

registration
let X be BCI-algebra;
let A be Ideal of X;
cluster -> symmetric transitive total I-congruence of X,A;
coherence
for b1 being I-congruence of X,A holds
( b1 is total & b1 is symmetric & b1 is transitive )
proof end;
end;

definition
let X be BCI-algebra;
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
ex b1 being set st
for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I )
proof end;
uniqueness
for b1, b2 being set st ( for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :
for X being BCI-algebra
for b2 being set holds
( b2 = IConSet X iff for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) );

definition
let X be BCI-algebra;
func ConSet X -> set equals :: BCIALG_2:def 14
{ R where R is Congruence of X : verum } ;
coherence
{ R where R is Congruence of X : verum } is set ;
func LConSet X -> set equals :: BCIALG_2:def 15
{ R where R is L-congruence of X : verum } ;
coherence
{ R where R is L-congruence of X : verum } is set ;
func RConSet X -> set equals :: BCIALG_2:def 16
{ R where R is R-congruence of X : verum } ;
coherence
{ R where R is R-congruence of X : verum } is set ;
end;

:: deftheorem defines ConSet BCIALG_2:def 14 :
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 } ;

:: deftheorem defines RConSet BCIALG_2:def 16 :
for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;

theorem :: BCIALG_2:35
for X being BCI-algebra
for E being Congruence of X holds Class E,(0. X) is closed Ideal of X
proof end;

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 ) )
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
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 b1 being I-congruence of X,I holds b1 is Congruence of X by