let X be BCI-algebra; ( ( for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) implies for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I )
assume A1:
for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n
; for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let E be Congruence of X; for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let I be Ideal of X; ( I = Class (E,(0. X)) implies E is I-congruence of X,I )
assume A2:
I = Class (E,(0. X))
; E is I-congruence of X,I
now for x, y being Element of X holds
( [x,y] in E iff ( x \ y in I & y \ x in I ) )let x,
y be
Element of
X;
( [x,y] in E iff ( x \ y in I & y \ x in I ) )
(
x \ y in I &
y \ x in I implies
[x,y] in E )
proof
assume that A3:
x \ y in I
and A4:
y \ x in I
;
[x,y] in E
ex
z being
object st
(
[z,(y \ x)] in E &
z in {(0. X)} )
by A2, A4, RELAT_1:def 13;
then A5:
[(0. X),(y \ x)] in E
by TARSKI:def 1;
ex
z being
object st
(
[z,(x \ y)] in E &
z in {(0. X)} )
by A2, A3, RELAT_1:def 13;
then A6:
[(0. X),(x \ y)] in E
by TARSKI:def 1;
consider i,
j,
m,
n being
Nat such that A7:
(
((x,(x \ y)) to_power i),
(y \ x))
to_power j = (
((y,(y \ x)) to_power m),
(x \ y))
to_power n
by A1;
A8:
field E = the
carrier of
X
by EQREL_1:9;
A9:
E is_reflexive_in field E
by RELAT_2:def 9;
then
[x,x] in E
by A8, RELAT_2:def 1;
then A10:
[x,((x,(x \ y)) to_power i)] in E
by A2, A3, Th42;
A11:
[x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E
proof
defpred S1[
Nat]
means [x,((((x,(x \ y)) to_power i),(y \ x)) to_power $1)] in E;
A12:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
[x,((((x,(x \ y)) to_power i),(y \ x)) to_power k)] in E
;
S1[k + 1]
then
[(x \ (0. X)),(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E
by A5, Def9;
then
[x,(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E
by BCIALG_1:2;
hence
S1[
k + 1]
by Th4;
verum
end;
A13:
S1[
0 ]
by A10, Th1;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A13, A12);
hence
[x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E
;
verum
end;
[y,y] in E
by A8, A9, RELAT_2:def 1;
then A14:
[y,((y,(y \ x)) to_power m)] in E
by A2, A4, Th42;
A15:
[y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E
proof
defpred S1[
Nat]
means [y,((((y,(y \ x)) to_power m),(x \ y)) to_power $1)] in E;
A16:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
[y,((((y,(y \ x)) to_power m),(x \ y)) to_power k)] in E
;
S1[k + 1]
then
[(y \ (0. X)),(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E
by A6, Def9;
then
[y,(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E
by BCIALG_1:2;
hence
S1[
k + 1]
by Th4;
verum
end;
A17:
S1[
0 ]
by A14, Th1;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A17, A16);
hence
[y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E
;
verum
end;
E is_symmetric_in field E
by RELAT_2:def 11;
then
(
E is_transitive_in field E &
[((((x,(x \ y)) to_power i),(y \ x)) to_power j),y] in E )
by A7, A8, A15, RELAT_2:def 3, RELAT_2:def 16;
hence
[x,y] in E
by A8, A11, RELAT_2:def 8;
verum
end; hence
(
[x,y] in E iff (
x \ y in I &
y \ x in I ) )
by A2, Th40;
verum end;
hence
E is I-congruence of X,I
by Def12; verum