:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu

::

:: Received August 26, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

definition

let G be non empty BCIStr_0 ;

ex b_{1} being Function of [: the carrier of G,NAT:], the carrier of G st

for x being Element of G holds

( b_{1} . (x,0) = 0. G & ( for n being Nat holds b_{1} . (x,(n + 1)) = x \ ((b_{1} . (x,n)) `) ) )

for b_{1}, b_{2} being Function of [: the carrier of G,NAT:], the carrier of G st ( for x being Element of G holds

( b_{1} . (x,0) = 0. G & ( for n being Nat holds b_{1} . (x,(n + 1)) = x \ ((b_{1} . (x,n)) `) ) ) ) & ( for x being Element of G holds

( b_{2} . (x,0) = 0. G & ( for n being Nat holds b_{2} . (x,(n + 1)) = x \ ((b_{2} . (x,n)) `) ) ) ) holds

b_{1} = b_{2}

end;
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 Nat holds it . (x,(n + 1)) = x \ ((it . (x,n)) `) ) );

existence for x being Element of G holds

( it . (x,0) = 0. G & ( for n being Nat holds it . (x,(n + 1)) = x \ ((it . (x,n)) `) ) );

ex b

for x being Element of G holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

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

for G being non empty BCIStr_0

for b_{2} being Function of [: the carrier of G,NAT:], the carrier of G holds

( b_{2} = BCI-power G iff for x being Element of G holds

( b_{2} . (x,0) = 0. G & ( for n being Nat holds b_{2} . (x,(n + 1)) = x \ ((b_{2} . (x,n)) `) ) ) );

for G being non empty BCIStr_0

for b

( b

( b

definition

let X be BCI-algebra;

let x be Element of X;

let i be Integer;

coherence

( ( 0 <= i implies (BCI-power X) . (x,|.i.|) is Element of X ) & ( not 0 <= i implies (BCI-power X) . ((x `),|.i.|) is Element of X ) );

consistency

for b_{1} being Element of X holds verum;

;

end;
let x be Element of X;

let i be Integer;

func x |^ i -> Element of X equals :Def2: :: BCIALG_6:def 2

(BCI-power X) . (x,|.i.|) if 0 <= i

otherwise (BCI-power X) . ((x `),|.i.|);

correctness (BCI-power X) . (x,|.i.|) if 0 <= i

otherwise (BCI-power X) . ((x `),|.i.|);

coherence

( ( 0 <= i implies (BCI-power X) . (x,|.i.|) is Element of X ) & ( not 0 <= i implies (BCI-power X) . ((x `),|.i.|) is Element of X ) );

consistency

for b

;

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

for X being BCI-algebra

for x being Element of X

for i being Integer holds

( ( 0 <= i implies x |^ i = (BCI-power X) . (x,|.i.|) ) & ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),|.i.|) ) );

for X being BCI-algebra

for x being Element of X

for i being Integer holds

( ( 0 <= i implies x |^ i = (BCI-power X) . (x,|.i.|) ) & ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),|.i.|) ) );

definition

let X be BCI-algebra;

let x be Element of X;

let n be natural Number ;

compatibility

for b_{1} being Element of X holds

( b_{1} = x |^ n iff b_{1} = (BCI-power X) . (x,n) )

end;
let x be Element of X;

let n be natural Number ;

compatibility

for b

( b

proof end;

:: deftheorem defines |^ BCIALG_6:def 3 :

for X being BCI-algebra

for x being Element of X

for n being natural Number holds x |^ n = (BCI-power X) . (x,n);

for X being BCI-algebra

for x being Element of X

for n being natural Number holds x |^ n = (BCI-power X) . (x,n);

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)

for x being Element of X

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

proof end;

::P18-theorem 1.4.2(1-4)

theorem :: BCIALG_6:9

for X being BCI-algebra

for x being Element of X

for n being Nat holds x |^ (- n) = ((x `) `) |^ (- n)

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)

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

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

for x being Element of X

for n being Nat st x in BCK-part X holds

x |^ (- n) = 0. X

proof end;

::P19 theorem 1.4.3

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

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

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 m, n 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)

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

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

for a being Element of AtomSet X

for n being Nat holds (a `) |^ n = (a |^ 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)) `

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

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

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)

for a being Element of AtomSet X

for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)

proof end;

::1.4.11

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)

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

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;

end;
let x be Element of X;

attr x is finite-period means :: BCIALG_6:def 4

ex n being Element of NAT st

