:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008-2011 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
f . n is Element of D
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
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)) `) ) )
proof end;
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
proof end;
end;

:: deftheorem Def1 defines BCI-power BCIALG_6:def 1 :
for G being non empty BCIStr_0
for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds
( b2 = BCI-power G iff 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)) `) ) ) );

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
coherence
( ( 0 <= i implies (BCI-power X) . (x,(abs i)) is Element of X ) & ( not 0 <= i implies (BCI-power X) . ((x `),(abs i)) is Element of X ) );
consistency
for b1 being Element of X holds verum;
;
end;

:: deftheorem Def2 defines |^ BCIALG_6:def 2 :
for X being BCI-algebra
for i being Integer
for x being Element of X holds
( ( 0 <= i implies x |^ i = (BCI-power X) . (x,(abs i)) ) & ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),(abs i)) ) );

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
for b1 being Element of X holds
( b1 = x |^ n iff b1 = (BCI-power X) . (x,n) )
proof end;
end;

:: deftheorem defines |^ BCIALG_6:def 3 :
for X being BCI-algebra
for n being Nat
for x being Element of X 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)
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 :
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
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
ex b1 being Element of NAT st
( x |^ b1 in BCK-part X & b1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b1 <= m ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st x |^ b1 in BCK-part X & b1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b1 <= m ) & x |^ b2 in BCK-part X & b2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b2 <= m ) holds
b1 = b2
proof end;
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 b3 being Element of NAT holds
( b3 = ord x iff ( x |^ b3 in BCK-part X & b3 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b3 <= m ) ) );

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 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;
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 :
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;
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 Element of bool [: the carrier of X, the carrier of X9:];
existence
ex b1 being Function of X,X9 st b1 is multiplicative
proof end;
end;

definition
let X, X9 be BCI-algebra;
mode BCI-homomorphism of X,X9 is multiplicative Function of X,X9;
end;

definition
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
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 :
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 be BCI-algebra;
mode Endomorphism of X is BCI-homomorphism of X,X;
end;

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

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

theorem Th35: :: BCIALG_6:35
for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds f . (0. X) = 0. X9
proof end;

registration
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
cluster Ker f -> non empty ;
coherence
not Ker f is empty
proof end;
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
proof end;

theorem :: BCIALG_6:37
for X9, X being BCI-algebra
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 X9, X 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
proof end;

theorem :: BCIALG_6:39
for X9, X, 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
proof end;

theorem :: BCIALG_6:40
canceled;

theorem :: BCIALG_6:41
for X9, X 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
proof end;

theorem Th42: :: BCIALG_6:42
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9 holds Ker f is closed Ideal of X
proof end;

registration
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
cluster Ker f -> closed Ideal of X;
coherence
for b1 being Ideal of X st b1 = Ker f holds
b1 is closed by Th42;
end;

theorem Th43: :: BCIALG_6:43
for X9, X 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
proof end;

theorem :: BCIALG_6:44
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9
for a being Element of X st a is atom holds
f . a is atom
proof end;

theorem :: BCIALG_6:45
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
proof end;

theorem Th46: :: BCIALG_6:46
for X9, X 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
proof end;

theorem :: BCIALG_6:47
for X9, X 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
proof end;

theorem Th48: :: BCIALG_6:48
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
proof end;

theorem :: BCIALG_6:49
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
proof end;

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

:: deftheorem Def9 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 );

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

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
ex b1 being BCI-homomorphism of X,(X ./. RI) st
for x being Element of X holds b1 . x = Class (RI,x)
proof end;
uniqueness
for b1, b2 being BCI-homomorphism of X,(X ./. RI) st ( for x being Element of X holds b1 . x = Class (RI,x) ) & ( for x being Element of X holds b2 . x = Class (RI,x) ) holds
b1 = b2
proof end;
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 b4 being BCI-homomorphism of X,(X ./. RI) holds
( b4 = nat_hom RI iff for x being Element of X holds b4 . x = Class (RI,x) );

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

theorem :: BCIALG_6:52
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 ) by Th51;

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

begin

theorem :: BCIALG_6:54
for X9, X 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
proof end;

theorem Th55: :: BCIALG_6:55
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
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
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;
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) } ;

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
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
proof end;
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
proof end;
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 b5 being BinOp of (Union (G,RK)) holds
( b5 = 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
b5 . (w1,w2) = x \ y );

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
0. X is Element of Union (G,RK)
proof end;
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;

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 :
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;
cluster HK (G,RK) -> non empty ;
coherence
not HK (G,RK) is empty ;
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
(HKOp (G,RK)) . (w1,w2) is Element of Union (G,RK) ;
end;

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

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