:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008-2021 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 Nat holds it . (x,(n + 1)) = x \ ((it . (x,n)) `) ) );

existence
ex b₁ being Function of [: the carrier of G,NAT:], the carrier of G st
for x being Element of G holds
( b₁ . (x,0) = 0. G & ( for n being Nat holds b₁ . (x,(n + 1)) = x \ ((b₁ . (x,n)) `) ) )

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of G,NAT:], the carrier of G st ( for x being Element of G holds
( b₁ . (x,0) = 0. G & ( for n being Nat holds b₁ . (x,(n + 1)) = x \ ((b₁ . (x,n)) `) ) ) ) & ( for x being Element of G holds
( b<sub>2</sub> . (x,0) = 0. G & ( for n being Nat holds b<sub>2</sub> . (x,(n + 1)) = x \ ((b<sub>2</sub> . (x,n)) `) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines BCI-power BCIALG_6:def 1 :
for G being non empty BCIStr_0
for b₂ being Function of [: the carrier of G,NAT:], the carrier of G holds
( b₂ = BCI-power G iff for x being Element of G holds
( b₂ . (x,0) = 0. G & ( for n being Nat holds b₂ . (x,(n + 1)) = x \ ((b₂ . (x,n)) `) ) ) );

definition

let X be BCI-algebra;
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
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₁ being Element of X holds verum;
;

end;

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

definition

let X be BCI-algebra;
let x be Element of X;
let n be natural Number ;

redefine func x |^ n equals :: BCIALG_6:def 3
(BCI-power X) . (x,n);

compatibility
for b₁ being Element of X holds
( b₁ = x |^ n iff b₁ = (BCI-power X) . (x,n) )

proof end;

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

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) `) by Def1;

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;

::P18-theorem 1.4.2(1-4)

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;

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

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

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;

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

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 :: BCIALG_6:def 4
ex n being Element of NAT st
( n <> 0 & x |^ n in BCK-part X );

end;

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

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 b₁ being Element of NAT st
( x |^ b₁ in BCK-part X & b₁ <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b₁ <= m ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st x |^ b₁ in BCK-part X & b₁ <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b₁ <= m ) & x |^ b₂ in BCK-part X & b₂ <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b₂ <= m ) holds
b₁ = b₂

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 b₃ being Element of NAT holds
( b₃ = ord x iff ( x |^ b₃ in BCK-part X & b₃ <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b₃ <= 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 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)

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;

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 for Element of bool [: the carrier of X, the carrier of X9:];

existence
ex b₁ being Function of X,X9 st b₁ 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 X, X9 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 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

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

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

proof end;

theorem Th41: :: BCIALG_6:41

for X, X9 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 for Ideal of X;

coherence
for b₁ being Ideal of X st b₁ = Ker f holds
b₁ is closed by Th41;

end;

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

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

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

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

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

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

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

proof end;

definition

let X, X9 be BCI-algebra;

pred X,X9 are_isomorphic means :: BCIALG_6:def 9
ex f being BCI-homomorphism of X,X9 st f is bijective ;

end;

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

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 b₁ being BCI-homomorphism of X,(X ./. RI) st
for x being Element of X holds b₁ . x = Class (RI,x)

proof end;

uniqueness
for b₁, b₂ being BCI-homomorphism of X,(X ./. RI) st ( for x being Element of X holds b₁ . x = Class (RI,x) ) & ( for x being Element of X holds b₂ . x = Class (RI,x) ) holds
b₁ = b₂

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 b₄ being BCI-homomorphism of X,(X ./. RI) holds
( b₄ = nat_hom RI iff for x being Element of X holds b₄ . x = Class (RI,x) );

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

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 )

proof end;

theorem :: BCIALG_6:51

canceled;

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

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

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

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 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 b₁ 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₁ . (w1,w2) = x \ y

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (w1,w2) = x \ y ) holds
b₁ = b₂

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 b₅ being BinOp of (Union (G,RK)) holds
( b₅ = 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₅ . (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 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

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

end;

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

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

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

proof end;