let X, X9 be 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
let H9 be 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
let I be 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
let RI be 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
let f be BCI-homomorphism of X,X9; ( I = Ker f & the carrier of H9 = rng f implies X ./. RI,H9 are_isomorphic )
assume that
A1:
I = Ker f
and
A2:
the carrier of H9 = rng f
; X ./. RI,H9 are_isomorphic
defpred S1[ set , set ] means for a being Element of X st $1 = Class (RI,a) holds
$2 = f . a;
set J = X ./. RI;
A3:
for x being Element of (X ./. RI) ex y being Element of H9 st S1[x,y]
proof
let x be
Element of
(X ./. RI);
ex y being Element of H9 st S1[x,y]
x in Class RI
;
then consider y being
object such that A4:
y in the
carrier of
X
and A5:
x = Class (
RI,
y)
by EQREL_1:def 3;
reconsider y =
y as
Element of
X by A4;
dom f = the
carrier of
X
by FUNCT_2:def 1;
then reconsider t =
f . y as
Element of
H9 by A2, FUNCT_1:def 3;
take
t
;
S1[x,t]
let a be
Element of
X;
( x = Class (RI,a) implies t = f . a )
assume
x = Class (
RI,
a)
;
t = f . a
then
y in Class (
RI,
a)
by A5, EQREL_1:23;
then A6:
[a,y] in RI
by EQREL_1:18;
then
y \ a in Ker f
by A1, BCIALG_2:def 12;
then
ex
x2 being
Element of
X st
(
y \ a = x2 &
f . x2 = 0. X9 )
;
then A7:
(f . y) \ (f . a) = 0. X9
by Def6;
a \ y in Ker f
by A1, A6, BCIALG_2:def 12;
then
ex
x1 being
Element of
X st
(
a \ y = x1 &
f . x1 = 0. X9 )
;
then
(f . a) \ (f . y) = 0. X9
by Def6;
hence
t = f . a
by A7, BCIALG_1:def 7;
verum
end;
consider h being Function of (X ./. RI),H9 such that
A8:
for x being Element of (X ./. RI) holds S1[x,h . x]
from FUNCT_2:sch 3(A3);
now for a, b being Element of (X ./. RI) holds (h . a) \ (h . b) = h . (a \ b)reconsider f =
f as
BCI-homomorphism of
X,
H9 by A2, Lm4;
let a,
b be
Element of
(X ./. RI);
(h . a) \ (h . b) = h . (a \ b)
a in Class RI
;
then consider a1 being
object such that A9:
a1 in the
carrier of
X
and A10:
a = Class (
RI,
a1)
by EQREL_1:def 3;
b in Class RI
;
then consider b1 being
object such that A11:
b1 in the
carrier of
X
and A12:
b = Class (
RI,
b1)
by EQREL_1:def 3;
reconsider a1 =
a1,
b1 =
b1 as
Element of
X by A9, A11;
A13:
a \ b = Class (
RI,
(a1 \ b1))
by A10, A12, BCIALG_2:def 17;
A14:
h . b = f . b1
by A8, A12;
h . a = f . a1
by A8, A10;
then
(h . a) \ (h . b) = f . (a1 \ b1)
by A14, Def6;
hence
(h . a) \ (h . b) = h . (a \ b)
by A8, A13;
verum end;
then reconsider h = h as BCI-homomorphism of (X ./. RI),H9 by Def6;
A15:
h is one-to-one
proof
let y1,
y2 be
object ;
FUNCT_1:def 4 ( not y1 in dom h or not y2 in dom h or not h . y1 = h . y2 or y1 = y2 )
assume that A16:
(
y1 in dom h &
y2 in dom h )
and A17:
h . y1 = h . y2
;
y1 = y2
reconsider y1 =
y1,
y2 =
y2 as
Element of
(X ./. RI) by A16;
y1 in Class RI
;
then consider a1 being
object such that A18:
a1 in the
carrier of
X
and A19:
y1 = Class (
RI,
a1)
by EQREL_1:def 3;
y2 in Class RI
;
then consider b1 being
object such that A20:
b1 in the
carrier of
X
and A21:
y2 = Class (
RI,
b1)
by EQREL_1:def 3;
reconsider a1 =
a1,
b1 =
b1 as
Element of
X by A18, A20;
A22:
h . y2 = f . b1
by A8, A21;
A23:
h . y1 = f . a1
by A8, A19;
then
(f . b1) \ (f . a1) = 0. X9
by A17, A22, BCIALG_1:def 5;
then
f . (b1 \ a1) = 0. X9
by Def6;
then A24:
b1 \ a1 in Ker f
;
(f . a1) \ (f . b1) = 0. X9
by A17, A23, A22, BCIALG_1:def 5;
then
f . (a1 \ b1) = 0. X9
by Def6;
then
a1 \ b1 in Ker f
;
then
[a1,b1] in RI
by A1, A24, BCIALG_2:def 12;
then
b1 in Class (
RI,
a1)
by EQREL_1:18;
hence
y1 = y2
by A19, A21, EQREL_1:23;
verum
end;
the carrier of H9 c= rng h
then
rng h = the carrier of H9
;
then
h is onto
by FUNCT_2:def 3;
hence
X ./. RI,H9 are_isomorphic
by A15; verum