:: Ideals of BCI-Algebras and Their Properties
:: by Chenglong Wu and Yuzhong Ding
::
:: Received March 3, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies BCIALG_1, XBOOLE_0, SUBSET_1, CARD_FIL, XXREAL_0, SUPINF_2,
CHORD, TARSKI, RCOMP_1, BINOP_1, STRUCT_0, WAYBEL15, BCIIDEAL;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
constructors BCIALG_2, BCIALG_3;
registrations STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities BCIALG_1;
expansions BCIALG_1, XBOOLE_0;
theorems BCIALG_1, TARSKI, XBOOLE_0, BCIALG_2, BCIALG_3;
begin :: Ideal of X
reserve X for BCI-algebra;
reserve X1 for non empty Subset of X;
reserve A,I for Ideal of X;
reserve x,y,z for Element of X;
reserve a for Element of A;
::P20
theorem
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;
assume x<=y;
then z\y<=z\x by BCIALG_1:5;
hence thesis by BCIALG_1:5;
end;
theorem
for x,y,z,u being Element of X holds (x\(y\z))\(x\(y\u))<=z\u
proof
let x,y,z,u be Element of X;
((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));
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;
then ((x\(y\z))\(x\(y\u)))\(z\u)=0.X by BCIALG_1:2;
hence thesis;
end;
theorem
for x,y,z,u,v being Element of X holds (x\(y\(z\u)))\(x\(y\(z\v)))<=v\ u
proof
let x,y,z,u,v be Element of X;
(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)));
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;
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);
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;
then (x\(y\(z\u)))\(x\(y\(z\v)))\(v\u)=0.X by BCIALG_1:2;
hence thesis;
end;
theorem
for x,y being Element of X holds (0.X\(x\y))\(y\x)=0.X
proof
let x,y be Element of 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 thesis by A1;
end;
::P26
definition
let X;
let a be Element of X;
func initial_section(a) -> set equals
{x where x is Element of X:x<=a};
coherence;
end;
theorem Th5: ::proposition 1.4.1
x<=a implies x in A
proof
assume x<=a;
then x\a = 0.X;
then x\a in A by BCIALG_1:def 18;
hence thesis by BCIALG_1:def 18;
end;
::P37
theorem
for x,a,b being Element of AtomSet(X) holds x is Element of BranchV(b)
implies a\x=a\b
proof
set P = AtomSet(X);
let x,a,b be Element of P;
set B = BranchV(b);
assume x is Element of B;
then x in B;
then ex x3 being Element of X st x=x3 & b<=x3;
then
A1: b\x=0.X;
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 thesis by A1;
end;
theorem
for a being Element of X,x,b being Element of AtomSet(X) holds x is
Element of BranchV(b) implies a\x=a\b
proof
set P = AtomSet(X);
let a be Element of X;
let x,b be Element of P;
set B = BranchV(b);
assume x is Element of B;
then x in B;
then ex x3 being Element of X st x=x3 & b<=x3;
then
A1: b\x=0.X;
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 thesis by A1;
end;
theorem
initial_section(a) c= A
proof
let b be object;
assume b in initial_section(a);
then ex x1 being Element of X st b=x1 & x1<=a;
hence thesis by Th5;
end;
theorem
AtomSet(X) is Ideal of X implies for x being Element of BCK-part(X),a
being Element of AtomSet(X) st x\a in AtomSet(X) holds x=0.X
proof
set B = BCK-part(X);
set P = AtomSet(X);
A1: x in {0.X} iff x in B/\P
proof
0.X in B & 0.X in P by BCIALG_1:19;
then 0.X in B/\P by XBOOLE_0:def 4;
hence x in {0.X} implies x in B/\P by TARSKI:def 1;
thus x in B/\P implies x in {0.X}
proof
assume
A2: x in B/\P;
then x in B 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;
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;
hence thesis by TARSKI:def 1;
end;
end;
assume
A4: P is Ideal of X;
for x being Element of B,a being Element of P st x\a in P holds x=0.X
proof
let x be Element of B;
let a be Element of P;
assume x\a in P;
then x in P by A4,BCIALG_1:def 18;
then x in B /\ P by XBOOLE_0:def 4;
then x in {0.X} by A1;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
theorem
AtomSet(X) is Ideal of X implies AtomSet(X) is closed Ideal of X
proof
set P = AtomSet(X);
A1: for x being Element of P holds x` in P
proof
let x be Element of P;
x` is minimal by BCIALG_2:30;
hence thesis;
end;
assume P is Ideal of X;
hence thesis by A1,BCIALG_1:def 19;
end;
::p47
definition
let X,I;
attr I is positive means
for x being Element of I holds x is positive;
end;
::P48
theorem
for X being BCK-algebra,A,I being Ideal of X holds (A/\I={0.X} iff for
x being Element of A,y being Element of I holds x\y =x )
proof
let X be BCK-algebra;
let A,I be Ideal of X;
thus A/\I={0.X} implies for x being Element of A,y being Element of I holds
x\y =x
proof
assume
A1: A/\I={0.X};
let x be Element of A;
let y be Element of I;
x\(x\y)\y=0.X by BCIALG_1:1;
then x\(x\y)<=y;
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;
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 thesis by A3,BCIALG_1:def 7;
end;
thus (for x being Element of A,y being Element of I holds x\y =x) implies A
/\I={0.X}
proof
assume
A4: for x being Element of A,y being Element of I holds x\y =x;
thus A/\I c= {0.X}
proof
let x be object;
assume
A5: x in A/\I;
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 thesis by TARSKI:def 1;
end;
let x be object;
assume x in {0.X};
then
A6: x =0.X by TARSKI:def 1;
0.X in A & 0.X in I by BCIALG_1:def 18;
hence thesis by A6,XBOOLE_0:def 4;
end;
end;
::P50
theorem
for X being associative BCI-algebra,A being Ideal of X holds A is closed
proof
let X be associative BCI-algebra;
let A be Ideal of X;
for x being Element of A holds x` in A
proof
let x be Element of A;
0.X\x=x\0.X by BCIALG_1:48
.=x by BCIALG_1:2;
hence thesis;
end;
hence thesis;
end;
theorem
for X being BCI-algebra,A being Ideal of X st X is quasi-associative
holds A is closed
by BCIALG_1:71,Th5;
begin :: associative Ideal of X
definition
let X be BCI-algebra,IT be Ideal of X;
attr IT is associative means
:Def3:
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;
registration
let X be BCI-algebra;
cluster associative for Ideal of X;
existence
proof
take Y={0.X};
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;
assume x\(y\z) in YY & y\z in YY;
then x\(y\z)=0.X & y\z=0.X by TARSKI:def 1;
hence thesis by BCIALG_1:2;
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 thesis by A1,Def3;
end;
end;
definition
let X be BCI-algebra;
mode associative-ideal of X -> non empty Subset of X means
:Def4:
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
proof
take X1=the carrier of X;
X1 c= the carrier of X;
hence thesis;
end;
end;
theorem
X1 is associative-ideal of X implies X1 is Ideal of X
proof
assume
A1: X1 is associative-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;
assume x\y in X1 & y in X1;
then (x\y)\0.X in X1 & y\0.X in X1 by BCIALG_1:2;
hence thesis by A1,Def4;
end;
0.X in X1 by A1,Def4;
hence thesis by A2,BCIALG_1:def 18;
end;
theorem Th15:
I is associative-ideal of X iff for x,y,z st (x\y)\z in I holds x\(y\z) in I
proof
thus I is associative-ideal of X implies for x,y,z st (x\y)\z in I holds x\(
y\z) in I
proof
assume
A1: I is associative-ideal of X;
let x,y,z such that
A2: (x\y)\z in I;
x\(x\y)\y =0.X by BCIALG_1:1;
then x\(x\y)<= y;
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;
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 thesis by A1,A2,Def4;
end;
assume
A4: for x,y,z st (x\y)\z in I holds x\(y\z) in I;
A5: for x,y,z st (x\y)\z in I & y\z in I holds x in I
proof
let x,y,z such that
A6: (x\y)\z in I and
A7: y\z in I;
x\(y\z) in I by A4,A6;
hence thesis by A7,BCIALG_1:def 18;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A5,Def4;
end;
theorem
I is associative-ideal of X implies for x being Element of X holds x\(
0.X\x) in I
proof
assume
A1: I is associative-ideal of X;
let x be Element of X;
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 thesis by A1,A2,Th15;
end;
theorem
(for x being Element of X holds x\(0.X\x) in I) implies I is closed
Ideal of X
proof
assume
A1: for x being Element of X holds x\(0.X\x) in I;
for x1 being Element of I holds x1` in I
proof
let x1 be Element of 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 thesis by BCIALG_1:def 18;
end;
hence thesis by BCIALG_1:def 19;
end;
definition
let X be BCI-algebra;
mode p-ideal of X -> non empty Subset of X means
:Def5:
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
proof
take X1=the carrier of X;
X1 c= X1;
hence thesis;
end;
end;
theorem
X1 is p-ideal of X implies X1 is Ideal of X
proof
assume
A1: X1 is p-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;
assume that
A3: x\y in X1 and
A4: y 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 thesis by A1,A4,Def5;
end;
0.X in X1 by A1,Def5;
hence thesis by A2,BCIALG_1:def 18;
end;
theorem Th19:
for X,I st I is p-ideal of X holds BCK-part(X) c= I
proof
let X,I;
assume
A1: I is p-ideal of X;
let x be object;
assume
A2: x in BCK-part(X);
then
A3: ex x1 being Element of X st x=x1 & 0.X<=x1;
reconsider x as Element of X by A2;
0.X\x = 0.X by A3;
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 thesis by A1,A4,Def5;
end;
theorem
BCK-part(X) is p-ideal of X
proof
set A = BCK-part(X);
A1: now
let x,y,z be Element of X;
assume that
A2: (x\z)\(y\z) in A and
A3: y in A;
ex c being Element of X st (x\z)\(y\z) = c & 0.X<=c by A2;
then ((x\z)\(y\z))`= 0.X;
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;
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;
hence x in A;
end;
0.X\0.X=0.X by BCIALG_1:def 5;
then 0.X <= 0.X;
then 0.X in A;
hence thesis by A1,Def5;
end;
theorem Th21:
I is p-ideal of X iff for x,y st x in I & x<=y holds y in I
proof
thus I is p-ideal of X implies for x,y st x in I & x<=y holds y in I
proof
assume I is p-ideal of X;
then
A1: BCK-part(X) c= I by Th19;
let x,y such that
A2: x in I and
A3: x <= y;
A4: x\y = 0.X by A3;
then (y\x)`=x\y by BCIALG_1:6;
then 0.X <= y\x by A4;
then y\x in BCK-part(X);
hence thesis by A2,A1,BCIALG_1:def 18;
end;
assume
A5: for x,y st x in I & x<=y holds y in I;
A6: for x,y,z st (x\z)\(y\z) in I & y in I holds x in I
proof
let x,y,z such that
A7: (x\z)\(y\z) in I and
A8: y in I;
((x\z)\(y\z))\(x\y)=0.X by BCIALG_1:def 3;
then ((x\z)\(y\z))<= x\y;
then x\y in I by A5,A7;
hence thesis by A8,BCIALG_1:def 18;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A6,Def5;
end;
theorem
I is p-ideal of X iff for x,y,z st (x\z)\(y\z) in I holds x\y in I
proof
thus I is p-ideal of X implies for x,y,z st (x\z)\(y\z) in I holds x\y in I
proof
assume
A1: I is p-ideal of X;
let x,y,z such that
A2: (x\z)\(y\z) in I;
(x\z)\(y\z)\(x\y) = 0.X by BCIALG_1:def 3;
then (x\z)\(y\z) <= (x\y);
hence thesis by A1,A2,Th21;
end;
assume
A3: for x,y,z st (x\z)\(y\z) in I holds x\y in I;
A4: for x,y,z st (x\z)\(y\z) in I & y in I holds x in I
proof
let x,y,z such that
A5: (x\z)\(y\z) in I and
A6: y in I;
x\y in I by A3,A5;
hence thesis by A6,BCIALG_1:def 18;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A4,Def5;
end;
begin :: P132: commutative Ideal of X
definition
let X be BCK-algebra, IT be Ideal of X;
attr IT is commutative means
:Def6:
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;
registration
let X be BCK-algebra;
cluster commutative for Ideal of X;
existence
proof
set X1 = BCK-part(X);
take X1;
A1: 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 such that
A2: x\y in X1 and
A3: y in X1;
ex x2 being Element of X st y=x2 & 0.X<=x2 by A3;
then
A4: y`=0.X;
ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
then (x\y)`=0.X;
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;
hence thesis;
end;
A5: 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;
assume that
(x\y)\z in X1 and
z in X1;
0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
then 0.X <= (x\(y\(y\x)));
hence thesis;
end;
0.X in BCK-part(X) by BCIALG_1:19;
then X1 is Ideal of X by A1,BCIALG_1:def 18;
hence thesis by A5,Def6;
end;
end;
theorem
for X being BCK-algebra holds BCK-part(X) is commutative Ideal of X
proof
let X be BCK-algebra;
set B = BCK-part(X);
A1: for x,y being Element of X st x\y in B & y in B holds x in B
proof
let x,y be Element of X such that
A2: x\y in B and
A3: y in B;
ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
then (x\y)`=0.X;
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;
then 0.X\x=0.X by BCIALG_1:2;
then 0.X<= x;
hence thesis;
end;
A5: for x,y,z being Element of X st (x\y)\z in B & z in B holds x\(y\(y\x))
in B
proof
let x,y,z be Element of X;
assume that
(x\y)\z in B and
z in B;
0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
then 0.X <= (x\(y\(y\x)));
hence thesis;
end;
0.X in BCK-part(X) by BCIALG_1:19;
hence thesis by A1,A5,Def6,BCIALG_1:def 18;
end;
theorem
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;
set X1={0.X};
A1: X1 c= the carrier of X
proof
let xx be object;
assume xx in X1;
then xx=0.X by TARSKI:def 1;
hence thesis;
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;
assume x\y in X1 & y in X1;
then x\y = 0.X & y = 0.X by TARSKI:def 1;
then x=0.X by BCIALG_1:2;
hence thesis by TARSKI:def 1;
end;
0.X in {0.X} by TARSKI:def 1;
then reconsider X1 as Ideal of X by A1,A2,BCIALG_1:def 18;
assume
A3: X is p-Semisimple BCI-algebra;
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;
assume (x\y)\z in X1 & z 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;
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 thesis by TARSKI:def 1;
end;
hence thesis by Def6;
end;
Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part(X)
proof
let X be BCK-algebra;
let x be object;
assume x in the carrier of 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;
hence thesis by A1;
end;
reserve X for BCK-algebra;
theorem Th25:
BCK-part(X) = the carrier of X
by Lm1;
reserve X for BCI-algebra;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y)
implies the carrier of X = BCK-part(X)
proof
assume for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y;
then X is BCK-algebra by BCIALG_1:13;
hence thesis by Th25;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x)
implies the carrier of X = BCK-part(X)
proof
assume for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x;
then X is BCK-algebra by BCIALG_1:14;
hence thesis by Th25;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x))
implies the carrier of X = BCK-part(X)
proof
assume for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x);
then X is BCK-algebra by BCIALG_1:12;
hence thesis by Th25;
end;
theorem
(for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\
(y\z)) implies the carrier of X = BCK-part(X)
proof
assume
for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z) \(y\z);
then X is BCK-algebra by BCIALG_1:15;
hence thesis by Th25;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y)
implies the carrier of X = BCK-part(X)
proof
assume for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y;
then X is BCK-algebra by BCIALG_1:16;
hence thesis by Th25;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y\
x))=0.X) implies the carrier of X = BCK-part(X)
proof
assume for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y
\x))=0.X;
then X is BCK-algebra by BCIALG_1:17;
hence thesis by Th25;
end;
theorem
for X being BCK-algebra holds the carrier of X is commutative Ideal of X
proof
let X be BCK-algebra;
set B = BCK-part(X);
A1: for x,y being Element of X st x\y in B & y in B holds x in B
proof
let x,y be Element of X such that
A2: x\y in B and
A3: y in B;
ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
then (x\y)`=0.X;
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;
then 0.X\x=0.X by BCIALG_1:2;
then 0.X<= x;
hence thesis;
end;
A5: for x,y,z being Element of X st (x\y)\z in B & z in B holds x\(y\(y\x))
in B
proof
let x,y,z be Element of X;
assume that
(x\y)\z in B and
z in B;
0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
then 0.X <= (x\(y\(y\x)));
hence thesis;
end;
the carrier of X=B by Th25;
hence thesis by A1,A5,Def6,BCIALG_1:def 18;
end;
reserve X for BCK-algebra;
reserve I for Ideal of X;
theorem Th33:
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
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
proof
A1: 0.X in I by BCIALG_1:def 18;
assume
A2: I is commutative Ideal of X;
let x,y be Element of X;
assume x\y in I;
then (x\y)\0.X in I by BCIALG_1:2;
hence thesis by A2,A1,Def6;
end;
assume
A3: for x,y being Element of X st x\y in I holds x\(y\(y\x)) in I;
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;
assume (x\y)\z in I & z in I;
then x\y in I by BCIALG_1:def 18;
hence thesis by A3;
end;
hence thesis by Def6;
end;
theorem Th34:
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 I,A be Ideal of X;
assume that
A1: I c= A and
A2: I 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;
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;
assume x<=y;
then z\y<=z\x by BCIALG_1:5;
hence thesis by BCIALG_1:5;
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;
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;
then (x\(y\(y\(x\(x\y))))) in A by A5,BCIALG_1:def 18;
hence thesis by A4,Th5;
end;
hence thesis by Th33;
end;
theorem Th35:
(for I being Ideal of X holds I is commutative Ideal of X) iff {
0.X} is commutative Ideal of X
proof
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;
thus {0.X} is commutative Ideal of X implies for I being Ideal of X holds I
is commutative Ideal of X
proof
assume
A1: {0.X} is commutative Ideal of X;
let I be Ideal of X;
for I being Ideal of X holds {0.X} c= I
proof
let I be Ideal of X;
let x be object;
assume x in {0.X};
then x=0.X by TARSKI:def 1;
hence thesis by BCIALG_1:def 18;
end;
hence thesis by A1,Th34;
end;
end;
theorem Th36:
{0.X} is commutative Ideal of X iff X is commutative BCK-algebra
proof
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;
let x,y be Element of X;
x\y = x\(x\(x\y)) by BCIALG_1:8
.= x\(y\(y\x)) by A2,BCIALG_3:def 1;
hence thesis;
end;
thus {0.X} is commutative Ideal of X implies X is commutative BCK-algebra
proof
assume
A3: {0.X} is commutative Ideal of X;
for x,y being Element of X st x<=y holds x=y\(y\x)
proof
let x,y be Element of X;
assume x<=y;
then x\y=0.X;
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 thesis by BCIALG_1:def 7;
end;
hence thesis by BCIALG_3:5;
end;
assume X is commutative BCK-algebra;
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 thesis by Th33,BCIALG_1:43;
end;
theorem Th37:
X is commutative BCK-algebra iff for I being Ideal of X holds I
is commutative Ideal of X
proof
thus X is commutative BCK-algebra implies for I being Ideal of X holds I is
commutative Ideal of X
proof
assume X is commutative BCK-algebra;
then {0.X} is commutative Ideal of X by Th36;
hence thesis by Th35;
end;
assume for I being Ideal of X holds I is commutative Ideal of X;
then {0.X} is commutative Ideal of X by Th35;
hence thesis by Th36;
end;
theorem
{0.X} is commutative Ideal of X iff for I being Ideal of X holds I is
commutative Ideal of X
by Th37,Th36;
reserve I for Ideal of X;
theorem
for x,y being Element of X holds 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
proof
let x,y be Element of X;
assume
A1: 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;
(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;
(y\0.X)\(y\x)\(x\0.X)=0.X by BCIALG_1:1;
then (y\0.X)\(y\x)<=(x\0.X);
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;
then y\(y\x)\(x\y)\(x\(x\y)) in I by BCIALG_1:def 18;
hence thesis by A1,BCIALG_1:def 18;
end;
theorem
{0.X} is commutative Ideal of X iff for x,y being Element of X holds x
\(x\y) <= y\(y\x)
by BCIALG_3:1,Th36;
theorem
{0.X} is commutative Ideal of X iff for x,y being Element of X holds x
\y = x\(y\(y\x))
by BCIALG_3:3,Th36;
theorem
{0.X} is commutative Ideal of X iff for x,y being Element of X holds x
\(x\y) = y\(y\(x\(x\y)))
by BCIALG_3:4,Th36;
theorem
{0.X} is commutative Ideal of X iff for x,y being Element of X st x<=
y holds x= y\(y\x)
by BCIALG_3:5,Th36;
theorem
{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)
proof
assume {0.X} is commutative Ideal of X;
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;
thus for x,y being Element of X st x\y=x holds y\x=y by A1,BCIALG_3:7;
thus for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x by A1,
BCIALG_3:8;
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;
thus thesis by A1,BCIALG_3:11;
end;
theorem
(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)
by BCIALG_3:1,Th37;
theorem
(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))
by BCIALG_3:3,Th37;
theorem
(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)))
by BCIALG_3:4,Th37;
theorem
(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)
by BCIALG_3:5,Th37;
theorem
(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)
proof
assume for I being Ideal of X holds I is commutative Ideal of X;
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;
thus for x,y being Element of X st x\y=x holds y\x=y by A1,BCIALG_3:7;
thus for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x by A1,
BCIALG_3:8;
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;
thus thesis by A1,BCIALG_3:11;
end;
begin :: implicative Ideal of X & positive-implicative-ideal
definition
let X be BCK-algebra;
mode implicative-ideal of X -> non empty Subset of X means
:Def7:
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
proof
take X1=the carrier of X;
X1 c= the carrier of X;
hence thesis;
end;
end;
reserve X for BCK-algebra;
reserve I for Ideal of X;
theorem Th50:
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
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;
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;
assume (x\(y\x))\z in I & z in I;
then x\(y\x) in I by BCIALG_1:def 18;
hence thesis by A2;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A3,Def7;
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;
let x,y be Element of X;
assume x\(y\x) in I;
then
A5: x\(y\x)\0.X in I by BCIALG_1:2;
thus thesis by A4,A5,Def7;
end;
hence thesis by A1;
end;
definition
let X be BCK-algebra;
mode positive-implicative-ideal of X -> non empty Subset of X means
:Def8:
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
proof
take X1=the carrier of X;
X1 c= the carrier of X;
hence thesis;
end;
end;
theorem Th51:
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
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
proof
assume
A1: I is positive-implicative-ideal of X;
let x,y be Element of X;
y\y =0.X by BCIALG_1:def 5;
then
A2: y\y in I by A1,Def8;
assume (x\y)\y in I;
hence thesis by A1,A2,Def8;
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
proof
assume
A3: for x,y being Element of X st (x\y)\y in I holds x\y in I;
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;
assume that
A5: (x\y)\z in I and
A6: y\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);
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;
then ((x\z)\z)\((x\y)\z)\(y\z)=0.X by BCIALG_1:2;
then ((x\z)\z)\((x\y)\z)<=y\z;
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 thesis by A3;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A4,Def8;
end;
end;
theorem Th52:
(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
proof
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;
let x,y,z be Element of X;
x\(y\z) \ (x\y) \ (y\(y\z)) =0.X by BCIALG_1:1;
then x\(y\z) \ (x\y)<=y\(y\z);
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;
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;
then x\(y\z)\z in I by A1,A3;
hence thesis by BCIALG_1:7;
end;
theorem Th53:
(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
proof
assume
A1: for x,y,z being Element of X st (x\y)\z in I holds (x\z)\(y\z) in I;
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;
assume that
A3: (x\y)\z in I and
A4: y\z in I;
(x\z)\(y\z) in I by A1,A3;
hence thesis by A4,BCIALG_1:def 18;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by A2,Def8;
end;
theorem
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
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;
assume
for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x\z in I;
hence thesis by A1,Def8;
end;
theorem
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
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 thesis by Th52,Th53;
end;
theorem
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 I,A be Ideal of X;
assume that
A1: I c= A and
A2: I 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;
(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;
hence thesis by A1,A3,BCIALG_1:def 18;
end;
hence thesis by Th51;
end;
theorem
I is implicative-ideal of X implies I is commutative Ideal of X & I is
positive-implicative-ideal of X
proof
assume
A1: I is 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;
(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;
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;
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;
assume x\y in I;
hence thesis by A1,A4,Th5,Th50;
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;
(x\y)\(x\(x\y))\((x\y)\y)=0.X by BCIALG_1:1;
then
A5: (x\y)\(x\(x\y))<=((x\y)\y);
assume (x\y)\y in I;
hence thesis by A1,A5,Th5,Th50;
end;
hence thesis by A2,Th33,Th51;
end;