( n <> 0 & x |^ n in BCK-part X );

ex n being Element of NAT st

( n <> 0 & x |^ n in BCK-part X );

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

for X being BCI-algebra

for x being Element of X holds

( x is finite-period iff ex n being Element of NAT st

( n <> 0 & x |^ n in BCK-part X ) );

for X being BCI-algebra

for x being Element of X holds

( x is finite-period iff ex n being Element of NAT st

( n <> 0 & x |^ n in BCK-part X ) );

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

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 ;

ex b_{1} being Element of NAT st

( x |^ b_{1} in BCK-part X & b_{1} <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds

b_{1} <= m ) )

for b_{1}, b_{2} being Element of NAT st x |^ b_{1} in BCK-part X & b_{1} <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds

b_{1} <= m ) & x |^ b_{2} in BCK-part X & b_{2} <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds

b_{2} <= m ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( x |^ b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines ord BCIALG_6:def 5 :

for X being BCI-algebra

for x being Element of X st x is finite-period holds

for b_{3} being Element of NAT holds

( b_{3} = ord x iff ( x |^ b_{3} in BCK-part X & b_{3} <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds

b_{3} <= m ) ) );

for X being BCI-algebra

for x being Element of X st x is finite-period holds

for b

( b

b

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

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

( 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

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 m, n being Nat st x is finite-period & ord x = n holds

( x |^ m in BCK-part X iff n divides m )

for x being Element of X

for m, n 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)

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

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

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)

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;

theorem Th34: :: BCIALG_6:34

for X being BCI-algebra

for Y being SubAlgebra of X

for x, y being Element of X

for x9, y9 being Element of Y st x = x9 & y = y9 holds

x \ y = x9 \ y9

for Y being SubAlgebra of X

for x, y being Element of X

for x9, y9 being Element of Y st x = x9 & y = y9 holds

x \ y = x9 \ y9

proof end;

definition

let X, X9 be non empty BCIStr_0 ;

let f be Function of X,X9;

end;
let f be Function of X,X9;

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

for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b);

:: deftheorem Def6 defines multiplicative BCIALG_6:def 6 :

for X, X9 being non empty BCIStr_0

for f being Function of X,X9 holds

( f is multiplicative iff for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b) );

for X, X9 being non empty BCIStr_0

for f being Function of X,X9 holds

( f is multiplicative iff for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b) );

registration

let X, X9 be BCI-algebra;

ex b_{1} being Function of X,X9 st b_{1} is multiplicative

end;
cluster Relation-like the carrier of X -defined the carrier of X9 -valued Function-like non empty V14( the carrier of X) quasi_total multiplicative for Function of ,;

existence ex b

proof end;

definition
end;

:: deftheorem defines isotonic BCIALG_6:def 7 :

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 holds

( f is isotonic iff for x, y being Element of X st x <= y holds

f . x <= f . y );

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 holds

( f is isotonic iff for x, y being Element of X st x <= y holds

f . x <= f . y );

definition

let X, X9 be BCI-algebra;

let f be BCI-homomorphism of X,X9;

coherence

{ x where x is Element of X : f . x = 0. X9 } is set ;

end;
let f be BCI-homomorphism of X,X9;

coherence

{ x where x is Element of X : f . x = 0. X9 } is set ;

:: deftheorem defines Ker BCIALG_6:def 8 :

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 holds Ker f = { x where x is Element of X : f . x = 0. X9 } ;

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 holds Ker f = { x where x is Element of X : f . x = 0. X9 } ;

registration
end;

theorem :: BCIALG_6:36

for X, X9 being BCI-algebra

for x, y being Element of X

for f being BCI-homomorphism of X,X9 st x <= y holds

f . x <= f . y

for x, y being Element of X

for f being BCI-homomorphism of X,X9 st x <= y holds

f . x <= f . y

proof end;

theorem :: BCIALG_6:37

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 holds

( f is one-to-one iff Ker f = {(0. X)} )

for f being BCI-homomorphism of X,X9 holds

( f is one-to-one iff Ker f = {(0. X)} )

proof end;

theorem :: BCIALG_6:38

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9

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

g is bijective

for f being BCI-homomorphism of X,X9

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

g is bijective

proof end;

theorem :: BCIALG_6:39

for X, X9, Y being BCI-algebra

for f being BCI-homomorphism of X,X9

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

for f being BCI-homomorphism of X,X9

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

proof end;

theorem :: BCIALG_6:40

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9

for Z being SubAlgebra of X9 st the carrier of Z = rng f holds

