let X be BCI-algebra; :: thesis: ( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 )
thus
( X is commutative BCK-algebra implies X is BCI-algebra of 0 , 0 , 0 , 0 )
:: thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is commutative BCK-algebra )proof
assume A1:
X is
commutative BCK-algebra
;
:: thesis: X is BCI-algebra of 0 , 0 , 0 , 0
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
B1:
x \ (x \ y) = y \ (y \ x)
by A1, BCIALG_3:def 1;
(x,(x \ y) to_power 1),
(y \ x) to_power 0 =
x,
(x \ y) to_power 1
by BCIALG_2:1
.=
y \ (y \ x)
by B1, BCIALG_2:2
.=
y,
(y \ x) to_power 1
by BCIALG_2:2
.=
(y,(y \ x) to_power 1),
(x \ y) to_power 0
by BCIALG_2:1
;
hence
Polynom 0 ,
0 ,
x,
y = Polynom 0 ,
0 ,
y,
x
;
:: thesis: verum
end;
hence
X is
BCI-algebra of
0 ,
0 ,
0 ,
0
by Def2;
:: thesis: verum
end;
assume A1:
X is BCI-algebra of 0 , 0 , 0 , 0
; :: thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x,
y be
Element of
X;
:: thesis: x \ (x \ y) = y \ (y \ x)
B1:
Polynom 0 ,
0 ,
x,
y = Polynom 0 ,
0 ,
y,
x
by A1, Def2;
x \ (x \ y) =
x,
(x \ y) to_power 1
by BCIALG_2:2
.=
(y,(y \ x) to_power 1),
(x \ y) to_power 0
by B1, BCIALG_2:1
.=
y,
(y \ x) to_power 1
by BCIALG_2:1
.=
y \ (y \ x)
by BCIALG_2:2
;
hence
x \ (x \ y) = y \ (y \ x)
;
:: thesis: verum
end;
hence
X is commutative BCK-algebra
by A1, Th40, BCIALG_3:def 1; :: thesis: verum