let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
let X be BCK-algebra of i,j,m,n; :: thesis: ( j = 0 & m > 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
assume A1:
( j = 0 & m > 0 )
; :: thesis: X is BCK-algebra of 0 , 0 , 0 , 0
for x, y being Element of X holds Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x
proof
let x,
y be
Element of
X;
:: thesis: Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x
D1:
Polynom i,
j,
x,
y = Polynom m,
n,
y,
x
by Def2;
B1:
x,
(x \ y) to_power (j + 1) = x,
(x \ y) to_power (m + 1)
by Th8;
B2:
j + 1
< m + 1
by A1, XREAL_1:8;
i + 1
>= j + 1
by A1, XREAL_1:8;
then
x,
(x \ y) to_power (i + 1) = x,
(x \ y) to_power (0 + 1)
by Th06, B1, B2, A1;
hence
Polynom 0 ,
0 ,
x,
y = Polynom 0 ,
n,
y,
x
by A1, Th8, D1;
:: thesis: verum
end;
then reconsider X = X as BCK-algebra of 0 , 0 , 0 ,n by Def2;
C1:
for x, y being Element of X holds Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x
proof
let x,
y be
Element of
X;
:: thesis: Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x
Polynom 0 ,
0 ,
x,
y = Polynom 0 ,
n,
y,
x
by Def2;
hence
Polynom 0 ,
0 ,
x,
y <= Polynom 0 ,
0 ,
y,
x
by Th05;
:: thesis: 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;
:: thesis: Polynom 0 ,0 ,y,x = Polynom 0 ,0 ,x,y
(
Polynom 0 ,
0 ,
y,
x <= Polynom 0 ,
0 ,
x,
y &
Polynom 0 ,
0 ,
x,
y <= Polynom 0 ,
0 ,
y,
x )
by C1;
then
(
(Polynom 0 ,0 ,y,x) \ (Polynom 0 ,0 ,x,y) = 0. X &
(Polynom 0 ,0 ,x,y) \ (Polynom 0 ,0 ,y,x) = 0. X )
by BCIALG_1:def 11;
hence
Polynom 0 ,
0 ,
y,
x = Polynom 0 ,
0 ,
x,
y
by BCIALG_1:def 7;
:: thesis: verum
end;
hence
X is BCK-algebra of 0 , 0 , 0 , 0
by Def2; :: thesis: verum