f is BCI-homomorphism of X,Z

for f being BCI-homomorphism of X,X9

for Z being SubAlgebra of X9 st the carrier of Z = rng f holds

f is BCI-homomorphism of X,Z

proof end;

registration

let X, X9 be BCI-algebra;

let f be BCI-homomorphism of X,X9;

coherence

for b_{1} being Ideal of X st b_{1} = Ker f holds

b_{1} is closed
by Th41;

end;
let f be BCI-homomorphism of X,X9;

coherence

for b

b

theorem Th42: :: BCIALG_6:42

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9 st f is onto holds

for c being Element of X9 ex x being Element of X st c = f . x

for f being BCI-homomorphism of X,X9 st f is onto holds

for c being Element of X9 ex x being Element of X st c = f . x

proof end;

::P75

theorem :: BCIALG_6:43

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9

for a being Element of X st a is minimal holds

f . a is minimal

for f being BCI-homomorphism of X,X9

for a being Element of X st a is minimal holds

f . a is minimal

proof end;

theorem :: BCIALG_6:44

for X, X9 being BCI-algebra

for f being BCI-homomorphism of X,X9

for a being Element of AtomSet X

for b being Element of AtomSet X9 st b = f . a holds

f .: (BranchV a) c= BranchV b

for f being BCI-homomorphism of X,X9

for a being Element of AtomSet X

for b being Element of AtomSet X9 st b = f . a holds

f .: (BranchV a) c= BranchV b

proof end;

::P76

theorem Th45: :: BCIALG_6:45

for X, X9 being BCI-algebra

for A9 being non empty Subset of X9

for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds

f " A9 is Ideal of X

for A9 being non empty Subset of X9

for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds

f " A9 is Ideal of X

proof end;

theorem :: BCIALG_6:46

for X, X9 being BCI-algebra

for A9 being non empty Subset of X9

for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds

f " A9 is closed Ideal of X

for A9 being non empty Subset of X9

for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds

f " A9 is closed Ideal of X

proof end;

theorem Th47: :: BCIALG_6:47

for X, X9 being BCI-algebra

for I being Ideal of X

for f being BCI-homomorphism of X,X9 st f is onto holds

f .: I is Ideal of X9

for I being Ideal of X

for f being BCI-homomorphism of X,X9 st f is onto holds

f .: I is Ideal of X9

proof end;

theorem :: BCIALG_6:48

for X, X9 being BCI-algebra

for CI being closed Ideal of X

for f being BCI-homomorphism of X,X9 st f is onto holds

f .: CI is closed Ideal of X9

for CI being closed Ideal of X

for f being BCI-homomorphism of X,X9 st f is onto holds

f .: CI is closed Ideal of X9

proof end;

definition

let X, X9 be BCI-algebra;

end;
pred X,X9 are_isomorphic means :: BCIALG_6:def 9

ex f being BCI-homomorphism of X,X9 st f is bijective ;

ex f being BCI-homomorphism of X,X9 st f is bijective ;

:: deftheorem defines are_isomorphic BCIALG_6:def 9 :

for X, X9 being BCI-algebra holds

( X,X9 are_isomorphic iff ex f being BCI-homomorphism of X,X9 st f is bijective );

for X, X9 being BCI-algebra holds

( X,X9 are_isomorphic iff ex f being BCI-homomorphism of X,X9 st f is bijective );

registration

let X be BCI-algebra;

let I be Ideal of X;

let RI be I-congruence of X,I;

coherence

( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) ;

end;
let I be Ideal of X;

let RI be I-congruence of X,I;

coherence

( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) ;

definition

let X be BCI-algebra;

let I be Ideal of X;

let RI be I-congruence of X,I;

ex b_{1} being BCI-homomorphism of X,(X ./. RI) st

for x being Element of X holds b_{1} . x = Class (RI,x)

