begin
:: 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:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: 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 )
Lm2:
for X being BCI-algebra holds 0. X is positive
Lm3:
for X being BCI-algebra holds 0. X is minimal
theorem
theorem
theorem
theorem
theorem
theorem Th28:
theorem
theorem Th30:
:: 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 );
:: 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 );
:: 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 ) ) );
theorem
theorem
theorem
theorem
begin
definition
let X be
BCI-algebra;
mode Congruence of
X -> Equivalence_Relation of
X means :
Def9:
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 :
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 );
:: 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 );
:: 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 );
:: 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 ) ) );
:: 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 ) );
:: 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
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
theorem
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
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem
definition
let X be
BCI-algebra;
let E be
Congruence of
X;
func EqClaOp E -> BinOp of
(Class E) means :
Def17:
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 :
for X being BCI-algebra
for E being Congruence of X
for b3 being BinOp of (Class E) holds
( b3 = 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
b3 . (W1,W2) = Class (E,(x \ y)) );
:: 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));
:: 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) #);
:: 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);
theorem Th51:
theorem