let i, j, m, n be Nat; for X being BCK-algebra of i,j,m,n st n = 0 & i <> 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
let X be BCK-algebra of i,j,m,n; ( n = 0 & i <> 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
assume that
A1:
n = 0
and
A2:
i <> 0
; X is BCK-algebra of 0 , 0 , 0 , 0
for x, y being Element of X holds Polynom (0,j,x,y) = Polynom (0,0,y,x)
proof
let x,
y be
Element of
X;
Polynom (0,j,x,y) = Polynom (0,0,y,x)
A3:
Polynom (
i,
j,
x,
y)
= Polynom (
m,
n,
y,
x)
by Def3;
A4:
m + 1
>= n + 1
by A1, XREAL_1:6;
( (
y,
(y \ x))
to_power (n + 1) = (
y,
(y \ x))
to_power (i + 1) &
n + 1
< i + 1 )
by A1, A2, Th19, XREAL_1:6;
then
(
y,
(y \ x))
to_power (m + 1) = (
y,
(y \ x))
to_power (0 + 1)
by A1, A4, Th6;
hence
Polynom (
0,
j,
x,
y)
= Polynom (
0,
0,
y,
x)
by A1, A3, Th19;
verum
end;
then reconsider X = X as BCK-algebra of 0 ,j, 0 , 0 by Def3;
A5:
for x, y being Element of X holds Polynom (0,0,y,x) <= Polynom (0,0,x,y)
proof
let x,
y be
Element of
X;
Polynom (0,0,y,x) <= Polynom (0,0,x,y)
Polynom (
0,
j,
x,
y)
= Polynom (
0,
0,
y,
x)
by Def3;
hence
Polynom (
0,
0,
y,
x)
<= Polynom (
0,
0,
x,
y)
by Th5;
verum
end;
for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y)
proof
let x,
y be
Element of
X;
Polynom (0,0,y,x) = Polynom (0,0,x,y)
Polynom (
0,
0,
x,
y)
<= Polynom (
0,
0,
y,
x)
by A5;
then A6:
(Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X
;
Polynom (
0,
0,
y,
x)
<= Polynom (
0,
0,
x,
y)
by A5;
then
(Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X
;
hence
Polynom (
0,
0,
y,
x)
= Polynom (
0,
0,
x,
y)
by A6, BCIALG_1:def 7;
verum
end;
hence
X is BCK-algebra of 0 , 0 , 0 , 0
by Def3; verum