let n be Element of NAT ; :: thesis: 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; :: thesis: ( 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) )
:: thesis: ( ( 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
;
:: thesis: 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;
:: thesis: x,y to_power (n + 1) = x,y to_power (n + 2)
B1:
Polynom n,
(n + 1),
x,
(x \ y) = Polynom n,
(n + 1),
(x \ y),
x
by A1, Def2;
B2:
(x \ y) \ x =
(x \ x) \ y
by BCIALG_1:7
.=
y `
by BCIALG_1:def 5
.=
0. X
by BCIALG_1:def 8
;
B3:
(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 B2, BCIALG_2:8
.=
x,
y to_power (n + 1)
by BCIALG_2:5
;
((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 B2, 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
;
hence
x,
y to_power (n + 1) = x,
y to_power (n + 2)
by B1, B3;
:: thesis: verum
end;
hence
for
x,
y being
Element of
X holds
x,
y to_power (n + 1) = x,
y to_power (n + 2)
;
:: thesis: verum
end;
assume A1:
for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2)
; :: thesis: 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;
:: thesis: Polynom n,(n + 1),x,y = Polynom n,(n + 1),y,x
B1:
x,
(x \ y) to_power (n + 1) = x,
(x \ y) to_power (n + 2)
by A1;
(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
by BCIALG_1:def 11;
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
x,
(x \ y) to_power (1 + (n + 1)) <= y,
(x \ y) to_power (n + 1)
by BCIALG_2:10;
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 B1, BCIALG_2:19;
then B2:
(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;
B3:
y,
(y \ x) to_power (n + 1) = y,
(y \ x) to_power (n + 2)
by A1;
(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
by BCIALG_1:def 11;
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
y,
(y \ x) to_power (1 + (n + 1)) <= x,
(y \ x) to_power (n + 1)
by BCIALG_2:10;
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 B3, BCIALG_2:19;
then
(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;
hence
Polynom n,
(n + 1),
x,
y = Polynom n,
(n + 1),
y,
x
by B2, Th02;
:: thesis: verum
end;
hence
X is BCK-algebra of n,n + 1,n,n + 1
by Def2; :: thesis: verum