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)
A2: x \ (x \ y) = y \ (y \ x) by ;
(((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
.= (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 Def3; :: thesis: verum
end;
assume A3: X is BCI-algebra of 0 , 0 , 0 , 0 ; :: thesis:
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)
A4: Polynom (0,0,x,y) = Polynom (0,0,y,x) by ;
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
.= (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 ; :: thesis: verum