let X be BCI-algebra; :: thesis: for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let RI be I-congruence of X,I; :: thesis: X ./. RI is BCI-algebra
reconsider IT = X ./. RI as non empty BCIStr_0 ;
A1:
IT is being_B
proof
now let w1,
w2,
w3 be
Element of
IT;
:: thesis: ((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. ITA2:
(
w1 in the
carrier of
IT &
w2 in the
carrier of
IT &
w3 in the
carrier of
IT )
;
then consider x1 being
set such that A3:
(
x1 in the
carrier of
X &
w1 = Class RI,
x1 )
by EQREL_1:def 5;
consider y1 being
set such that A4:
(
y1 in the
carrier of
X &
w2 = Class RI,
y1 )
by A2, EQREL_1:def 5;
consider z1 being
set such that A5:
(
z1 in the
carrier of
X &
w3 = Class RI,
z1 )
by A2, EQREL_1:def 5;
reconsider x1 =
x1,
y1 =
y1,
z1 =
z1 as
Element of
X by A3, A4, A5;
A6:
(
w1 \ w2 = Class RI,
(x1 \ y1) &
w3 \ w2 = Class RI,
(z1 \ y1) &
w1 \ w3 = Class RI,
(x1 \ z1) )
by A3, A4, A5, Def17;
then
(w1 \ w2) \ (w3 \ w2) = Class RI,
((x1 \ y1) \ (z1 \ y1))
by Def17;
then
((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = Class RI,
(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1))
by A6, Def17;
hence
((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. IT
by BCIALG_1:def 3;
:: thesis: verum end;
hence
IT is
being_B
by BCIALG_1:def 3;
:: thesis: verum
end;
A7:
IT is being_C
proof
now let w1,
w2,
w3 be
Element of
IT;
:: thesis: ((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. ITA8:
(
w1 in the
carrier of
IT &
w2 in the
carrier of
IT &
w3 in the
carrier of
IT )
;
then consider x1 being
set such that A9:
(
x1 in the
carrier of
X &
w1 = Class RI,
x1 )
by EQREL_1:def 5;
consider y1 being
set such that A10:
(
y1 in the
carrier of
X &
w2 = Class RI,
y1 )
by A8, EQREL_1:def 5;
consider z1 being
set such that A11:
(
z1 in the
carrier of
X &
w3 = Class RI,
z1 )
by A8, EQREL_1:def 5;
reconsider x1 =
x1,
y1 =
y1,
z1 =
z1 as
Element of
X by A9, A10, A11;
(
w1 \ w2 = Class RI,
(x1 \ y1) &
w1 \ w3 = Class RI,
(x1 \ z1) )
by A9, A10, A11, Def17;
then
(
(w1 \ w2) \ w3 = Class RI,
((x1 \ y1) \ z1) &
(w1 \ w3) \ w2 = Class RI,
((x1 \ z1) \ y1) )
by A10, A11, Def17;
then
((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = Class RI,
(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1))
by Def17;
hence
((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. IT
by BCIALG_1:def 4;
:: thesis: verum end;
hence
IT is
being_C
by BCIALG_1:def 4;
:: thesis: verum
end;
A12:
IT is being_I
IT is being_BCI-4
proof
now let w1,
w2 be
Element of
IT;
:: thesis: ( w1 \ w2 = 0. IT & w2 \ w1 = 0. IT implies w1 = w2 )assume A14:
(
w1 \ w2 = 0. IT &
w2 \ w1 = 0. IT )
;
:: thesis: w1 = w2A15:
(
w1 in the
carrier of
IT &
w2 in the
carrier of
IT )
;
then consider x1 being
set such that A16:
(
x1 in the
carrier of
X &
w1 = Class RI,
x1 )
by EQREL_1:def 5;
consider y1 being
set such that A17:
(
y1 in the
carrier of
X &
w2 = Class RI,
y1 )
by A15, EQREL_1:def 5;
reconsider x1 =
x1,
y1 =
y1 as
Element of
X by A16, A17;
(
w1 \ w2 = Class RI,
(x1 \ y1) &
w2 \ w1 = Class RI,
(y1 \ x1) )
by A16, A17, Def17;
then
(
0. X in Class RI,
(x1 \ y1) &
0. X in Class RI,
(y1 \ x1) )
by A14, EQREL_1:31;
then
(
[(x1 \ y1),(0. X)] in RI &
[(y1 \ x1),(0. X)] in RI )
by EQREL_1:26;
then
(
(x1 \ y1) \ (0. X) in I &
(y1 \ x1) \ (0. X) in I )
by Def12;
then
(
x1 \ y1 in I &
y1 \ x1 in I )
by BCIALG_1:2;
then
[x1,y1] in RI
by Def12;
hence
w1 = w2
by A16, A17, EQREL_1:44;
:: thesis: verum end;
hence
IT is
being_BCI-4
by BCIALG_1:def 7;
:: thesis: verum
end;
hence
X ./. RI is BCI-algebra
by A1, A7, A12; :: thesis: verum