BCIALG_6: {BCI}-Homomorphisms

:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008 Association of Mizar Users

begin

definition

let D be set ;
let f be Function of NAT ,D;
let n be Nat;
:: original: .
redefine func f . n -> Element of D;
coherence

proof end;

end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines BCI-power BCIALG_6:def 1 :

definition

let X be BCI-algebra;
let i be Integer;
let x be Element of X;
func x |^ i -> Element of X equals :Def2: :: BCIALG_6:def 2
(BCI-power X) . x,(abs i) if 0 <= i
otherwise (BCI-power X) . (x ` ),(abs i);
correctness ;

end;

:: deftheorem Def2 defines |^ BCIALG_6:def 2 :

definition

let X be BCI-algebra;
let n be Nat;
let x be Element of X;
redefine func x |^ n equals :: BCIALG_6:def 3
(BCI-power X) . x,n;
compatibility

proof end;

end;

:: deftheorem defines |^ BCIALG_6:def 3 :

theorem Th1: :: BCIALG_6:1

for X being BCI-algebra
for x being Element of X
for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a)

proof end;

theorem Th2: :: BCIALG_6:2

for X being BCI-algebra
for x being Element of X
for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) ` )

proof end;

theorem Th3: :: BCIALG_6:3

for X being BCI-algebra
for x being Element of X holds x |^ 0 = 0. X by Def1;

theorem Th4: :: BCIALG_6:4

for X being BCI-algebra
for x being Element of X holds x |^ 1 = x

proof end;

theorem Th5: :: BCIALG_6:5

for X being BCI-algebra
for x being Element of X holds x |^ (- 1) = x `

proof end;

theorem :: BCIALG_6:6

for X being BCI-algebra
for x being Element of X holds x |^ 2 = x \ (x ` )

proof end;

theorem Th7: :: BCIALG_6:7

for X being BCI-algebra
for n being Nat holds (0. X) |^ n = 0. X

proof end;

theorem :: BCIALG_6:8

for X being BCI-algebra
for a being Element of AtomSet X holds (a |^ (- 1)) |^ (- 1) = a

proof end;

theorem :: BCIALG_6:9

for X being BCI-algebra
for x being Element of X
for n being Nat holds x |^ (- n) = ((x ` ) ` ) |^ (- n)

proof end;

theorem Th10: :: BCIALG_6:10

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a ` ) |^ n = a |^ (- n)

proof end;

theorem :: BCIALG_6:11

for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X & n >= 1 holds
x |^ n = x

proof end;

theorem :: BCIALG_6:12

for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X holds
x |^ (- n) = 0. X

proof end;

theorem Th13: :: BCIALG_6:13

for X being BCI-algebra
for a being Element of AtomSet X
for i being Integer holds a |^ i in AtomSet X

proof end;

theorem Th14: :: BCIALG_6:14

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) ` ) \ a

proof end;

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) ` )

proof end;

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)

proof end;

theorem Th15: :: BCIALG_6:15

for X being BCI-algebra
for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n)

proof end;

theorem :: BCIALG_6:16

for X being BCI-algebra
for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n))

proof end;

theorem Th17: :: BCIALG_6:17

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a ` ) |^ n = (a |^ n) `

proof end;

theorem Th18: :: BCIALG_6:18

for X being BCI-algebra
for x being Element of X
for n being Nat holds (x ` ) |^ n = (x |^ n) `

proof end;

theorem :: BCIALG_6:19

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a ` ) |^ (- n) = (a |^ (- n)) `

proof end;

theorem Th20: :: BCIALG_6:20

for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X
for n being Nat st a = ((x ` ) ` ) |^ n holds
x |^ n in BranchV a

proof end;

theorem Th21: :: BCIALG_6:21

for X being BCI-algebra
for x being Element of X
for n being Nat holds (x |^ n) ` = (((x ` ) ` ) |^ n) `

proof end;

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)

proof end;

theorem Th22: :: BCIALG_6:22

for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)

proof end;

theorem Th23: :: BCIALG_6:23

for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j)

proof end;

theorem Th24: :: BCIALG_6:24

for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds a |^ (i + j) = (a |^ i) \ ((a |^ j) ` )

proof end;

definition

let X be BCI-algebra;
let x be Element of X;
attr x is finite-period means :Def4: :: BCIALG_6:def 4
ex n being Element of NAT st
( n <> 0 & x |^ n in BCK-part X );

end;

:: deftheorem Def4 defines finite-period BCIALG_6:def 4 :

theorem Th25: :: BCIALG_6:25

