:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008 Association of Mizar Users
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:
:: BCIALG_6:def 1
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 Th0: :: BCIALG_6:1
theorem Th1: :: BCIALG_6:2
theorem Th2: :: BCIALG_6:3
theorem Th3: :: BCIALG_6:4
theorem Th4: :: BCIALG_6:5
theorem :: BCIALG_6:6
theorem Th6: :: BCIALG_6:7
theorem :: BCIALG_6:8
theorem :: BCIALG_6:9
theorem Th9: :: BCIALG_6:10
theorem :: BCIALG_6:11
theorem :: BCIALG_6:12
theorem Th12: :: BCIALG_6:13
theorem Th13: :: BCIALG_6:14
Th14:
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) ` )
Th15:
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 Th16: :: BCIALG_6:15
theorem :: BCIALG_6:16
theorem Th17: :: BCIALG_6:17
theorem Th17b: :: BCIALG_6:18
theorem :: BCIALG_6:19
theorem Th18: :: BCIALG_6:20
theorem Th19: :: BCIALG_6:21
Lm20:
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 Th20: :: BCIALG_6:22
theorem Th21: :: BCIALG_6:23
theorem Th22: :: BCIALG_6:24
:: deftheorem Defx1 defines finite-period BCIALG_6:def 4 :
theorem Thx22: :: BCIALG_6:25
:: deftheorem Def8a defines ord BCIALG_6:def 5 :
theorem Th23: :: BCIALG_6:26
theorem :: BCIALG_6:27
theorem Th25: :: BCIALG_6:28
theorem Th26: :: BCIALG_6:29
theorem :: BCIALG_6:30
theorem :: BCIALG_6:31
theorem :: BCIALG_6:32
theorem :: BCIALG_6:33
theorem Lmth14: :: BCIALG_6:34
:: deftheorem Def0 defines multiplicative BCIALG_6:def 6 :
:: deftheorem defines isotonic BCIALG_6:def 7 :
:: deftheorem defines Ker BCIALG_6:def 8 :
theorem PR1621: :: BCIALG_6:35
theorem :: BCIALG_6:36
theorem :: BCIALG_6:37
theorem :: BCIALG_6:38
theorem :: BCIALG_6:39
theorem :: BCIALG_6:40
canceled;
theorem :: BCIALG_6:41
theorem PR1641: :: BCIALG_6:42
theorem Lm1653: :: BCIALG_6:43
theorem :: BCIALG_6:44
theorem :: BCIALG_6:45
theorem Thp167: :: BCIALG_6:46
theorem :: BCIALG_6:47
theorem PR1651: :: BCIALG_6:48
theorem :: BCIALG_6:49
:: deftheorem Def4 defines are_isomorphic BCIALG_6:def 9 :
:: deftheorem Def5 defines nat_hom BCIALG_6:def 10 :
theorem :: BCIALG_6:50
theorem Lm1662: :: BCIALG_6:51
theorem :: BCIALG_6:52
theorem :: BCIALG_6:53
Lmco1671:
for X', X being BCI-algebra
for H' being SubAlgebra of X'
for f being BCI-homomorphism of X,X' st the carrier of H' = rng f holds
f is BCI-homomorphism of X,H'
theorem :: BCIALG_6:54
theorem CO1672: :: BCIALG_6:55
:: deftheorem defines Union BCIALG_6:def 11 :
Lm168:
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 :
Def6:
:: BCIALG_6:def 12
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 Def6 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 :: BCIALG_6:def 14
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 Thz1: :: BCIALG_6:56
theorem Thxm1: :: BCIALG_6:57
theorem :: BCIALG_6:58
theorem :: BCIALG_6:59