:: BCIIDEAL semantic presentation
begin
theorem :: BCIIDEAL:1
for X being BCI-algebra
for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
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;
theorem :: BCIIDEAL:2
for X being BCI-algebra
for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
let x, y, z, u be Element of X; ::_thesis: (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
((x \ (y \ z)) \ (x \ (y \ u))) \ ((y \ u) \ (y \ z)) = 0. X by BCIALG_1:1;
then (x \ (y \ z)) \ (x \ (y \ u)) <= (y \ u) \ (y \ z) by BCIALG_1:def_11;
then A1: ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= ((y \ u) \ (y \ z)) \ (z \ u) by BCIALG_1:5;
((y \ u) \ (y \ z)) \ (z \ u) = ((y \ u) \ (z \ u)) \ (y \ z) by BCIALG_1:7;
then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= 0. X by A1, BCIALG_1:def_3;
then (((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u)) \ (0. X) = 0. X by BCIALG_1:def_11;
then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) = 0. X by BCIALG_1:2;
hence (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u by BCIALG_1:def_11; ::_thesis: verum
end;
theorem :: BCIIDEAL:3
for X being BCI-algebra
for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
let x, y, z, u, v be Element of X; ::_thesis: (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((y \ (z \ v)) \ (y \ (z \ u))) = 0. X by BCIALG_1:1;
then (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (y \ (z \ v)) \ (y \ (z \ u)) by BCIALG_1:def_11;
then A1: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= ((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) by BCIALG_1:5;
((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) = ((y \ (z \ v)) \ ((z \ u) \ (z \ v))) \ (y \ (z \ u)) by BCIALG_1:7;
then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= 0. X by A1, BCIALG_1:def_3;
then (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v))) \ (0. X) = 0. X by BCIALG_1:def_11;
then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) = 0. X by BCIALG_1:2;
then (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (z \ u) \ (z \ v) by BCIALG_1:def_11;
then A2: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) <= ((z \ u) \ (z \ v)) \ (v \ u) by BCIALG_1:5;
((z \ u) \ (z \ v)) \ (v \ u) = ((z \ u) \ (v \ u)) \ (z \ v) by BCIALG_1:7
.= 0. X by BCIALG_1:def_3 ;
then (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u)) \ (0. X) = 0. X by A2, BCIALG_1:def_11;
then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) = 0. X by BCIALG_1:2;
hence (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u by BCIALG_1:def_11; ::_thesis: verum
end;
theorem :: BCIIDEAL:4
for X being BCI-algebra
for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
let x, y be Element of X; ::_thesis: ((0. X) \ (x \ y)) \ (y \ x) = 0. X
(((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((0. X) \ x) \ (y \ x)) \ ((0. X) \ y) by BCIALG_1:7;
then A1: (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((y \ x) `) \ x) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ (x `)) \ x) \ ((0. X) \ y) by BCIALG_1:9
.= (((y `) \ x) \ (x `)) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ x) \ (y `)) \ (x `) by BCIALG_1:7
.= (((y `) \ (y `)) \ x) \ (x `) by BCIALG_1:7
.= (x `) \ (x `) by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_5 ;
((0. X) \ (x \ y)) \ (y \ x) = ((x \ y) `) \ (y \ x)
.= ((x `) \ (y `)) \ (y \ x) by BCIALG_1:9
.= (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) ;
hence ((0. X) \ (x \ y)) \ (y \ x) = 0. X by A1; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let a be Element of X;
func initial_section a -> set equals :: BCIIDEAL:def 1
{ x where x is Element of X : x <= a } ;
coherence
{ x where x is Element of X : x <= a } is set ;
end;
:: deftheorem defines initial_section BCIIDEAL:def_1_:_
for X being BCI-algebra
for a being Element of X holds initial_section a = { x where x is Element of X : x <= a } ;
theorem Th5: :: BCIIDEAL:5
for X being BCI-algebra
for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
let A be Ideal of X; ::_thesis: for x being Element of X
for a being Element of A st x <= a holds
x in A
let x be Element of X; ::_thesis: for a being Element of A st x <= a holds
x in A
let a be Element of A; ::_thesis: ( x <= a implies x in A )
assume x <= a ; ::_thesis: x in A
then x \ a = 0. X by BCIALG_1:def_11;
then x \ a in A by BCIALG_1:def_18;
hence x in A by BCIALG_1:def_18; ::_thesis: verum
end;
theorem :: BCIIDEAL:6
for X being BCI-algebra
for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof
let X be BCI-algebra; ::_thesis: for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let x, a, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume x is Element of BranchV b ; ::_thesis: a \ x = a \ b
then x in BranchV b ;
then ex x3 being Element of X st
( x = x3 & b <= x3 ) ;
then A1: b \ x = 0. X by BCIALG_1:def_11;
x in { x1 where x1 is Element of X : x1 is minimal } ;
then ex x1 being Element of X st
( x = x1 & x1 is minimal ) ;
hence a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum
end;
theorem :: BCIIDEAL:7
for X being BCI-algebra
for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof
let X be BCI-algebra; ::_thesis: for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let a be Element of X; ::_thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
let x, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume x is Element of BranchV b ; ::_thesis: a \ x = a \ b
then x in BranchV b ;
then ex x3 being Element of X st
( x = x3 & b <= x3 ) ;
then A1: b \ x = 0. X by BCIALG_1:def_11;
x in { x1 where x1 is Element of X : x1 is minimal } ;
then ex x1 being Element of X st
( x = x1 & x1 is minimal ) ;
hence a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum
end;
theorem :: BCIIDEAL:8
for X being BCI-algebra
for A being Ideal of X
for a being Element of A holds initial_section a c= A
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X
for a being Element of A holds initial_section a c= A
let A be Ideal of X; ::_thesis: for a being Element of A holds initial_section a c= A
let a be Element of A; ::_thesis: initial_section a c= A
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in initial_section a or b in A )
assume b in initial_section a ; ::_thesis: b in A
then ex x1 being Element of X st
( b = x1 & x1 <= a ) ;
hence b in A by Th5; ::_thesis: verum
end;
theorem :: BCIIDEAL:9
for X being BCI-algebra st AtomSet X is Ideal of X holds
for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
proof
let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X )
set B = BCK-part X;
set P = AtomSet X;
A1: for x being Element of X holds
( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )
proof
let x be Element of X; ::_thesis: ( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )
( 0. X in BCK-part X & 0. X in AtomSet X ) by BCIALG_1:19;
then 0. X in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4;
hence ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) by TARSKI:def_1; ::_thesis: ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} )
thus ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) ::_thesis: verum
proof
assume A2: x in (BCK-part X) /\ (AtomSet X) ; ::_thesis: x in {(0. X)}
then x in BCK-part X by XBOOLE_0:def_4;
then ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
then A3: (0. X) \ x = 0. X by BCIALG_1:def_11;
x in { x2 where x2 is Element of X : x2 is minimal } by A2, XBOOLE_0:def_4;
then ex x2 being Element of X st
( x = x2 & x2 is minimal ) ;
then 0. X = x by A3, BCIALG_1:def_14;
hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
end;
assume A4: AtomSet X is Ideal of X ; ::_thesis: for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
proof
let x be Element of BCK-part X; ::_thesis: for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
let a be Element of AtomSet X; ::_thesis: ( x \ a in AtomSet X implies x = 0. X )
assume x \ a in AtomSet X ; ::_thesis: x = 0. X
then x in AtomSet X by A4, BCIALG_1:def_18;
then x in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4;
then x in {(0. X)} by A1;
hence x = 0. X by TARSKI:def_1; ::_thesis: verum
end;
hence for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X ; ::_thesis: verum
end;
theorem :: BCIIDEAL:10
for X being BCI-algebra st AtomSet X is Ideal of X holds
AtomSet X is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies AtomSet X is closed Ideal of X )
set P = AtomSet X;
A1: for x being Element of AtomSet X holds x ` in AtomSet X
proof
let x be Element of AtomSet X; ::_thesis: x ` in AtomSet X
x ` is minimal by BCIALG_2:30;
hence x ` in AtomSet X ; ::_thesis: verum
end;
assume AtomSet X is Ideal of X ; ::_thesis: AtomSet X is closed Ideal of X
hence AtomSet X is closed Ideal of X by A1, BCIALG_1:def_19; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let I be Ideal of X;
attrI is positive means :: BCIIDEAL:def 2
for x being Element of I holds x is positive ;
end;
:: deftheorem defines positive BCIIDEAL:def_2_:_
for X being BCI-algebra
for I being Ideal of X holds
( I is positive iff for x being Element of I holds x is positive );
theorem :: BCIIDEAL:11
for X being BCK-algebra
for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
proof
let X be BCK-algebra; ::_thesis: for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
let A, I be Ideal of X; ::_thesis: ( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
thus ( A /\ I = {(0. X)} implies for x being Element of A
for y being Element of I holds x \ y = x ) ::_thesis: ( ( for x being Element of A
for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} )
proof
assume A1: A /\ I = {(0. X)} ; ::_thesis: for x being Element of A
for y being Element of I holds x \ y = x
let x be Element of A; ::_thesis: for y being Element of I holds x \ y = x
let y be Element of I; ::_thesis: x \ y = x
(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
then x \ (x \ y) <= y by BCIALG_1:def_11;
then A2: x \ (x \ y) in I by Th5;
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (x \ y) <= x by BCIALG_1:def_11;
then x \ (x \ y) in A by Th5;
then x \ (x \ y) in {(0. X)} by A1, A2, XBOOLE_0:def_4;
then A3: x \ (x \ y) = 0. X by TARSKI:def_1;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ y = x by A3, BCIALG_1:def_7; ::_thesis: verum
end;
thus ( ( for x being Element of A
for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) ::_thesis: verum
proof
assume A4: for x being Element of A
for y being Element of I holds x \ y = x ; ::_thesis: A /\ I = {(0. X)}
thus A /\ I c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= A /\ I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ I or x in {(0. X)} )
assume A5: x in A /\ I ; ::_thesis: x in {(0. X)}
then reconsider xxx = x as Element of A by XBOOLE_0:def_4;
reconsider xx = x as Element of I by A5, XBOOLE_0:def_4;
xxx \ xx = xxx by A4;
then x = 0. X by BCIALG_1:def_5;
hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in A /\ I )
assume x in {(0. X)} ; ::_thesis: x in A /\ I
then A6: x = 0. X by TARSKI:def_1;
( 0. X in A & 0. X in I ) by BCIALG_1:def_18;
hence x in A /\ I by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
theorem :: BCIIDEAL:12
for X being associative BCI-algebra
for A being Ideal of X holds A is closed
proof
let X be associative BCI-algebra; ::_thesis: for A being Ideal of X holds A is closed
let A be Ideal of X; ::_thesis: A is closed
for x being Element of A holds x ` in A
proof
let x be Element of A; ::_thesis: x ` in A
(0. X) \ x = x \ (0. X) by BCIALG_1:48
.= x by BCIALG_1:2 ;
hence x ` in A ; ::_thesis: verum
end;
hence A is closed by BCIALG_1:def_19; ::_thesis: verum
end;
theorem :: BCIIDEAL:13
for X being BCI-algebra
for A being Ideal of X st X is quasi-associative holds
A is closed
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X st X is quasi-associative holds
A is closed
let A be Ideal of X; ::_thesis: ( X is quasi-associative implies A is closed )
assume A1: X is quasi-associative ; ::_thesis: A is closed
for x being Element of A holds x ` in A
proof
let x be Element of A; ::_thesis: x ` in A
x ` <= x by A1, BCIALG_1:71;
hence x ` in A by Th5; ::_thesis: verum
end;
hence A is closed by BCIALG_1:def_19; ::_thesis: verum
end;
begin
definition
let X be BCI-algebra;
let IT be Ideal of X;
attrIT is associative means :Def3: :: BCIIDEAL:def 3
( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) );
end;
:: deftheorem Def3 defines associative BCIIDEAL:def_3_:_
for X being BCI-algebra
for IT being Ideal of X holds
( IT is associative iff ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) ) );
registration
let X be BCI-algebra;
cluster non empty associative for Ideal of X;
existence
ex b1 being Ideal of X st b1 is associative
proof
take Y = {(0. X)}; ::_thesis: ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative )
reconsider YY = Y as Ideal of X by BCIALG_1:43;
A1: 0. X in YY by TARSKI:def_1;
for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x = 0. X
proof
let x, y, z be Element of X; ::_thesis: ( x \ (y \ z) in YY & y \ z in YY implies x = 0. X )
assume ( x \ (y \ z) in YY & y \ z in YY ) ; ::_thesis: x = 0. X
then ( x \ (y \ z) = 0. X & y \ z = 0. X ) by TARSKI:def_1;
hence x = 0. X by BCIALG_1:2; ::_thesis: verum
end;
then for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x in YY by A1;
hence ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) by A1, Def3; ::_thesis: verum
end;
end;
definition
let X be BCI-algebra;
mode associative-ideal of X -> non empty Subset of X means :Def4: :: BCIIDEAL:def 4
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
x in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x in X1 ) )
X1 c= the carrier of X ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines associative-ideal BCIIDEAL:def_4_:_
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is associative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x in b2 ) ) );
theorem :: BCIIDEAL:14
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X
proof
let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X
let X1 be non empty Subset of X; ::_thesis: ( X1 is associative-ideal of X implies X1 is Ideal of X )
assume A1: X1 is associative-ideal of X ; ::_thesis: X1 is Ideal of X
A2: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1
proof
let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume ( x \ y in X1 & y in X1 ) ; ::_thesis: x in X1
then ( (x \ y) \ (0. X) in X1 & y \ (0. X) in X1 ) by BCIALG_1:2;
hence x in X1 by A1, Def4; ::_thesis: verum
end;
0. X in X1 by A1, Def4;
hence X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum
end;
theorem Th15: :: BCIIDEAL:15
for X being BCI-algebra
for I being Ideal of X holds
( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
let I be Ideal of X; ::_thesis: ( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
thus ( I is associative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ) implies I is associative-ideal of X )
proof
assume A1: I is associative-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies x \ (y \ z) in I )
assume A2: (x \ y) \ z in I ; ::_thesis: x \ (y \ z) in I
(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
then x \ (x \ y) <= y by BCIALG_1:def_11;
then (x \ (x \ y)) \ (y \ z) <= y \ (y \ z) by BCIALG_1:5;
then A3: ((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;
(y \ (y \ z)) \ z = 0. X by BCIALG_1:1;
then (((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X by A3, BCIALG_1:def_11;
then ((x \ (x \ y)) \ (y \ z)) \ z = 0. X by BCIALG_1:2;
then ((x \ (x \ y)) \ (y \ z)) \ z in I by A1, Def4;
then ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:7;
hence x \ (y \ z) in I by A1, A2, Def4; ::_thesis: verum
end;
assume A4: for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ; ::_thesis: I is associative-ideal of X
A5: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x in I )
assume that
A6: (x \ y) \ z in I and
A7: y \ z in I ; ::_thesis: x in I
x \ (y \ z) in I by A4, A6;
hence x in I by A7, BCIALG_1:def_18; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is associative-ideal of X by A5, Def4; ::_thesis: verum
end;
theorem :: BCIIDEAL:16
for X being BCI-algebra
for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
let I be Ideal of X; ::_thesis: ( I is associative-ideal of X implies for x being Element of X holds x \ ((0. X) \ x) in I )
assume A1: I is associative-ideal of X ; ::_thesis: for x being Element of X holds x \ ((0. X) \ x) in I
let x be Element of X; ::_thesis: x \ ((0. X) \ x) in I
x \ x = 0. X by BCIALG_1:def_5;
then A2: (x \ (0. X)) \ x = 0. X by BCIALG_1:2;
0. X in I by A1, Def4;
hence x \ ((0. X) \ x) in I by A1, A2, Th15; ::_thesis: verum
end;
theorem :: BCIIDEAL:17
for X being BCI-algebra
for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
let I be Ideal of X; ::_thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X )
assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; ::_thesis: I is closed Ideal of X
for x1 being Element of I holds x1 ` in I
proof
let x1 be Element of I; ::_thesis: x1 ` in I
((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8;
then ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7;
then ((0. X) \ x1) \ x1 in I by A1;
hence x1 ` in I by BCIALG_1:def_18; ::_thesis: verum
end;
hence I is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum
end;
definition
let X be BCI-algebra;
mode p-ideal of X -> non empty Subset of X means :Def5: :: BCIIDEAL:def 5
( 0. X in it & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in it & y in it holds
x in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b1 & y in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) )
X1 c= X1 ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines p-ideal BCIIDEAL:def_5_:_
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is p-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b2 & y in b2 holds
x in b2 ) ) );
theorem :: BCIIDEAL:18
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
proof
let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
let X1 be non empty Subset of X; ::_thesis: ( X1 is p-ideal of X implies X1 is Ideal of X )
assume A1: X1 is p-ideal of X ; ::_thesis: X1 is Ideal of X
A2: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1
proof
let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume that
A3: x \ y in X1 and
A4: y in X1 ; ::_thesis: x in X1
(x \ (0. X)) \ y in X1 by A3, BCIALG_1:2;
then (x \ (0. X)) \ (y \ (0. X)) in X1 by BCIALG_1:2;
hence x in X1 by A1, A4, Def5; ::_thesis: verum
end;
0. X in X1 by A1, Def5;
hence X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum
end;
theorem Th19: :: BCIIDEAL:19
for X being BCI-algebra
for I being Ideal of X st I is p-ideal of X holds
BCK-part X c= I
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is p-ideal of X holds
BCK-part X c= I
let I be Ideal of X; ::_thesis: ( I is p-ideal of X implies BCK-part X c= I )
assume A1: I is p-ideal of X ; ::_thesis: BCK-part X c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BCK-part X or x in I )
assume A2: x in BCK-part X ; ::_thesis: x in I
then A3: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
reconsider x = x as Element of X by A2;
(0. X) \ x = 0. X by A3, BCIALG_1:def_11;
then (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2;
then A4: (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def_5;
0. X in I by A1, Def5;
hence x in I by A1, A4, Def5; ::_thesis: verum
end;
theorem :: BCIIDEAL:20
for X being BCI-algebra holds BCK-part X is p-ideal of X
proof
let X be BCI-algebra; ::_thesis: BCK-part X is p-ideal of X
set A = BCK-part X;
A1: now__::_thesis:_for_x,_y,_z_being_Element_of_X_st_(x_\_z)_\_(y_\_z)_in_BCK-part_X_&_y_in_BCK-part_X_holds_
x_in_BCK-part_X
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: (x \ z) \ (y \ z) in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
ex c being Element of X st
( (x \ z) \ (y \ z) = c & 0. X <= c ) by A2;
then ((x \ z) \ (y \ z)) ` = 0. X by BCIALG_1:def_11;
then ((x \ z) `) \ ((y \ z) `) = 0. X by BCIALG_1:9;
then A4: ((x `) \ (z `)) \ ((y \ z) `) = 0. X by BCIALG_1:9;
ex d being Element of X st
( y = d & 0. X <= d ) by A3;
then y ` = 0. X by BCIALG_1:def_11;
then (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = ((x `) \ (0. X)) ` by A4, BCIALG_1:9;
then (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = (x `) ` by BCIALG_1:2;
then 0. X = (0. X) \ ((0. X) \ x) by BCIALG_1:def_3;
then (0. X) \ x = 0. X by BCIALG_1:1;
then 0. X <= x by BCIALG_1:def_11;
hence x in BCK-part X ; ::_thesis: verum
end;
(0. X) \ (0. X) = 0. X by BCIALG_1:def_5;
then 0. X <= 0. X by BCIALG_1:def_11;
then 0. X in BCK-part X ;
hence BCK-part X is p-ideal of X by A1, Def5; ::_thesis: verum
end;
theorem Th21: :: BCIIDEAL:21
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
thus ( I is p-ideal of X implies for x, y being Element of X st x in I & x <= y holds
y in I ) ::_thesis: ( ( for x, y being Element of X st x in I & x <= y holds
y in I ) implies I is p-ideal of X )
proof
assume I is p-ideal of X ; ::_thesis: for x, y being Element of X st x in I & x <= y holds
y in I
then A1: BCK-part X c= I by Th19;
let x, y be Element of X; ::_thesis: ( x in I & x <= y implies y in I )
assume that
A2: x in I and
A3: x <= y ; ::_thesis: y in I
A4: x \ y = 0. X by A3, BCIALG_1:def_11;
then (y \ x) ` = x \ y by BCIALG_1:6;
then 0. X <= y \ x by A4, BCIALG_1:def_11;
then y \ x in BCK-part X ;
hence y in I by A2, A1, BCIALG_1:def_18; ::_thesis: verum
end;
assume A5: for x, y being Element of X st x in I & x <= y holds
y in I ; ::_thesis: I is p-ideal of X
A6: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )
assume that
A7: (x \ z) \ (y \ z) in I and
A8: y in I ; ::_thesis: x in I
((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3;
then (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11;
then x \ y in I by A5, A7;
hence x in I by A8, BCIALG_1:def_18; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is p-ideal of X by A6, Def5; ::_thesis: verum
end;
theorem :: BCIIDEAL:22
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
thus ( I is p-ideal of X implies for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ) implies I is p-ideal of X )
proof
assume A1: I is p-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I implies x \ y in I )
assume A2: (x \ z) \ (y \ z) in I ; ::_thesis: x \ y in I
((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3;
then (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11;
hence x \ y in I by A1, A2, Th21; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ; ::_thesis: I is p-ideal of X
A4: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )
assume that
A5: (x \ z) \ (y \ z) in I and
A6: y in I ; ::_thesis: x in I
x \ y in I by A3, A5;
hence x in I by A6, BCIALG_1:def_18; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is p-ideal of X by A4, Def5; ::_thesis: verum
end;
begin
definition
let X be BCK-algebra;
let IT be Ideal of X;
attrIT is commutative means :Def6: :: BCIIDEAL:def 6
for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT;
end;
:: deftheorem Def6 defines commutative BCIIDEAL:def_6_:_
for X being BCK-algebra
for IT being Ideal of X holds
( IT is commutative iff for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT );
registration
let X be BCK-algebra;
cluster non empty commutative for Ideal of X;
existence
ex b1 being Ideal of X st b1 is commutative
proof
set X1 = BCK-part X;
take BCK-part X ; ::_thesis: ( BCK-part X is Ideal of X & BCK-part X is commutative )
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then A4: y ` = 0. X by BCIALG_1:def_11;
ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then (x \ y) ` = 0. X by BCIALG_1:def_11;
then (x `) \ (0. X) = 0. X by A4, BCIALG_1:9;
then (0. X) \ x = 0. X by BCIALG_1:2;
then 0. X <= x by BCIALG_1:def_11;
hence x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
(x \ y) \ z in BCK-part X and
z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
0. X in BCK-part X by BCIALG_1:19;
then BCK-part X is Ideal of X by A1, BCIALG_1:def_18;
hence ( BCK-part X is Ideal of X & BCK-part X is commutative ) by A5, Def6; ::_thesis: verum
end;
end;
theorem :: BCIIDEAL:23
for X being BCK-algebra holds BCK-part X is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: BCK-part X is commutative Ideal of X
set B = BCK-part X;
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then (x \ y) ` = 0. X by BCIALG_1:def_11;
then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;
ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11;
then (0. X) \ x = 0. X by BCIALG_1:2;
then 0. X <= x by BCIALG_1:def_11;
hence x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
(x \ y) \ z in BCK-part X and
z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
0. X in BCK-part X by BCIALG_1:19;
hence BCK-part X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum
end;
theorem :: BCIIDEAL:24
for X being BCK-algebra st X is p-Semisimple BCI-algebra holds
{(0. X)} is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies {(0. X)} is commutative Ideal of X )
set X1 = {(0. X)};
A1: {(0. X)} c= the carrier of X
proof
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in {(0. X)} or xx in the carrier of X )
assume xx in {(0. X)} ; ::_thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def_1;
hence xx in the carrier of X ; ::_thesis: verum
end;
A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
x in {(0. X)}
proof
set X1 = {(0. X)};
let x, y be Element of X; ::_thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; ::_thesis: x in {(0. X)}
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1;
then x = 0. X by BCIALG_1:2;
hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
0. X in {(0. X)} by TARSKI:def_1;
then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def_18;
assume A3: X is p-Semisimple BCI-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X
for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds
x \ (y \ (y \ x)) in X1
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in X1 & z in X1 implies x \ (y \ (y \ x)) in X1 )
assume ( (x \ y) \ z in X1 & z in X1 ) ; ::_thesis: x \ (y \ (y \ x)) in X1
then ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def_1;
then A4: x \ y = 0. X by BCIALG_1:2;
y is atom by A3, BCIALG_1:52;
then x = y by A4, BCIALG_1:def_14;
then x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def_5;
then x \ (y \ (y \ x)) = x \ x by BCIALG_1:2;
then x \ (y \ (y \ x)) = 0. X by BCIALG_1:def_5;
hence x \ (y \ (y \ x)) in X1 by TARSKI:def_1; ::_thesis: verum
end;
hence {(0. X)} is commutative Ideal of X by Def6; ::_thesis: verum
end;
Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part X
proof
let X be BCK-algebra; ::_thesis: the carrier of X c= BCK-part X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of X or x in BCK-part X )
assume x in the carrier of X ; ::_thesis: x in BCK-part X
then consider x1 being Element of X such that
A1: x = x1 ;
x1 ` = 0. X by BCIALG_1:def_8;
then 0. X <= x1 by BCIALG_1:def_11;
hence x in BCK-part X by A1; ::_thesis: verum
end;
theorem Th25: :: BCIIDEAL:25
for X being BCK-algebra holds BCK-part X = the carrier of X
proof
let X be BCK-algebra; ::_thesis: BCK-part X = the carrier of X
the carrier of X c= BCK-part X by Lm1;
hence BCK-part X = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: BCIIDEAL:26
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:13;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:27
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:14;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:28
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:12;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:29
for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:15;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:30
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:16;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:31
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; ::_thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:17;
hence the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;
theorem :: BCIIDEAL:32
for X being BCK-algebra holds the carrier of X is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: the carrier of X is commutative Ideal of X
set B = BCK-part X;
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then (x \ y) ` = 0. X by BCIALG_1:def_11;
then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;
ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11;
then (0. X) \ x = 0. X by BCIALG_1:2;
then 0. X <= x by BCIALG_1:def_11;
hence x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
(x \ y) \ z in BCK-part X and
z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
the carrier of X = BCK-part X by Th25;
hence the carrier of X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum
end;
theorem Th33: :: BCIIDEAL:33
for X being BCK-algebra
for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
let I be Ideal of X; ::_thesis: ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
thus ( I is commutative Ideal of X implies for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) ::_thesis: ( ( for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) implies I is commutative Ideal of X )
proof
A1: 0. X in I by BCIALG_1:def_18;
assume A2: I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I
let x, y be Element of X; ::_thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )
assume x \ y in I ; ::_thesis: x \ (y \ (y \ x)) in I
then (x \ y) \ (0. X) in I by BCIALG_1:2;
hence x \ (y \ (y \ x)) in I by A2, A1, Def6; ::_thesis: verum
end;
assume A3: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ; ::_thesis: I is commutative Ideal of X
for x, y, z being Element of X st (x \ y) \ z in I & z in I holds
x \ (y \ (y \ x)) in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & z in I implies x \ (y \ (y \ x)) in I )
assume ( (x \ y) \ z in I & z in I ) ; ::_thesis: x \ (y \ (y \ x)) in I
then x \ y in I by BCIALG_1:def_18;
hence x \ (y \ (y \ x)) in I by A3; ::_thesis: verum
end;
hence I is commutative Ideal of X by Def6; ::_thesis: verum
end;
theorem Th34: :: BCIIDEAL:34
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds
A is commutative Ideal of X
proof
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
proof
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)
proof
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;
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (x \ y) <= x by BCIALG_1:def_11;
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;
hence A is commutative Ideal of X by Th33; ::_thesis: verum
end;
theorem Th35: :: BCIIDEAL:35
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X ) by BCIALG_1:43; ::_thesis: ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X )
thus ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: verum
proof
assume A1: {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
let I be Ideal of X; ::_thesis: I is commutative Ideal of X
for I being Ideal of X holds {(0. X)} c= I
proof
let I be Ideal of X; ::_thesis: {(0. X)} c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in I )
assume x in {(0. X)} ; ::_thesis: x in I
then x = 0. X by TARSKI:def_1;
hence x in I by BCIALG_1:def_18; ::_thesis: verum
end;
hence I is commutative Ideal of X by A1, Th34; ::_thesis: verum
end;
end;
theorem Th36: :: BCIIDEAL:36
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
assume A2: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
let x, y be Element of X; ::_thesis: x \ y = x \ (y \ (y \ x))
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (y \ (y \ x)) by A2, BCIALG_3:def_1 ;
hence x \ y = x \ (y \ (y \ x)) ; ::_thesis: verum
end;
thus ( {(0. X)} is commutative Ideal of X implies X is commutative BCK-algebra ) ::_thesis: ( X is commutative BCK-algebra implies {(0. X)} is commutative Ideal of X )
proof
assume A3: {(0. X)} is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra
for x, y being Element of X st x <= y holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) )
assume x <= y ; ::_thesis: x = y \ (y \ x)
then x \ y = 0. X by BCIALG_1:def_11;
then x \ y in {(0. X)} by TARSKI:def_1;
then x \ (y \ (y \ x)) in {(0. X)} by A3, Th33;
then ( (y \ (y \ x)) \ x = 0. X & x \ (y \ (y \ x)) = 0. X ) by BCIALG_1:1, TARSKI:def_1;
hence x = y \ (y \ x) by BCIALG_1:def_7; ::_thesis: verum
end;
hence X is commutative BCK-algebra by BCIALG_3:5; ::_thesis: verum
end;
assume X is commutative BCK-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X
then for x, y being Element of X st x \ y in {(0. X)} holds
x \ (y \ (y \ x)) in {(0. X)} by A1;
hence {(0. X)} is commutative Ideal of X by Th33, BCIALG_1:43; ::_thesis: verum
end;
theorem Th37: :: BCIIDEAL:37
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
thus ( X is commutative BCK-algebra implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies X is commutative BCK-algebra )
proof
assume X is commutative BCK-algebra ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then {(0. X)} is commutative Ideal of X by Th36;
hence for I being Ideal of X holds I is commutative Ideal of X by Th35; ::_thesis: verum
end;
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra
then {(0. X)} is commutative Ideal of X by Th35;
hence X is commutative BCK-algebra by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:38
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X )
thus ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X )
proof
assume {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by Th36;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by Th37;
hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:39
for X being BCK-algebra
for I being Ideal of X
for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X
for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
let I be Ideal of X; ::_thesis: for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
let x, y be Element of X; ::_thesis: ( x \ (x \ y) in I implies ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) )
assume A1: x \ (x \ y) in I ; ::_thesis: ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
(x \ y) \ ((x \ y) \ x) = (x \ y) \ ((x \ x) \ y) by BCIALG_1:7
.= (x \ ((x \ x) \ y)) \ y by BCIALG_1:7
.= (x \ (y `)) \ y by BCIALG_1:def_5
.= (x \ (0. X)) \ y by BCIALG_1:def_8
.= x \ y by BCIALG_1:2 ;
hence x \ ((x \ y) \ ((x \ y) \ x)) in I by A1; ::_thesis: ( (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1;
then ((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:def_18;
then (y \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:2;
hence (y \ (y \ x)) \ x in I by BCIALG_1:2; ::_thesis: (y \ (y \ x)) \ (x \ y) in I
((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1;
then (y \ (0. X)) \ (y \ x) <= x \ (0. X) by BCIALG_1:def_11;
then ((y \ (0. X)) \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:5;
then (y \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:2;
then (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) by BCIALG_1:2;
then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = 0. X by BCIALG_1:def_11;
then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) in I by BCIALG_1:def_18;
hence (y \ (y \ x)) \ (x \ y) in I by A1, BCIALG_1:def_18; ::_thesis: verum
end;
theorem :: BCIIDEAL:40
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X )
proof
assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
then X is commutative BCK-algebra by Th36;
hence for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:1;
hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:41
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies {(0. X)} is commutative Ideal of X )
proof
assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
then X is commutative BCK-algebra by Th36;
hence for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:3;
hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:42
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies {(0. X)} is commutative Ideal of X )
proof
assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
then X is commutative BCK-algebra by Th36;
hence for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:4;
hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:43
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X )
proof
assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
then X is commutative BCK-algebra by Th36;
hence for x, y being Element of X st x <= y holds
x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum
end;
assume for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:5;
hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;
theorem :: BCIIDEAL:44
for X being BCK-algebra st {(0. X)} is commutative Ideal of X holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X implies ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) )
assume {(0. X)} is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
then A1: X is commutative BCK-algebra by Th36;
hence for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y being Element of X st x \ y = x holds
y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y)
thus for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum
end;
theorem :: BCIIDEAL:45
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
then X is commutative BCK-algebra by Th37;
hence for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:1;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
theorem :: BCIIDEAL:46
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
then X is commutative BCK-algebra by Th37;
hence for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:3;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
theorem :: BCIIDEAL:47
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
then X is commutative BCK-algebra by Th37;
hence for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum
end;
assume for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:4;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
theorem :: BCIIDEAL:48
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
then X is commutative BCK-algebra by Th37;
hence for x, y being Element of X st x <= y holds
x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum
end;
assume for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:5;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
theorem :: BCIIDEAL:49
for X being BCK-algebra st ( for I being Ideal of X holds I is commutative Ideal of X ) holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) )
assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
then A1: X is commutative BCK-algebra by Th37;
hence for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y being Element of X st x \ y = x holds
y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y)
thus for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum
end;
begin
definition
let X be BCK-algebra;
mode implicative-ideal of X -> non empty Subset of X means :Def7: :: BCIIDEAL:def 7
( 0. X in it & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in it & z in it holds
x in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b1 & z in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) )
X1 c= the carrier of X ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def_7_:_
for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b2 & z in b2 holds
x in b2 ) ) );
theorem Th50: :: BCIIDEAL:50
for X being BCK-algebra
for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
let I be Ideal of X; ::_thesis: ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
A1: ( ( for x, y being Element of X st x \ (y \ x) in I holds
x in I ) implies I is implicative-ideal of X )
proof
assume A2: for x, y being Element of X st x \ (y \ x) in I holds
x in I ; ::_thesis: I is implicative-ideal of X
A3: for x, y, z being Element of X st (x \ (y \ x)) \ z in I & z in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ (y \ x)) \ z in I & z in I implies x in I )
assume ( (x \ (y \ x)) \ z in I & z in I ) ; ::_thesis: x in I
then x \ (y \ x) in I by BCIALG_1:def_18;
hence x in I by A2; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is implicative-ideal of X by A3, Def7; ::_thesis: verum
end;
( I is implicative-ideal of X implies for x, y being Element of X st x \ (y \ x) in I holds
x in I )
proof
assume A4: I is implicative-ideal of X ; ::_thesis: for x, y being Element of X st x \ (y \ x) in I holds
x in I
let x, y be Element of X; ::_thesis: ( x \ (y \ x) in I implies x in I )
assume x \ (y \ x) in I ; ::_thesis: x in I
then A5: (x \ (y \ x)) \ (0. X) in I by BCIALG_1:2;
thus x in I by A4, A5, Def7; ::_thesis: verum
end;
hence ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I ) by A1; ::_thesis: verum
end;
definition
let X be BCK-algebra;
mode positive-implicative-ideal of X -> non empty Subset of X means :Def8: :: BCIIDEAL:def 8
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
x \ z in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds
x \ z in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x \ z in X1 ) )
X1 c= the carrier of X ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x \ z in X1 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def_8_:_
for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is positive-implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x \ z in b2 ) ) );
theorem Th51: :: BCIIDEAL:51
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
thus ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) ::_thesis: ( ( for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) implies I is positive-implicative-ideal of X )
proof
assume A1: I is positive-implicative-ideal of X ; ::_thesis: for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I
let x, y be Element of X; ::_thesis: ( (x \ y) \ y in I implies x \ y in I )
y \ y = 0. X by BCIALG_1:def_5;
then A2: y \ y in I by A1, Def8;
assume (x \ y) \ y in I ; ::_thesis: x \ y in I
hence x \ y in I by A1, A2, Def8; ::_thesis: verum
end;
thus ( ( for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) implies I is positive-implicative-ideal of X ) ::_thesis: verum
proof
assume A3: for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ; ::_thesis: I is positive-implicative-ideal of X
A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )
assume that
A5: (x \ y) \ z in I and
A6: y \ z in I ; ::_thesis: x \ z in I
(((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def_3;
then ((x \ z) \ z) \ ((x \ y) \ z) <= (x \ z) \ (x \ y) by BCIALG_1:def_11;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= 0. X by BCIALG_1:1;
then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by BCIALG_1:def_11;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2;
then ((x \ z) \ z) \ ((x \ y) \ z) <= y \ z by BCIALG_1:def_11;
then ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5;
then (x \ z) \ z in I by A5, BCIALG_1:def_18;
hence x \ z in I by A3; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is positive-implicative-ideal of X by A4, Def8; ::_thesis: verum
end;
end;
theorem Th52: :: BCIIDEAL:52
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) implies for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
assume A1: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies (x \ z) \ (y \ z) in I )
((x \ (y \ z)) \ (x \ y)) \ (y \ (y \ z)) = 0. X by BCIALG_1:1;
then (x \ (y \ z)) \ (x \ y) <= y \ (y \ z) by BCIALG_1:def_11;
then A2: ((x \ (y \ z)) \ (x \ y)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;
(y \ (y \ z)) \ z = (y \ z) \ (y \ z) by BCIALG_1:7;
then ((x \ (y \ z)) \ (x \ y)) \ z <= 0. X by A2, BCIALG_1:def_5;
then (((x \ (y \ z)) \ (x \ y)) \ z) \ (0. X) = 0. X by BCIALG_1:def_11;
then ((x \ (y \ z)) \ (x \ y)) \ z = 0. X by BCIALG_1:2;
then A3: ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:def_18;
assume (x \ y) \ z in I ; ::_thesis: (x \ z) \ (y \ z) in I
then (x \ (y \ z)) \ z in I by A1, A3;
hence (x \ z) \ (y \ z) in I by BCIALG_1:7; ::_thesis: verum
end;
theorem Th53: :: BCIIDEAL:53
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) holds
I is positive-implicative-ideal of X
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) holds
I is positive-implicative-ideal of X
let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) implies I is positive-implicative-ideal of X )
assume A1: for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ; ::_thesis: I is positive-implicative-ideal of X
A2: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )
assume that
A3: (x \ y) \ z in I and
A4: y \ z in I ; ::_thesis: x \ z in I
(x \ z) \ (y \ z) in I by A1, A3;
hence x \ z in I by A4, BCIALG_1:def_18; ::_thesis: verum
end;
0. X in I by BCIALG_1:def_18;
hence I is positive-implicative-ideal of X by A2, Def8; ::_thesis: verum
end;
theorem :: BCIIDEAL:54
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
A1: 0. X in I by BCIALG_1:def_18;
thus ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) by Def8; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) implies I is positive-implicative-ideal of X )
assume for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ; ::_thesis: I is positive-implicative-ideal of X
hence I is positive-implicative-ideal of X by A1, Def8; ::_thesis: verum
end;
theorem :: BCIIDEAL:55
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) by Def8;
hence ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) by Th52, Th53; ::_thesis: verum
end;
theorem :: BCIIDEAL:56
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X
proof
let X be BCK-algebra; ::_thesis: for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X
let I, A be Ideal of X; ::_thesis: ( I c= A & I is positive-implicative-ideal of X implies A is positive-implicative-ideal of X )
assume that
A1: I c= A and
A2: I is positive-implicative-ideal of X ; ::_thesis: A is positive-implicative-ideal of X
for x, y being Element of X st (x \ y) \ y in A holds
x \ y in A
proof
let x, y be Element of X; ::_thesis: ( (x \ y) \ y in A implies x \ y in A )
((x \ ((x \ y) \ y)) \ y) \ y = ((x \ y) \ ((x \ y) \ y)) \ y by BCIALG_1:7
.= ((x \ y) \ y) \ ((x \ y) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then ((x \ ((x \ y) \ y)) \ y) \ y in I by BCIALG_1:def_18;
then (x \ ((x \ y) \ y)) \ y in I by A2, Th51;
then A3: (x \ y) \ ((x \ y) \ y) in I by BCIALG_1:7;
assume (x \ y) \ y in A ; ::_thesis: x \ y in A
hence x \ y in A by A1, A3, BCIALG_1:def_18; ::_thesis: verum
end;
hence A is positive-implicative-ideal of X by Th51; ::_thesis: verum
end;
theorem :: BCIIDEAL:57
for X being BCK-algebra
for I being Ideal of X st I is implicative-ideal of X holds
( I is commutative Ideal of X & I is positive-implicative-ideal of X )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X st I is implicative-ideal of X holds
( I is commutative Ideal of X & I is positive-implicative-ideal of X )
let I be Ideal of X; ::_thesis: ( I is implicative-ideal of X implies ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) )
assume A1: I is implicative-ideal of X ; ::_thesis: ( I is commutative Ideal of X & I is positive-implicative-ideal of X )
A2: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I
proof
let x, y be Element of X; ::_thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )
(x \ (y \ (y \ x))) \ x = (x \ x) \ (y \ (y \ x)) by BCIALG_1:7
.= (y \ (y \ x)) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (y \ (y \ x)) <= x by BCIALG_1:def_11;
then y \ x <= y \ (x \ (y \ (y \ x))) by BCIALG_1:5;
then (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= (x \ (y \ (y \ x))) \ (y \ x) by BCIALG_1:5;
then A3: ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= ((x \ (y \ (y \ x))) \ (y \ x)) \ (x \ y) by BCIALG_1:5;
(x \ (y \ (y \ x))) \ (y \ x) = (x \ (y \ x)) \ (y \ (y \ x)) by BCIALG_1:7;
then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= 0. X by A3, BCIALG_1:def_3;
then (((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (0. X) = 0. X by BCIALG_1:def_11;
then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) = 0. X by BCIALG_1:2;
then A4: (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= x \ y by BCIALG_1:def_11;
assume x \ y in I ; ::_thesis: x \ (y \ (y \ x)) in I
hence x \ (y \ (y \ x)) in I by A1, A4, Th5, Th50; ::_thesis: verum
end;
for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I
proof
let x, y be Element of X; ::_thesis: ( (x \ y) \ y in I implies x \ y in I )
((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) = 0. X by BCIALG_1:1;
then A5: (x \ y) \ (x \ (x \ y)) <= (x \ y) \ y by BCIALG_1:def_11;
assume (x \ y) \ y in I ; ::_thesis: x \ y in I
hence x \ y in I by A1, A5, Th5, Th50; ::_thesis: verum
end;
hence ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) by A2, Th33, Th51; ::_thesis: verum
end;