let X be BCK-algebra; :: thesis: for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds

A is commutative Ideal of X

let I, A be Ideal of X; :: thesis: ( I c= A & I is commutative Ideal of X implies A is commutative Ideal of X )

assume that

A1: I c= A and

A2: I is commutative Ideal of X ; :: thesis: A is commutative Ideal of X

for x, y being Element of X st x \ y in A holds

x \ (y \ (y \ x)) in A

A is commutative Ideal of X

let I, A be Ideal of X; :: thesis: ( I c= A & I is commutative Ideal of X implies A is commutative Ideal of X )

assume that

A1: I c= A and

A2: I is commutative Ideal of X ; :: thesis: A is commutative Ideal of X

for x, y being Element of X st x \ y in A holds

x \ (y \ (y \ x)) in A

proof

hence
A is commutative Ideal of X
by Th33; :: thesis: verum
let x, y be Element of X; :: thesis: ( x \ y in A implies x \ (y \ (y \ x)) in A )

A3: for x, y, z, u being Element of X st x <= y holds

u \ (z \ x) <= u \ (z \ y)

.= (x \ y) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (x \ y) <= x ;

then y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A3;

then A4: x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5;

(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then (x \ (x \ y)) \ y in I by BCIALG_1:def 18;

then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in I by A2, Th33;

then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1;

then A5: (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7;

assume x \ y in A ; :: thesis: x \ (y \ (y \ x)) in A

then x \ (y \ (y \ (x \ (x \ y)))) in A by A5, BCIALG_1:def 18;

hence x \ (y \ (y \ x)) in A by A4, Th5; :: thesis: verum

end;A3: for x, y, z, u being Element of X st x <= y holds

u \ (z \ x) <= u \ (z \ y)

proof

(x \ (x \ y)) \ x =
(x \ x) \ (x \ y)
by BCIALG_1:7
let x, y, z, u be Element of X; :: thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) )

assume x <= y ; :: thesis: u \ (z \ x) <= u \ (z \ y)

then z \ y <= z \ x by BCIALG_1:5;

hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; :: thesis: verum

end;assume x <= y ; :: thesis: u \ (z \ x) <= u \ (z \ y)

then z \ y <= z \ x by BCIALG_1:5;

hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; :: thesis: verum

.= (x \ y) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (x \ y) <= x ;

then y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A3;

then A4: x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5;

(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then (x \ (x \ y)) \ y in I by BCIALG_1:def 18;

then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in I by A2, Th33;

then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1;

then A5: (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7;

assume x \ y in A ; :: thesis: x \ (y \ (y \ x)) in A

then x \ (y \ (y \ (x \ (x \ y)))) in A by A5, BCIALG_1:def 18;

hence x \ (y \ (y \ x)) in A by A4, Th5; :: thesis: verum