:: 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;
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;