for b_{1}, b_{2} being BCI-homomorphism of X,(X ./. RI) st ( for x being Element of X holds b_{1} . x = Class (RI,x) ) & ( for x being Element of X holds b_{2} . x = Class (RI,x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X holds it . x = Class (RI,x);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines nat_hom BCIALG_6:def 10 :

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for b_{4} being BCI-homomorphism of X,(X ./. RI) holds

( b_{4} = nat_hom RI iff for x being Element of X holds b_{4} . x = Class (RI,x) );

for X being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for b

( b

:: f

:: X--------->X'

:: | /

:: g| / h

:: | /

:: | /

:: | /

:: V /

:: X/Ker(f)

:: X--------->X'

:: | /

:: g| / h

:: | /

:: | /

:: | /

:: V /

:: X/Ker(f)

theorem :: BCIALG_6:49

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

for I being Ideal of X

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

proof end;

theorem Th50: :: BCIALG_6:50

for X, X9 being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f holds

ex h being BCI-homomorphism of (X ./. RI),X9 st

( f = h * (nat_hom RI) & h is one-to-one )

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f holds

ex h being BCI-homomorphism of (X ./. RI),X9 st

( f = h * (nat_hom RI) & h is one-to-one )

proof end;

::$CT

theorem :: BCIALG_6:52

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

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, X9 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

proof end;

theorem :: BCIALG_6:53

for X, X9 being BCI-algebra

for H9 being SubAlgebra of X9

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds

X ./. RI,H9 are_isomorphic

for H9 being SubAlgebra of X9

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds

X ./. RI,H9 are_isomorphic

proof end;

theorem Th53: :: BCIALG_6:54

for X, X9 being BCI-algebra

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds

X ./. RI,X9 are_isomorphic

for I being Ideal of X

for RI being I-congruence of X,I

for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds

X ./. RI,X9 are_isomorphic

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;

coherence

union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } is non empty Subset of X;

end;
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 union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ;

coherence

union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } is non empty Subset of X;

proof end;

:: deftheorem defines Union BCIALG_6:def 11 :

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 Union (G,RK) = union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ;

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 Union (G,RK) = union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ;

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;

ex b_{1} 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

b_{1} . (w1,w2) = x \ y

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (w1,w2) = x \ y ) holds

b_{1} = b_{2}

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

ex b

for w1, w2 being Element of Union (G,RK)

for x, y being Element of X st w1 = x & w2 = y holds

b

proof end;

uniqueness for b

for x, y being Element of X st w1 = x & w2 = y holds

b

for x, y being Element of X st w1 = x & w2 = y holds

b

b

proof end;

:: deftheorem Def12 defines HKOp BCIALG_6:def 12 :

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 b_{5} being BinOp of (Union (G,RK)) holds

( b_{5} = HKOp (G,RK) iff for w1, w2 being Element of Union (G,RK)

for x, y being Element of X st w1 = x & w2 = y holds

b_{5} . (w1,w2) = x \ y );

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 b

( b

for x, y being Element of X st w1 = x & w2 = y holds

b

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;

coherence

0. X is Element of Union (G,RK)

end;
let G be SubAlgebra of X;

let K be closed Ideal of X;

let RK be I-congruence of X,K;

coherence

0. X is Element of Union (G,RK)

proof end;

:: deftheorem defines zeroHK BCIALG_6:def 13 :

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 zeroHK (G,RK) = 0. X;

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 zeroHK (G,RK) = 0. X;

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;

BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #) is BCIStr_0 ;

end;
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)) #);

BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #) is BCIStr_0 ;

:: deftheorem defines HK BCIALG_6:def 14 :

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) = BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #);

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) = BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #);

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;

coherence

not HK (G,RK) is empty ;

end;
let G be SubAlgebra of X;

let K be closed Ideal of X;

let RK be I-congruence of X,K;

coherence

not HK (G,RK) is empty ;

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

coherence

(HKOp (G,RK)) . (w1,w2) is Element of Union (G,RK) ;

end;
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);

coherence

(HKOp (G,RK)) . (w1,w2) is Element of Union (G,RK) ;

:: deftheorem defines \ BCIALG_6:def 15 :

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 w1, w2 being Element of Union (G,RK) holds w1 \ w2 = (HKOp (G,RK)) . (w1,w2);

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 w1, w2 being Element of Union (G,RK) holds w1 \ w2 = (HKOp (G,RK)) . (w1,w2);

theorem Th54: :: BCIALG_6:55

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

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;

coherence

( HK (G,RK) is strict & HK (G,RK) is being_B & HK (G,RK) is being_C & HK (G,RK) is being_I & HK (G,RK) is being_BCI-4 ) by Th54;

end;
let G be SubAlgebra of X;

let K be closed Ideal of X;

let RK be I-congruence of X,K;

coherence

( HK (G,RK) is strict & HK (G,RK) is being_B & HK (G,RK) is being_C & HK (G,RK) is being_I & HK (G,RK) is being_BCI-4 ) by Th54;

theorem Th55: :: 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 SubAlgebra of X

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

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

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

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

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;