let X', X be BCI-algebra; :: thesis: 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
let H' be SubAlgebra of X'; :: thesis: 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
let I be Ideal of X; :: thesis: 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
let RI be I-congruence of X,I; :: thesis: for f being BCI-homomorphism of X,X' st I = Ker f & the carrier of H' = rng f holds
X ./. RI,H' are_isomorphic
let f be BCI-homomorphism of X,X'; :: thesis: ( I = Ker f & the carrier of H' = rng f implies X ./. RI,H' are_isomorphic )
assume AA:
( I = Ker f & the carrier of H' = rng f )
; :: thesis: X ./. RI,H' are_isomorphic
set J = X ./. RI;
defpred S1[ set , set ] means for a being Element of X st $1 = Class RI,a holds
$2 = f . a;
A1:
for x being Element of (X ./. RI) ex y being Element of H' st S1[x,y]
proof
let x be
Element of
(X ./. RI);
:: thesis: ex y being Element of H' st S1[x,y]
x in Class RI
;
then consider y being
set such that B3:
(
y in the
carrier of
X &
x = Class RI,
y )
by EQREL_1:def 5;
reconsider y =
y as
Element of
X by B3;
dom f = the
carrier of
X
by FUNCT_2:def 1;
then reconsider t =
f . y as
Element of
H' by AA, FUNCT_1:def 5;
take
t
;
:: thesis: S1[x,t]
let a be
Element of
X;
:: thesis: ( x = Class RI,a implies t = f . a )
assume
x = Class RI,
a
;
:: thesis: t = f . a
then
y in Class RI,
a
by B3, EQREL_1:31;
then
[a,y] in RI
by EQREL_1:26;
then B4:
(
a \ y in Ker f &
y \ a in Ker f )
by AA, BCIALG_2:def 12;
then consider x1 being
Element of
X such that B5:
(
a \ y = x1 &
f . x1 = 0. X' )
;
consider x2 being
Element of
X such that B7:
(
y \ a = x2 &
f . x2 = 0. X' )
by B4;
(
(f . a) \ (f . y) = 0. X' &
(f . y) \ (f . a) = 0. X' )
by Def0, B5, B7;
hence
t = f . a
by BCIALG_1:def 7;
:: thesis: verum
end;
consider h being Function of (X ./. RI),H' such that
A9:
for x being Element of (X ./. RI) holds S1[x,h . x]
from FUNCT_2:sch 3(A1);
now let a,
b be
Element of
(X ./. RI);
:: thesis: (h . a) \ (h . b) = h . (a \ b)A11:
(
a in Class RI &
b in Class RI )
;
then consider a1 being
set such that A13:
(
a1 in the
carrier of
X &
a = Class RI,
a1 )
by EQREL_1:def 5;
consider b1 being
set such that A15:
(
b1 in the
carrier of
X &
b = Class RI,
b1 )
by A11, EQREL_1:def 5;
reconsider a1 =
a1,
b1 =
b1 as
Element of
X by A13, A15;
reconsider f =
f as
BCI-homomorphism of
X,
H' by AA, Lmco1671;
(
h . a = f . a1 &
h . b = f . b1 )
by A9, A13, A15;
then A19:
(h . a) \ (h . b) = f . (a1 \ b1)
by Def0;
a \ b = Class RI,
(a1 \ b1)
by A13, A15, BCIALG_2:def 17;
hence
(h . a) \ (h . b) = h . (a \ b)
by A19, A9;
:: thesis: verum end;
then reconsider h = h as BCI-homomorphism of (X ./. RI),H' by Def0;
X1:
h is one-to-one
proof
let y1,
y2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not y1 in dom h or not y2 in dom h or not h . y1 = h . y2 or y1 = y2 )
assume DD:
(
y1 in dom h &
y2 in dom h &
h . y1 = h . y2 )
;
:: thesis: y1 = y2
then reconsider y1 =
y1,
y2 =
y2 as
Element of
(X ./. RI) ;
A21:
(
y1 in Class RI &
y2 in Class RI )
;
then consider a1 being
set such that A23:
(
a1 in the
carrier of
X &
y1 = Class RI,
a1 )
by EQREL_1:def 5;
consider b1 being
set such that A25:
(
b1 in the
carrier of
X &
y2 = Class RI,
b1 )
by A21, EQREL_1:def 5;
reconsider a1 =
a1,
b1 =
b1 as
Element of
X by A23, A25;
(
h . y1 = f . a1 &
h . y2 = f . b1 )
by A9, A23, A25;
then
(
(f . a1) \ (f . b1) = 0. X' &
(f . b1) \ (f . a1) = 0. X' )
by DD, BCIALG_1:def 5;
then
(
f . (a1 \ b1) = 0. X' &
f . (b1 \ a1) = 0. X' )
by Def0;
then
(
a1 \ b1 in Ker f &
b1 \ a1 in Ker f )
;
then
[a1,b1] in RI
by AA, BCIALG_2:def 12;
then
b1 in Class RI,
a1
by EQREL_1:26;
hence
y1 = y2
by A23, A25, EQREL_1:31;
:: thesis: verum
end;
X3:
the carrier of H' c= rng h
rng h = the carrier of H'
by X3, XBOOLE_0:def 10;
then
h is onto
by FUNCT_2:def 3;
hence
X ./. RI,H' are_isomorphic
by Def4, X1; :: thesis: verum