:: Congruences and Quotient Algebras of {BCI}-algebras
:: by Yuzhong Ding and Zhiyong Pang
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines to_power BCIALG_2:def 1 :
theorem Th1: :: BCIALG_2:1
theorem Th2: :: BCIALG_2:2
theorem :: BCIALG_2:3
theorem Th4: :: BCIALG_2:4
theorem Th5: :: BCIALG_2:5
theorem Th6: :: BCIALG_2:6
theorem Th7: :: BCIALG_2:7
theorem :: BCIALG_2:8
theorem Th9: :: BCIALG_2:9
theorem Th10: :: BCIALG_2:10
theorem :: BCIALG_2:11
theorem Th12: :: BCIALG_2:12
theorem Th13: :: BCIALG_2:13
theorem :: BCIALG_2:14
theorem :: BCIALG_2:15
theorem :: BCIALG_2:16
theorem :: BCIALG_2:17
theorem :: BCIALG_2:18
theorem :: BCIALG_2:19
theorem :: BCIALG_2:20
theorem :: BCIALG_2:21
theorem :: BCIALG_2:22
:: deftheorem Def2 defines positive BCIALG_2:def 2 :
:: deftheorem defines least BCIALG_2:def 3 :
:: deftheorem Def4 defines maximal BCIALG_2:def 4 :
:: deftheorem Def5 defines greatest BCIALG_2:def 5 :
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 )
Lm2:
for X being BCI-algebra holds 0. X is positive
Lm3:
for X being BCI-algebra holds 0. X is minimal
theorem :: BCIALG_2:23
theorem :: BCIALG_2:24
theorem :: BCIALG_2:25
theorem :: BCIALG_2:26
theorem :: BCIALG_2:27
theorem Th28: :: BCIALG_2:28
theorem :: BCIALG_2:29
theorem Th30: :: BCIALG_2:30
:: deftheorem Def6 defines nilpotent BCIALG_2:def 6 :
:: deftheorem defines nilpotent BCIALG_2:def 7 :
:: deftheorem Def8 defines ord BCIALG_2:def 8 :
theorem :: BCIALG_2:31
theorem :: BCIALG_2:32
theorem :: BCIALG_2:33
theorem :: BCIALG_2:34
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
end;
:: deftheorem Def9 defines Congruence BCIALG_2:def 9 :
:: deftheorem Def10 defines L-congruence BCIALG_2:def 10 :
:: deftheorem Def11 defines R-congruence BCIALG_2:def 11 :
:: deftheorem Def12 defines I-congruence BCIALG_2:def 12 :
:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :
:: deftheorem defines ConSet BCIALG_2:def 14 :
:: deftheorem defines LConSet BCIALG_2:def 15 :
:: deftheorem defines RConSet BCIALG_2:def 16 :
theorem :: BCIALG_2:35
theorem Th36: :: BCIALG_2:36
theorem Th37: :: BCIALG_2:37
theorem Th38: :: BCIALG_2:38
theorem :: BCIALG_2:39
theorem Th40: :: BCIALG_2:40
theorem :: BCIALG_2:41
theorem Th42: :: BCIALG_2:42
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
Element of
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
theorem :: BCIALG_2:44
theorem Th45: :: BCIALG_2:45
theorem Th46: :: BCIALG_2:46
theorem :: BCIALG_2:47
theorem :: BCIALG_2:48
theorem :: BCIALG_2:49
theorem :: BCIALG_2:50
definition
let X be
BCI-algebra;
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
ex b1 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
b1 . W1,W2 = Class E,(x \ y)
uniqueness
for b1, b2 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
b1 . 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
b2 . W1,W2 = Class E,(x \ y) ) holds
b1 = b2
end;
:: deftheorem Def17 defines EqClaOp BCIALG_2:def 17 :
:: deftheorem defines zeroEqC BCIALG_2:def 18 :
:: deftheorem defines ./. BCIALG_2:def 19 :
:: deftheorem defines \ BCIALG_2:def 20 :
theorem Th51: :: BCIALG_2:51
theorem :: BCIALG_2:52