begin
definition
let G be non
empty BCIStr_0 ;
func BCI-power G -> Function of
[:the carrier of G,NAT :],the
carrier of
G means :
Def1:
for
x being
Element of
G holds
(
it . x,
0 = 0. G & ( for
n being
Element of
NAT holds
it . x,
(n + 1) = x \ ((it . x,n) ` ) ) );
existence
ex b1 being Function of [:the carrier of G,NAT :],the carrier of G st
for x being Element of G holds
( b1 . x,0 = 0. G & ( for n being Element of NAT holds b1 . x,(n + 1) = x \ ((b1 . x,n) ` ) ) )
uniqueness
for b1, b2 being Function of [:the carrier of G,NAT :],the carrier of G st ( for x being Element of G holds
( b1 . x,0 = 0. G & ( for n being Element of NAT holds b1 . x,(n + 1) = x \ ((b1 . x,n) ` ) ) ) ) & ( for x being Element of G holds
( b2 . x,0 = 0. G & ( for n being Element of NAT holds b2 . x,(n + 1) = x \ ((b2 . x,n) ` ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines BCI-power BCIALG_6:def 1 :
:: deftheorem Def2 defines |^ BCIALG_6:def 2 :
:: deftheorem defines |^ BCIALG_6:def 3 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
Lm1:
for X being BCI-algebra
for a being Element of AtomSet X
for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) ` )
Lm2:
for X being BCI-algebra
for a being Element of AtomSet X
for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n)
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
Lm3:
for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer st i > 0 & j > 0 holds
(a |^ i) \ (a |^ j) = a |^ (i - j)
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem Def4 defines finite-period BCIALG_6:def 4 :
theorem Th25:
:: deftheorem Def5 defines ord BCIALG_6:def 5 :
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem
begin
theorem Th34:
:: deftheorem Def6 defines multiplicative BCIALG_6:def 6 :
:: deftheorem defines isotonic BCIALG_6:def 7 :
:: deftheorem defines Ker BCIALG_6:def 8 :
theorem Th35:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem Th42:
theorem Th43:
theorem
theorem
theorem Th46:
theorem
theorem Th48:
theorem
:: deftheorem Def9 defines are_isomorphic BCIALG_6:def 9 :
:: deftheorem Def10 defines nat_hom BCIALG_6:def 10 :
begin
theorem
theorem Th51:
theorem
theorem
Lm4:
for X9, X being BCI-algebra
for H9 being SubAlgebra of X9
for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds
f is BCI-homomorphism of X,H9
begin
theorem
theorem Th55:
begin
:: deftheorem defines Union BCIALG_6:def 11 :
Lm5:
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for w being Element of Union G,RK ex a being Element of G st w in Class RK,a
definition
let X be
BCI-algebra;
let G be
SubAlgebra of
X;
let K be
closed Ideal of
X;
let RK be
I-congruence of
X,
K;
func HKOp G,
RK -> BinOp of
(Union G,RK) means :
Def12:
for
w1,
w2 being
Element of
Union G,
RK for
x,
y being
Element of
X st
w1 = x &
w2 = y holds
it . w1,
w2 = x \ y;
existence
ex b1 being BinOp of (Union G,RK) st
for w1, w2 being Element of Union G,RK
for x, y being Element of X st w1 = x & w2 = y holds
b1 . w1,w2 = x \ y
uniqueness
for b1, b2 being BinOp of (Union G,RK) st ( for w1, w2 being Element of Union G,RK
for x, y being Element of X st w1 = x & w2 = y holds
b1 . w1,w2 = x \ y ) & ( for w1, w2 being Element of Union G,RK
for x, y being Element of X st w1 = x & w2 = y holds
b2 . w1,w2 = x \ y ) holds
b1 = b2
end;
:: deftheorem Def12 defines HKOp BCIALG_6:def 12 :
:: deftheorem defines zeroHK BCIALG_6:def 13 :
definition
let X be
BCI-algebra;
let G be
SubAlgebra of
X;
let K be
closed Ideal of
X;
let RK be
I-congruence of
X,
K;
func HK G,
RK -> BCIStr_0 equals
BCIStr_0(#
(Union G,RK),
(HKOp G,RK),
(zeroHK G,RK) #);
coherence
BCIStr_0(# (Union G,RK),(HKOp G,RK),(zeroHK G,RK) #) is BCIStr_0
;
end;
:: deftheorem defines HK BCIALG_6:def 14 :
:: deftheorem defines \ BCIALG_6:def 15 :
theorem Th56:
theorem Th57:
theorem
theorem