let X be BCI-algebra; :: thesis: 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 K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let G be SubAlgebra of X; :: thesis: 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 K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let K be closed Ideal of X; :: thesis: 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 K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RK be I-congruence of X,K; :: thesis: 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 K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let K1 be Ideal of HK G,RK; :: thesis: 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 K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RK1 be I-congruence of HK G,RK,K1; :: thesis: for I being Ideal of G
for RI being I-congruence of G,I st K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let I be Ideal of G; :: thesis: for RI being I-congruence of G,I st K1 = K & RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RI be I-congruence of G,I; :: thesis: ( K1 = K & RK1 = RK & I = the carrier of G /\ K implies G ./. RI,(HK G,RK) ./. RK1 are_isomorphic )
assume A1:
( K1 = K & RK1 = RK & I = the carrier of G /\ K )
; :: thesis: G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
A3:
the carrier of G c= the carrier of (HK G,RK)
proof
let xx be
set ;
:: according to TARSKI:def 3 :: thesis: ( not xx in the carrier of G or xx in the carrier of (HK G,RK) )
assume
xx in the
carrier of
G
;
:: thesis: xx in the carrier of (HK G,RK)
then reconsider x =
xx as
Element of
G ;
the
carrier of
G c= the
carrier of
X
by BCIALG_1:def 10;
then H2:
x in the
carrier of
X
by TARSKI:def 3;
then
[x,x] in RK
by EQREL_1:11;
then H3:
x in Class RK,
x
by EQREL_1:26;
Class RK,
x in the
carrier of
(X ./. RK)
by H2, EQREL_1:def 5;
then
Class RK,
x in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) }
;
hence
xx in the
carrier of
(HK G,RK)
by H3, TARSKI:def 4;
:: thesis: verum
end;
defpred S1[ Element of G, set ] means $2 = Class RK1,$1;
A5:
for x being Element of G ex y being Element of ((HK G,RK) ./. RK1) st S1[x,y]
consider f being Function of G,((HK G,RK) ./. RK1) such that
A7:
for x being Element of G holds S1[x,f . x]
from FUNCT_2:sch 3(A5);
now let a,
b be
Element of
G;
:: thesis: f . (a \ b) = (f . a) \ (f . b)
(
a in the
carrier of
G &
b in the
carrier of
G )
;
then reconsider Wa =
Class RK1,
a,
Wb =
Class RK1,
b as
Element of
Class RK1 by A3, EQREL_1:def 5;
(
a in the
carrier of
G &
b in the
carrier of
G )
;
then reconsider a1 =
a,
b1 =
b as
Element of
(HK G,RK) by A3;
(
Wa = f . a &
Wb = f . b )
by A7;
then B9:
(f . a) \ (f . b) = Class RK1,
(a1 \ b1)
by BCIALG_2:def 17;
the
carrier of
G c= the
carrier of
X
by BCIALG_1:def 10;
then reconsider xa =
a,
xb =
b as
Element of
X by TARSKI:def 3;
CC:
HK G,
RK is
SubAlgebra of
X
by Thxm1;
xa \ xb = a1 \ b1
by Lmth14, CC;
then
(f . a) \ (f . b) = Class RK1,
(a \ b)
by B9, Lmth14;
hence
f . (a \ b) = (f . a) \ (f . b)
by A7;
:: thesis: verum end;
then reconsider f = f as BCI-homomorphism of G,((HK G,RK) ./. RK1) by Def0;
CC1:
f is onto
proof
now let y be
set ;
:: thesis: ( y in rng f iff y in the carrier of ((HK G,RK) ./. RK1) )
(
y in the
carrier of
((HK G,RK) ./. RK1) implies
y in rng f )
proof
assume
y in the
carrier of
((HK G,RK) ./. RK1)
;
:: thesis: y in rng f
then consider x being
set such that D3:
(
x in the
carrier of
(HK G,RK) &
y = Class RK1,
x )
by EQREL_1:def 5;
consider a being
Element of
G such that D5:
x in Class RK,
a
by Lm168, D3;
(
a in the
carrier of
G & the
carrier of
G c= the
carrier of
X )
by BCIALG_1:def 10;
then
y = Class RK1,
a
by D3, A1, D5, EQREL_1:31;
then D9:
y = f . a
by A7;
(
a in the
carrier of
G &
dom f = the
carrier of
G )
by FUNCT_2:def 1;
hence
y in rng f
by D9, FUNCT_1:def 5;
:: thesis: verum
end; hence
(
y in rng f iff
y in the
carrier of
((HK G,RK) ./. RK1) )
;
:: thesis: verum end;
then
rng f = the
carrier of
((HK G,RK) ./. RK1)
by TARSKI:2;
hence
f is
onto
by FUNCT_2:def 3;
:: thesis: verum
end;
Ker f = I
proof
set X' =
(HK G,RK) ./. RK1;
thus
Ker f c= I
:: according to XBOOLE_0:def 10 :: thesis: I c= Ker fproof
let h be
set ;
:: according to TARSKI:def 3 :: thesis: ( not h in Ker f or h in I )
assume
h in Ker f
;
:: thesis: h in I
then consider x being
Element of
G such that D1:
(
h = x &
f . x = 0. ((HK G,RK) ./. RK1) )
;
(
x in the
carrier of
G & the
carrier of
G c= the
carrier of
X )
by BCIALG_1:def 10;
then reconsider x =
x as
Element of
X ;
Class RK,
x = Class RK,
(0. X)
by A1, D1, A7;
then
0. X in Class RK,
x
by EQREL_1:31;
then
[x,(0. X)] in RK
by EQREL_1:26;
then
(
x \ (0. X) in K &
0. X in K )
by BCIALG_1:def 18, BCIALG_2:def 12;
then
x in K
by BCIALG_1:def 18;
hence
h in I
by D1, A1, XBOOLE_0:def 4;
:: thesis: verum
end;
let h be
set ;
:: according to TARSKI:def 3 :: thesis: ( not h in I or h in Ker f )
assume D0:
h in I
;
:: thesis: h in Ker f
then reconsider x =
h as
Element of
X by A1;
D1:
(
h in the
carrier of
G &
h in K )
by A1, D0, XBOOLE_0:def 4;
D3:
x \ (0. X) in K
by D1, BCIALG_1:2;
x ` in K
by D1, BCIALG_1:def 19;
then
[x,(0. X)] in RK
by D3, BCIALG_2:def 12;
then
0. X in Class RK,
x
by EQREL_1:26;
then
Class RK1,
h = Class RK1,
(0. X)
by A1, EQREL_1:31;
then
f . h = 0. ((HK G,RK) ./. RK1)
by A7, D0;
hence
h in Ker f
by D0;
:: thesis: verum
end;
hence
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
by CO1672, CC1; :: thesis: verum