let n be Nat; for X being quasi-commutative BCK-algebra holds
( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) )
let X be quasi-commutative BCK-algebra; ( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) )
thus
( X is BCK-algebra of n,n + 1,n,n + 1 implies for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) )
( ( for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) implies X is BCK-algebra of n,n + 1,n,n + 1 )proof
assume A1:
X is
BCK-algebra of
n,
n + 1,
n,
n + 1
;
for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2)
for
x,
y being
Element of
X holds (
x,
y)
to_power (n + 1) = (
x,
y)
to_power (n + 2)
proof
let x,
y be
Element of
X;
(x,y) to_power (n + 1) = (x,y) to_power (n + 2)
A2:
(x \ y) \ x =
(x \ x) \ y
by BCIALG_1:7
.=
y `
by BCIALG_1:def 5
.=
0. X
by BCIALG_1:def 8
;
then A3: (
((x,(x \ (x \ y))) to_power (n + 1)),
((x \ y) \ x))
to_power (n + 1) =
(
((x,y) to_power (n + 1)),
(0. X))
to_power (n + 1)
by BCIALG_2:8
.=
(
x,
y)
to_power (n + 1)
by BCIALG_2:5
;
A4: (
(((x \ y),((x \ y) \ x)) to_power (n + 1)),
(x \ (x \ y)))
to_power (n + 1) =
(
(x \ y),
(x \ (x \ y)))
to_power (n + 1)
by A2, BCIALG_2:5
.=
((x,(x \ (x \ y))) to_power (n + 1)) \ y
by BCIALG_2:7
.=
((x,y) to_power (n + 1)) \ y
by BCIALG_2:8
.=
(
x,
y)
to_power ((n + 1) + 1)
by BCIALG_2:4
;
Polynom (
n,
(n + 1),
x,
(x \ y))
= Polynom (
n,
(n + 1),
(x \ y),
x)
by A1, Def3;
hence
(
x,
y)
to_power (n + 1) = (
x,
y)
to_power (n + 2)
by A3, A4;
verum
end;
hence
for
x,
y being
Element of
X holds (
x,
y)
to_power (n + 1) = (
x,
y)
to_power (n + 2)
;
verum
end;
assume A5:
for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2)
; X is BCK-algebra of n,n + 1,n,n + 1
for x, y being Element of X holds Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x)
proof
let x,
y be
Element of
X;
Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x)
(x \ y) \ (x \ y) = 0. X
by BCIALG_1:def 5;
then
(x \ (x \ y)) \ y = 0. X
by BCIALG_1:7;
then
x \ (x \ y) <= y
;
then
(
(x \ (x \ y)),
(x \ y))
to_power (n + 1) <= (
y,
(x \ y))
to_power (n + 1)
by BCIALG_2:19;
then
(
((x,(x \ y)) to_power 1),
(x \ y))
to_power (n + 1) <= (
y,
(x \ y))
to_power (n + 1)
by BCIALG_2:2;
then A6:
(
x,
(x \ y))
to_power (1 + (n + 1)) <= (
y,
(x \ y))
to_power (n + 1)
by BCIALG_2:10;
(y \ x) \ (y \ x) = 0. X
by BCIALG_1:def 5;
then
(y \ (y \ x)) \ x = 0. X
by BCIALG_1:7;
then
y \ (y \ x) <= x
;
then
(
(y \ (y \ x)),
(y \ x))
to_power (n + 1) <= (
x,
(y \ x))
to_power (n + 1)
by BCIALG_2:19;
then
(
((y,(y \ x)) to_power 1),
(y \ x))
to_power (n + 1) <= (
x,
(y \ x))
to_power (n + 1)
by BCIALG_2:2;
then A7:
(
y,
(y \ x))
to_power (1 + (n + 1)) <= (
x,
(y \ x))
to_power (n + 1)
by BCIALG_2:10;
(
y,
(y \ x))
to_power (n + 1) = (
y,
(y \ x))
to_power (n + 2)
by A5;
then
(
((y,(y \ x)) to_power (n + 1)),
(x \ y))
to_power (n + 1) <= (
((x,(y \ x)) to_power (n + 1)),
(x \ y))
to_power (n + 1)
by A7, BCIALG_2:19;
then A8:
(
((y,(y \ x)) to_power (n + 1)),
(x \ y))
to_power (n + 1) <= (
((x,(x \ y)) to_power (n + 1)),
(y \ x))
to_power (n + 1)
by BCIALG_2:11;
(
x,
(x \ y))
to_power (n + 1) = (
x,
(x \ y))
to_power (n + 2)
by A5;
then
(
((x,(x \ y)) to_power (n + 1)),
(y \ x))
to_power (n + 1) <= (
((y,(x \ y)) to_power (n + 1)),
(y \ x))
to_power (n + 1)
by A6, BCIALG_2:19;
then
(
((x,(x \ y)) to_power (n + 1)),
(y \ x))
to_power (n + 1) <= (
((y,(y \ x)) to_power (n + 1)),
(x \ y))
to_power (n + 1)
by BCIALG_2:11;
hence
Polynom (
n,
(n + 1),
x,
y)
= Polynom (
n,
(n + 1),
y,
x)
by A8, Th2;
verum
end;
hence
X is BCK-algebra of n,n + 1,n,n + 1
by Def3; verum