:: Ideals of BCI-Algebras and Their Properties :: by Chenglong Wu and Yuzhong Ding :: :: Received March 3, 2008 :: Copyright (c) 2008-2021 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; 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 :: BCIIDEAL:1 for x,y,z,u being Element of X st x<=y holds u\(z\x)<=u\(z\y); theorem :: BCIIDEAL:2 for x,y,z,u being Element of X holds (x\(y\z))\(x\(y\u))<=z\u; theorem :: BCIIDEAL:3 for x,y,z,u,v being Element of X holds (x\(y\(z\u)))\(x\(y\(z\v)))<=v\ u; theorem :: BCIIDEAL:4 for x,y being Element of X holds (0.X\(x\y))\(y\x)=0.X; ::P26 definition let X; let a be Element of X; func initial_section(a) -> set equals :: BCIIDEAL:def 1 {x where x is Element of X:x<=a}; end; theorem :: BCIIDEAL:5 ::proposition 1.4.1 x<=a implies x in A; ::P37 theorem :: BCIIDEAL:6 for x,a,b being Element of AtomSet(X) holds x is Element of BranchV(b) implies a\x=a\b; theorem :: BCIIDEAL:7 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; theorem :: BCIIDEAL:8 initial_section(a) c= A; theorem :: BCIIDEAL:9 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; theorem :: BCIIDEAL:10 AtomSet(X) is Ideal of X implies AtomSet(X) is closed Ideal of X; ::p47 definition let X,I; attr I is positive means :: BCIIDEAL:def 2 for x being Element of I holds x is positive; end; ::P48 theorem :: BCIIDEAL:11 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 ); ::P50 theorem :: BCIIDEAL:12 for X being associative BCI-algebra,A being Ideal of X holds A is closed; theorem :: BCIIDEAL:13 for X being BCI-algebra,A being Ideal of X st X is quasi-associative holds A is closed; begin :: associative Ideal of X definition let X be BCI-algebra,IT be Ideal of X; attr IT is associative means :: 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; registration let X be BCI-algebra; cluster associative for Ideal of X; end; definition let X be BCI-algebra; mode associative-ideal of X -> non empty Subset of X means :: 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; end; theorem :: BCIIDEAL:14 X1 is associative-ideal of X implies X1 is Ideal of X; theorem :: BCIIDEAL:15 I is associative-ideal of X iff for x,y,z st (x\y)\z in I holds x\(y\z) in I; theorem :: BCIIDEAL:16 I is associative-ideal of X implies for x being Element of X holds x\( 0.X\x) in I; theorem :: BCIIDEAL:17 (for x being Element of X holds x\(0.X\x) in I) implies I is closed Ideal of X; definition let X be BCI-algebra; mode p-ideal of X -> non empty Subset of X means :: 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; end; theorem :: BCIIDEAL:18 X1 is p-ideal of X implies X1 is Ideal of X; theorem :: BCIIDEAL:19 for X,I st I is p-ideal of X holds BCK-part(X) c= I; theorem :: BCIIDEAL:20 BCK-part(X) is p-ideal of X; theorem :: BCIIDEAL:21 I is p-ideal of X iff for x,y st x in I & x<=y holds y in I; theorem :: BCIIDEAL:22 I is p-ideal of X iff for x,y,z st (x\z)\(y\z) in I holds x\y in I; begin :: P132: commutative Ideal of X definition let X be BCK-algebra, IT be Ideal of X; attr IT is commutative means :: 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; registration let X be BCK-algebra; cluster commutative for Ideal of X; end; theorem :: BCIIDEAL:23 for X being BCK-algebra holds BCK-part(X) is commutative Ideal of X; theorem :: BCIIDEAL:24 for X being BCK-algebra st X is p-Semisimple BCI-algebra holds {0.X} is commutative Ideal of X; reserve X for BCK-algebra; theorem :: BCIIDEAL:25 BCK-part(X) = the carrier of X; reserve X for BCI-algebra; theorem :: BCIIDEAL:26 (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); theorem :: BCIIDEAL:27 (for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x) implies the carrier of X = BCK-part(X); theorem :: BCIIDEAL:28 (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); theorem :: BCIIDEAL:29 (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); theorem :: BCIIDEAL:30 (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); theorem :: BCIIDEAL:31 (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); theorem :: BCIIDEAL:32 for X being BCK-algebra holds the carrier of X is commutative Ideal of X; reserve X for BCK-algebra; reserve I for Ideal of X; theorem :: BCIIDEAL:33 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; theorem :: BCIIDEAL:34 for I,A being Ideal of X st I c= A & I is commutative Ideal of X holds A is commutative Ideal of X; theorem :: BCIIDEAL:35 (for I being Ideal of X holds I is commutative Ideal of X) iff { 0.X} is commutative Ideal of X; theorem :: BCIIDEAL:36 {0.X} is commutative Ideal of X iff X is commutative BCK-algebra; theorem :: BCIIDEAL:37 X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X; theorem :: BCIIDEAL:38 {0.X} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X; reserve I for Ideal of X; theorem :: BCIIDEAL:39 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; theorem :: BCIIDEAL:40 {0.X} is commutative Ideal of X iff for x,y being Element of X holds x \(x\y) <= y\(y\x); theorem :: BCIIDEAL:41 {0.X} is commutative Ideal of X iff for x,y being Element of X holds x \y = x\(y\(y\x)); theorem :: BCIIDEAL:42 {0.X} is commutative Ideal of X iff for x,y being Element of X holds x \(x\y) = y\(y\(x\(x\y))); theorem :: BCIIDEAL:43 {0.X} is commutative Ideal of X iff for x,y being Element of X st x<= y holds x= y\(y\x); theorem :: BCIIDEAL:44 {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); theorem :: BCIIDEAL:45 (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); theorem :: BCIIDEAL:46 (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)); theorem :: BCIIDEAL:47 (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))); theorem :: BCIIDEAL:48 (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); theorem :: BCIIDEAL:49 (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); 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 :: 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; end; reserve X for BCK-algebra; reserve I for Ideal of X; theorem :: BCIIDEAL:50 I is implicative-ideal of X iff for x,y being Element of X st x\ (y\x) in I holds x in I; definition let X be BCK-algebra; mode positive-implicative-ideal of X -> non empty Subset of X means :: 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; end; theorem :: BCIIDEAL:51 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; theorem :: BCIIDEAL:52 (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; theorem :: BCIIDEAL:53 (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; theorem :: BCIIDEAL:54 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; theorem :: BCIIDEAL:55 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; theorem :: BCIIDEAL:56 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; theorem :: BCIIDEAL:57 I is implicative-ideal of X implies I is commutative Ideal of X & I is positive-implicative-ideal of X;