:: Ideals of BCI-Algebras and Their Properties :: by Chenglong Wu and Yuzhong Ding :: :: Received March 3, 2008 :: Copyright (c) 2008-2018 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;