for X being BCI-algebra
for x being Element of X st x is finite-period holds
(x ` ) ` is finite-period

proof end;

definition

let X be BCI-algebra;
let x be Element of X;
assume A1: x is finite-period ;
func ord x -> Element of NAT means :Def5: :: BCIALG_6:def 5
( x |^ it in BCK-part X & it <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
it <= m ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ord BCIALG_6:def 5 :

theorem Th26: :: BCIALG_6:26

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat st a is finite-period & ord a = n holds
a |^ n = 0. X

proof end;

theorem :: BCIALG_6:27

for X being BCI-algebra holds
( X is BCK-algebra iff for x being Element of X holds
( x is finite-period & ord x = 1 ) )

proof end;

theorem Th28: :: BCIALG_6:28

for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds
ord x = ord a

proof end;

theorem Th29: :: BCIALG_6:29

for X being BCI-algebra
for x being Element of X
for n, m being Nat st x is finite-period & ord x = n holds
( x |^ m in BCK-part X iff n divides m )

proof end;

theorem :: BCIALG_6:30

for X being BCI-algebra
for x being Element of X
for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds
ord (x |^ m) = n div (m gcd n)

proof end;

theorem :: BCIALG_6:31

for X being BCI-algebra
for x being Element of X st x is finite-period & x ` is finite-period holds
ord x = ord (x ` )

proof end;

theorem :: BCIALG_6:32

for X being BCI-algebra
for x, y being Element of X
for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds
ord (x \ y) = 1

proof end;

theorem :: BCIALG_6:33

for X being BCI-algebra
for x, y being Element of X
for a, b being Element of AtomSet X st a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b holds
ord (a \ b) divides (ord x) lcm (ord y)

proof end;

begin

theorem Th34: :: BCIALG_6:34

for X being BCI-algebra
for Y being SubAlgebra of X
for x, y being Element of X
for x', y' being Element of Y st x = x' & y = y' holds
x \ y = x' \ y'

proof end;

definition

let X, X' be non empty BCIStr_0 ;
let f be Function of X,X';
attr f is multiplicative means :Def6: :: BCIALG_6:def 6
for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b);

end;

:: deftheorem Def6 defines multiplicative BCIALG_6:def 6 :

registration

