let X be BCI-algebra; for i, j, k being Element of NAT st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra
let i, j, k be Element of NAT ; ( X is BCI-algebra of i,j,j + k,i + k implies X is BCK-algebra )
assume A1:
X is BCI-algebra of i,j,j + k,i + k
; X is BCK-algebra
for y being Element of X holds (0. X) \ y = 0. X
proof
let y be
Element of
X;
(0. X) \ y = 0. X
A2:
(y,y to_power ((j + k) + 1)),
((0. X) \ y) to_power (i + k) =
((y,y to_power (j + k)) \ y),
((0. X) \ y) to_power (i + k)
by BCIALG_2:4
.=
((y \ y),y to_power (j + k)),
((0. X) \ y) to_power (i + k)
by BCIALG_2:7
.=
((0. X),y to_power (j + k)),
((0. X) \ y) to_power (i + k)
by BCIALG_1:def 5
.=
((0. X),((0. X) \ y) to_power (i + k)),
y to_power (j + k)
by BCIALG_2:11
.=
(((0. X),(0. X) to_power (i + k)) \ ((0. X),y to_power (i + k))),
y to_power (j + k)
by BCIALG_2:18
.=
((0. X) \ ((0. X),y to_power (i + k))),
y to_power (j + k)
by BCIALG_2:6
.=
((0. X),y to_power (j + k)) \ ((0. X),y to_power (i + k))
by BCIALG_2:7
.=
(((0. X),y to_power j),y to_power k) \ ((0. X),y to_power (i + k))
by BCIALG_2:10
.=
(((0. X),y to_power j),y to_power k) \ (((0. X),y to_power i),y to_power k)
by BCIALG_2:10
;
A3:
(((0. X),y to_power j),y to_power k) \ (((0. X),y to_power i),y to_power k) <= ((0. X),y to_power j) \ ((0. X),y to_power i)
by BCIALG_2:21;
Polynom i,
j,
(0. X),
y = Polynom (j + k),
(i + k),
y,
(0. X)
by A1, Def3;
then
((0. X),((0. X) \ y) to_power (i + 1)),
y to_power j = (y,(y \ (0. X)) to_power ((j + k) + 1)),
((0. X) \ y) to_power (i + k)
by BCIALG_1:2;
then
((0. X),((0. X) \ y) to_power (i + 1)),
y to_power j = (y,y to_power ((j + k) + 1)),
((0. X) \ y) to_power (i + k)
by BCIALG_1:2;
then A4:
((0. X),y to_power j),
((0. X) \ y) to_power (i + 1) = (y,y to_power ((j + k) + 1)),
((0. X) \ y) to_power (i + k)
by BCIALG_2:11;
((0. X),y to_power j),
((0. X) \ y) to_power (i + 1) =
((0. X),((0. X) \ y) to_power (i + 1)),
y to_power j
by BCIALG_2:11
.=
(((0. X),(0. X) to_power (i + 1)) \ ((0. X),y to_power (i + 1))),
y to_power j
by BCIALG_2:18
.=
((0. X) \ ((0. X),y to_power (i + 1))),
y to_power j
by BCIALG_2:6
.=
((0. X),y to_power j) \ ((0. X),y to_power (i + 1))
by BCIALG_2:7
;
then
(((0. X),y to_power j) \ ((0. X),y to_power (i + 1))) \ (((0. X),y to_power j) \ ((0. X),y to_power i)) = 0. X
by A4, A2, A3, BCIALG_1:def 11;
then
(0. X) \ (((0. X),y to_power i) \ ((0. X),y to_power (i + 1))) = 0. X
by BCIALG_1:11;
then A5:
0. X <= ((0. X),y to_power i) \ ((0. X),y to_power (i + 1))
by BCIALG_1:def 11;
((0. X),y to_power i) \ ((0. X),y to_power (i + 1)) =
((0. X),y to_power i) \ (((0. X),y to_power i) \ y)
by BCIALG_2:4
.=
((0. X),y to_power i) \ (((0. X) \ y),y to_power i)
by BCIALG_2:7
;
then
((0. X),y to_power i) \ ((0. X),y to_power (i + 1)) <= (0. X) \ ((0. X) \ y)
by BCIALG_2:21;
then
0. X <= (0. X) \ ((0. X) \ y)
by A5, Th1;
then
(0. X) \ ((0. X) \ ((0. X) \ y)) = 0. X
by BCIALG_1:def 11;
hence
(0. X) \ y = 0. X
by BCIALG_1:8;
verum
end;
then
for x being Element of X holds x ` = 0. X
;
hence
X is BCK-algebra
by BCIALG_1:def 8; verum