let X, X' be BCI-algebra;
cluster multiplicative Element of bool [:the carrier of X,the carrier of X':];
existence

proof end;

end;

definition

let X, X' be BCI-algebra;
mode BCI-homomorphism of X,X' is multiplicative Function of X,X';

end;

definition

let X, X' be BCI-algebra;
let f be BCI-homomorphism of X,X';
attr f is isotonic means :: BCIALG_6:def 7
for x, y being Element of X st x <= y holds
f . x <= f . y;

end;

:: deftheorem defines isotonic BCIALG_6:def 7 :

definition

let X be BCI-algebra;
mode Endomorphism of X is BCI-homomorphism of X,X;

end;

definition

let X, X' be BCI-algebra;
let f be BCI-homomorphism of X,X';
func Ker f -> set equals :: BCIALG_6:def 8
{ x where x is Element of X : f . x = 0. X' } ;
coherence ;

end;

:: deftheorem defines Ker BCIALG_6:def 8 :

theorem Th35: :: BCIALG_6:35

for X, X' being BCI-algebra
for f being BCI-homomorphism of X,X' holds f . (0. X) = 0. X'

proof end;

registration

let X, X' be BCI-algebra;
let f be BCI-homomorphism of X,X';
cluster Ker f -> non empty ;
coherence

proof end;

end;

theorem :: BCIALG_6:36

for X, X' being BCI-algebra
for x, y being Element of X
for f being BCI-homomorphism of X,X' st x <= y holds
f . x <= f . y

proof end;

theorem :: BCIALG_6:37

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X' holds
( f is one-to-one iff Ker f = {(0. X)} )

proof end;

theorem :: BCIALG_6:38

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X'
for g being BCI-homomorphism of X',X st f is bijective & g = f " holds
g is bijective

proof end;

theorem :: BCIALG_6:39

for X', X, Y being BCI-algebra
for f being BCI-homomorphism of X,X'
for h being BCI-homomorphism of X',Y holds h * f is BCI-homomorphism of X,Y

proof end;

theorem :: BCIALG_6:40

canceled;

theorem :: BCIALG_6:41

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X'
for Z being SubAlgebra of X' st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z

proof end;

theorem Th42: :: BCIALG_6:42

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X' holds Ker f is closed Ideal of X

proof end;

registration

let X, X' be BCI-algebra;
let f be BCI-homomorphism of X,X';
cluster Ker f -> closed Ideal of X;
coherence by Th42;

end;

theorem Th43: :: BCIALG_6:43

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X' st f is onto holds
for c being Element of X' ex x being Element of X st c = f . x

proof end;

theorem :: BCIALG_6:44

for X', X being BCI-algebra
for f being BCI-homomorphism of X,X'
for a being Element of X st a is atom holds
f . a is atom

proof end;

theorem :: BCIALG_6:45

for X, X' being BCI-algebra
for f being BCI-homomorphism of X,X'
for a being Element of AtomSet X
for b being Element of AtomSet X' st b = f . a holds
f .: (BranchV a) c= BranchV b

proof end;

theorem Th46: :: BCIALG_6:46

for X', X being BCI-algebra
for A' being non empty Subset of X'
for f being BCI-homomorphism of X,X' st A' is Ideal of X' holds
f " A' is Ideal of X

proof end;

theorem :: BCIALG_6:47

for X', X being BCI-algebra
for A' being non empty Subset of X'
for f being BCI-homomorphism of X,X' st A' is closed Ideal of X' holds
f " A' is closed Ideal of X

proof end;

theorem Th48: :: BCIALG_6:48

for X, X' being BCI-algebra
for I being Ideal of X
for f being BCI-homomorphism of X,X' st f is onto holds
f .: I is Ideal of X'

proof end;

theorem :: BCIALG_6:49

for X, X' being BCI-algebra
for CI being closed Ideal of X
for f being BCI-homomorphism of X,X' st f is onto holds
f .: CI is closed Ideal of X'

proof end;

definition

let X, X' be BCI-algebra;
pred X,X' are_isomorphic means :Def9: :: BCIALG_6:def 9
ex f being BCI-homomorphism of X,X' st f is bijective ;

end;

:: deftheorem Def9 defines are_isomorphic BCIALG_6:def 9 :

registration

let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
cluster X ./. RI -> strict being_B being_C being_I being_BCI-4 ;
coherence ;

end;

definition

let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
func nat_hom RI -> BCI-homomorphism of X,(X ./. RI) means :Def10: :: BCIALG_6:def 10
for x being Element of X holds it . x = Class RI,x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines nat_hom BCIALG_6:def 10 :

begin

theorem :: BCIALG_6:50

for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds nat_hom RI is onto

proof end;

theorem Th51: :: BCIALG_6:51

for X, X' being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X' st I = Ker f holds
ex h being BCI-homomorphism of (X ./. RI),X' st
( f = h * (nat_hom RI) & h is one-to-one )

proof end;

theorem :: BCIALG_6:52

theorem :: BCIALG_6:53

for X being BCI-algebra
for K being closed Ideal of X
for RK being I-congruence of X,K holds Ker (nat_hom RK) = K

proof end;

Lm4: 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'

proof end;

begin

theorem :: BCIALG_6:54

for X', X being BCI-algebra
for H' being SubAlgebra of X'
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X' st I = Ker f & the carrier of H' = rng f holds
X ./. RI,H' are_isomorphic

proof end;

theorem Th55: :: BCIALG_6:55

for X, X' being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X' st I = Ker f & f is onto holds
X ./. RI,X' are_isomorphic

proof end;

begin

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 Union G,RK -> non empty Subset of X equals :: BCIALG_6:def 11
union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
correctness

proof end;

end;

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines HKOp BCIALG_6:def 12 :

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 zeroHK G,RK -> Element of Union G,RK equals :: BCIALG_6:def 13
0. X;
coherence

proof end;

end;

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

end;

:: deftheorem defines HK BCIALG_6:def 14 :

registration

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;
cluster HK G,RK -> non empty ;
coherence ;

end;

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;
let w1, w2 be Element of Union G,RK;
func w1 \ w2 -> Element of Union G,RK equals :: BCIALG_6:def 15
(HKOp G,RK) . w1,w2;
coherence ;

end;

:: deftheorem defines \ BCIALG_6:def 15 :

theorem Th56: :: BCIALG_6:56

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 holds HK G,RK is BCI-algebra

proof end;

registration

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;
cluster HK G,RK -> strict being_B being_C being_I being_BCI-4 ;
coherence by Th56;

end;

theorem Th57: :: BCIALG_6:57

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 holds HK G,RK is SubAlgebra of X

proof end;

theorem :: BCIALG_6:58

for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G

proof end;

theorem :: BCIALG_6:59

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 K1 being Ideal of HK G,RK
for RK1 being I-congruence of HK G,RK,K1
for I being Ideal of G
for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic

proof end;