:: Several Classes of {BCI}-algebras and Their Properties
:: by Yuzhong Ding
::
:: Received February 23, 2007
:: Copyright (c) 2007-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 STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, FUNCT_1, SUPINF_2,
FUNCT_5, ZFMISC_1, UNIALG_2, TARSKI, REALSET1, RELAT_1, XXREAL_0,
WAYBEL15, CARD_FIL, RCOMP_1, FILTER_0, BCIALG_1, CARD_1;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, ORDINAL1, BINOP_1, FUNCT_5,
REALSET1, STRUCT_0, RELAT_1;
constructors BINOP_1, REALSET1, MIDSP_1, FUNCT_5, RELSET_1, NUMBERS;
registrations RELAT_1, STRUCT_0, CARD_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, STRUCT_0;
equalities REALSET1, XBOOLE_0;
expansions STRUCT_0;
theorems TARSKI, ZFMISC_1, XBOOLE_0, STRUCT_0, FUNCT_2;
begin :: The Basics of General Theory of BCI-algebra
definition
struct (1-sorted) BCIStr (# carrier -> set, InternalDiff -> BinOp of the
carrier #);
end;
registration
cluster non empty strict for BCIStr;
existence
proof
set A = the non empty set,m = the BinOp of A;
take BCIStr(#A,m#);
thus the carrier of BCIStr(#A,m#) is non empty;
thus thesis;
end;
end;
definition
let A be BCIStr;
let x,y be Element of A;
func x \ y -> Element of A equals
(the InternalDiff of A).(x,y);
coherence;
end;
definition
struct (BCIStr,ZeroStr) BCIStr_0 (# carrier -> set, InternalDiff -> BinOp of
the carrier, ZeroF -> Element of the carrier #);
end;
registration
cluster non empty strict for BCIStr_0;
existence
proof
set A = the non empty set,m = the BinOp of A,u = the Element of A;
take BCIStr_0(#A,m,u#);
thus the carrier of BCIStr_0(#A,m,u#) is non empty;
thus thesis;
end;
end;
definition
let IT be non empty BCIStr_0, x be Element of IT;
func x` -> Element of IT equals
0.IT\x;
coherence;
end;
definition
let IT be non empty BCIStr_0;
attr IT is being_B means
:Def3:
for x,y,z being Element of IT holds ((x\y)\( z\y))\(x\z)=0.IT;
attr IT is being_C means
:Def4:
for x,y,z being Element of IT holds ((x\y)\z )\((x\z)\y)=0.IT;
attr IT is being_I means
:Def5:
for x being Element of IT holds x\x=0.IT;
attr IT is being_K means
for x,y being Element of IT holds (x\y)\x=0. IT;
attr IT is being_BCI-4 means
:Def7:
for x,y being Element of IT holds (x\y= 0.IT&y\x=0.IT implies x = y);
attr IT is being_BCK-5 means
:Def8:
for x being Element of IT holds x`=0.IT;
end;
definition
func BCI-EXAMPLE -> BCIStr_0 equals
BCIStr_0 (# {0}, op2, op0 #);
coherence;
end;
registration
cluster BCI-EXAMPLE -> strict 1-element;
coherence;
end;
registration
cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5;
coherence
by STRUCT_0:def 10;
end;
registration
cluster strict being_B being_C being_I being_BCI-4 being_BCK-5 for non empty
BCIStr_0;
existence
proof
take BCI-EXAMPLE;
thus thesis;
end;
end;
definition
mode BCI-algebra is being_B being_C being_I being_BCI-4 non empty BCIStr_0;
end;
definition
mode BCK-algebra is being_BCK-5 BCI-algebra;
end;
definition
let X be BCI-algebra;
mode SubAlgebra of X -> BCI-algebra means
:Def10:
0.it = 0.X & the carrier
of it c= the carrier of X & the InternalDiff of it = (the InternalDiff of X)||
the carrier of it;
existence
proof
take X;
dom(the InternalDiff of X) = [:the carrier of X,the carrier of X:] by
FUNCT_2:def 1;
hence thesis;
end;
end;
::T1.1.11
theorem Th1:
for X being non empty BCIStr_0 holds (X is BCI-algebra iff (X is
being_I & X is being_BCI-4 &for x,y,z being Element of X holds ((x\y)\(x\z))\(z
\y)=0.X & (x\(x\y))\y = 0.X ))
proof
let X be non empty BCIStr_0;
thus X is BCI-algebra implies (X is being_I & X is being_BCI-4 &for x,y,z
being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X )
proof
assume
A1: X is BCI-algebra;
now
let x,y,z be Element of X;
A2: ((x\y)\(z\y))\(x\z)=0.X by A1,Def3;
A3: for x,y,z being Element of X holds (x\y)\z = (x\z)\y
proof
let x,y,z be Element of X;
((x\y)\z)\((x\z)\y)=0.X & ((x\z)\y)\((x\y)\z)=0.X by A1,Def4;
hence thesis by A1,Def7;
end;
then (x\(x\y))\y=(x\y)\(x\y);
hence
((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X & x\x = 0.X & (x\y = 0.
X & y\x = 0.X implies x = y) by A1,A2,A3,Def5,Def7;
end;
hence thesis;
end;
assume that
A4: X is being_I and
A5: X is being_BCI-4 and
A6: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y
))\y = 0.X;
A7: for x being Element of X st x\0.X=0.X holds x=0.X
proof
let x be Element of X;
assume
A8: x\0.X =0.X;
then x` = (x \ (x\x)) \ x by A4
.= 0.X by A6;
hence thesis by A5,A8;
end;
A9: for x being Element of X holds x \ 0.X = x
proof
let x be Element of X;
(x\(x\0.X))\0.X = 0.X by A6;
then
A10: x\(x\0.X) = 0.X by A7;
0.X = (x\(x\x))\x by A6
.= (x\0.X)\x by A4;
hence thesis by A5,A10;
end;
A11: for x,y,z being Element of X st x\y=0.X & y\z=0.X holds x\z=0.X
proof
let x,y,z be Element of X;
assume that
A12: x\y=0.X and
A13: y\z=0.X;
((x\z)\(x\y))\(y\z)=0.X by A6;
then (x\z)\(x\y)=0.X by A9,A13;
hence thesis by A9,A12;
end;
A14: for x,y,z being Element of X holds ((x\y)\z)\((x\z)\y) = 0.X
proof
let x,y,z be Element of X;
(((x\y)\z)\((x\y)\(x\(x\z))))\((x\(x\z))\z)=0.X by A6;
then (((x\y)\z)\((x\y)\(x\(x\z))))\0.X=0.X by A6;
then
A15: ((x\y)\z)\((x\y)\(x\(x\z)))=0.X by A7;
((x\y)\(x\(x\z)))\((x\z)\y) = 0.X by A6;
hence thesis by A11,A15;
end;
A16: for x,y,z being Element of X st x\y=0.X holds (x\z)\(y\z)=0.X&(z\y)\(z\
x)=0.X
proof
let x,y,z be Element of X;
assume
A17: x\y=0.X;
((z\y)\(z\x))\(x\y)=0.X & ((x\z)\(x\y))\(y\z)=0.X by A6;
hence thesis by A9,A17;
end;
for x,y,z being Element of X holds ((x\y)\(z\y))\(x\z) = 0.X
proof
let x,y,z be Element of X;
((x\y)\(x\z))\(z\y) = 0.X by A6;
then ((x\y)\(z\y))\((x\y)\((x\y)\(x\z))) = 0.X by A16;
then (((x\y)\(z\y))\(x\z))\(((x\y)\((x\y)\(x\z)))\(x\z)) = 0.X by A16;
then (((x\y)\(z\y))\(x\z))\ 0.X = 0.X by A6;
hence thesis by A7;
end;
hence thesis by A4,A5,A14,Def3,Def4;
end;
definition
let IT be non empty BCIStr_0;
let x,y be Element of IT;
pred x <= y means
x \ y = 0.IT;
end;
reserve X for BCI-algebra;
reserve x,y,z,u,a,b for Element of X;
reserve IT for non empty Subset of X;
Lm1: x\0.X = 0.X implies x = 0.X
proof
assume
A1: x\0.X =0.X;
then x` = (x \ (x\x)) \ x by Def5
.= 0.X by Th1;
hence thesis by A1,Def7;
end;
theorem Th2:
x \ 0.X = x
proof
(x\(x\0.X))\0.X = 0.X by Th1;
then
A1: x\(x\0.X) = 0.X by Lm1;
0.X = (x\(x\x))\x by Th1
.= (x\0.X)\x by Def5;
hence thesis by A1,Def7;
end;
theorem Th3:
x\y=0.X & y\z=0.X implies x\z=0.X
proof
assume that
A1: x\y=0.X and
A2: y\z=0.X;
((x\z)\(x\y))\(y\z)=0.X by Th1;
then (x\z)\(x\y)=0.X by A2,Th2;
hence thesis by A1,Th2;
end;
theorem Th4:
x\y=0.X implies (x\z)\(y\z)=0.X & (z\y)\(z\x)=0.X
proof
assume
A1: x\y=0.X;
((z\y)\(z\x))\(x\y)=0.X & ((x\z)\(x\y))\(y\z)=0.X by Th1;
hence thesis by A1,Th2;
end;
theorem
x <= y implies x\z <= y\z & z\y <= z\x
by Th4;
theorem
x\y=0.X implies (y\x)` = 0.X
proof
assume x\y = 0.X;
then (x\x)\(y\x) = 0.X by Th4;
hence thesis by Def5;
end;
theorem Th7:
(x\y)\z = (x\z)\y
proof
(x\(x\z))\z = 0.X by Th1;
then
A1: ((x\y)\z)\((x\y)\(x\(x\z)))=0.X by Th4;
(x\(x\y))\y = 0.X by Th1;
then
A2: ((x\z)\y)\((x\z)\(x\(x\y)))=0.X by Th4;
((x\z)\(x\(x\y)))\((x\y)\z) = 0.X by Th1;
then
A3: ((x\z)\y)\((x\y)\z) = 0.X by A2,Th3;
((x\y)\(x\(x\z)))\((x\z)\y) = 0.X by Th1;
then ((x\y)\z)\((x\z)\y) = 0.X by A1,Th3;
hence thesis by A3,Def7;
end;
theorem Th8:
x\(x\(x\y)) = x\y
proof
(x\y)\(x\(x\(x\y)))\((x\(x\y))\y) = 0.X by Th1;
then (x\y)\(x\(x\(x\y)))\0.X = 0.X by Th1;
then
A1: (x\y)\(x\(x\(x\y))) = 0.X by Th2;
(x\(x\(x\y)))\(x\y) = 0.X by Th1;
hence thesis by A1,Def7;
end;
theorem Th9:
(x\y)` = x`\y`
proof
x`\y`= ((((x\y)\(x\y))\x)\y`) by Def5
.= ((((x\y)\x)\(x\y))\y`) by Th7
.= ((((x\x)\y)\(x\y))\y`) by Th7
.= ((y`\(x\y))\y`) by Def5
.= (y`\y`)\(x\y) by Th7;
hence thesis by Def5;
end;
theorem Th10:
((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X
proof
((x\(x\y))\(y\x))\(x\(x\(y\(y\x)))) =((x\(x\y))\(x\(x\(y\(y\x)))))\(y\x)
by Th7
.=((x\(x\(x\(y\(y\x)))))\(x\y))\(y\x) by Th7
.=((x\(y\(y\x)))\(x\y))\(y\x) by Th8
.=((x\(y\(y\x)))\(x\y))\(y\(y\(y\x))) by Th8;
hence thesis by Th1;
end;
theorem ::T1.1.6
for X being non empty BCIStr_0 holds (X is BCI-algebra iff (X is
being_BCI-4 & for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.
X = x ))
proof
let X be non empty BCIStr_0;
thus X is BCI-algebra implies (X is being_BCI-4 & for x,y,z being Element of
X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X = x ) by Th1,Th2;
thus (X is being_BCI-4 & for x,y,z being Element of X holds ((x\y)\(x\z))\(z
\y)=0.X & x\0.X = x )implies X is BCI-algebra
proof
assume that
A1: X is being_BCI-4 and
A2: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X = x;
A3: X is being_I
proof
let x be Element of X;
x\x=(x\x)\0.X by A2;
then x\x=((x\0.X)\x)\0.X by A2;
then x\x=((x\0.X)\(x\0.X))\0.X by A2;
then x\x=((x\0.X)\(x\0.X))\(0.X)` by A2;
hence thesis by A2;
end;
now
let x,y,z be Element of X;
((x\0.X)\(x\y))\(y\0.X)=0.X by A2;
then (x\(x\y))\(y\0.X)=0.X by A2;
hence ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X by A2;
end;
hence thesis by A1,A3,Th1;
end;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x))
implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x);
for z being Element of X holds z` = 0.X
proof
let z be Element of X;
z`` = z \ (z \ 0.X) by A1;
then z`` = z \ z by Th2;
then z`` \ z = z` by Def5;
hence thesis by Th1;
end;
hence thesis by Def8;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y)
implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y;
for z being Element of X holds z` = 0.X
proof
let z be Element of X;
z`\(z` \ z) =z`\z` by A1;
then z`\(z` \ z) =0.X by Def5;
hence thesis by Th1;
end;
hence thesis by Def8;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x)
implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x;
for z being Element of X holds z` = 0.X
proof
let z be Element of X;
(z \ 0.X )` = 0.X by A1;
hence thesis by Th2;
end;
hence thesis by Def8;
end;
theorem
(for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\
(y\z) ) implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)
\(y\z);
for s being Element of X holds s` = 0.X
proof
let s be Element of X;
s` \ s=s` \ (s \ s) by A1;
then s` \ s=s` \ 0.X by Def5;
then s`\(s` \ s) =s`\s` by Th2;
then s`\(s` \ s) =0.X by Def5;
hence thesis by Th1;
end;
hence thesis by Def8;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y)
implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y;
for s being Element of X holds s` = 0.X
proof
let s be Element of X;
s` \ (s \ 0.X ) = s` by A1;
then s`\(s` \ s) =s`\s` by Th2;
then s`\(s` \ s) =0.X by Def5;
hence thesis by Th1;
end;
hence thesis by Def8;
end;
theorem
(for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y\
x))=0.X) implies X is BCK-algebra
proof
assume
A1: for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y
\x))=0.X;
for s being Element of X holds s` = 0.X
proof
let s be Element of X;
s`\(s`\(s\0.X))=0.X by A1;
then (s`\(s`\s))\s=s` by Th2;
hence thesis by Th1;
end;
hence thesis by Def8;
end;
theorem
for X being BCI-algebra holds X is being_K iff X is BCK-algebra
proof
let X be BCI-algebra;
thus X is being_K implies X is BCK-algebra
proof
assume
A1: X is being_K;
now
let s be Element of X;
s`\0.X = 0.X by A1;
hence s` = 0.X by Th2;
end;
hence thesis by Def8;
end;
assume
A2: X is BCK-algebra;
let x,y be Element of X;
y` = 0.X by A2,Def8;
then (x\y)\(x\0.X) = 0.X by Th4;
hence thesis by Th2;
end;
definition
let X be BCI-algebra; ::P4 1.3 atom BranchV
func BCK-part(X) -> non empty Subset of X equals
{x where x is Element of X:
0.X<=x};
coherence
proof
set Y={x where x is Element of X:0.X<=x};
A1: now
let y be object;
assume y in Y;
then ex x being Element of X st y=x & 0.X<=x;
hence y in the carrier of X;
end;
(0.X)`=0.X by Def5;
then 0.X <= 0.X;
then 0.X in Y;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th19:
0.X in BCK-part(X)
proof
(0.X)`=0.X by Def5;
then 0.X <= 0.X;
hence thesis;
end;
theorem
for x,y being Element of BCK-part(X) holds x\y in BCK-part(X)
proof
let x,y be Element of BCK-part(X);
x in {x1 where x1 is Element of X:0.X<=x1};
then
A1: ex x1 being Element of X st x=x1 & 0.X<= x1;
y in {y1 where y1 is Element of X:0.X<=y1};
then
A2: ex y1 being Element of X st y=y1 & 0.X<=y1;
(x\y)`=x`\y` by Th9;
then (x\y)`=(y`)` by A1;
then (x\y)`=(0.X)` by A2;
then (x\y)`=0.X by Def5;
then 0.X <= x\y;
hence thesis;
end;
theorem
for x being Element of X,y being Element of BCK-part(X) holds x\y <= x
proof
let x be Element of X,y be Element of BCK-part(X);
y in {y1 where y1 is Element of X:0.X<=y1};
then ex y1 being Element of X st y=y1 & 0.X<=y1;
then y`=0.X;
then (x\x)\y=0.X by Def5;
then (x\y)\x=0.X by Th7;
hence thesis;
end;
theorem Th22:
X is SubAlgebra of X
proof
dom(the InternalDiff of X) = [:the carrier of X,the carrier of X:] by
FUNCT_2:def 1;
then
0.X = 0.X & the InternalDiff of X =(the InternalDiff of X)||the carrier
of X;
hence thesis by Def10;
end;
definition
let X be BCI-algebra,IT be SubAlgebra of X;
attr IT is proper means
:Def13:
IT <> X;
end;
registration
let X;
cluster non proper for SubAlgebra of X;
existence
proof
take X;
X is SubAlgebra of X by Th22;
hence thesis by Def13;
end;
end;
definition
let X be BCI-algebra,IT be Element of X;
attr IT is atom means
for z being Element of X holds z\IT=0.X implies z=IT;
end;
definition
let X be BCI-algebra;
func AtomSet(X) -> non empty Subset of X equals
{x where x is Element of X:x
is atom};
coherence
proof
set Y={x where x is Element of X:x is atom};
A1: now
let y be object;
assume y in Y;
then ex x being Element of X st y=x & x is atom;
hence y in the carrier of X;
end;
for z being Element of X st z\0.X=0.X holds z=0.X by Th2;
then 0.X is atom;
then 0.X in Y;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th23:
0.X in AtomSet(X)
proof
for z being Element of X st z\0.X=0.X holds z=0.X by Th2;
then 0.X is atom;
hence thesis;
end;
theorem Th24:
for x being Element of X holds x in AtomSet(X) iff for z being
Element of X holds z\(z\x)=x
proof
let x be Element of X;
thus x in AtomSet(X) implies for z being Element of X holds z\(z\x)=x
proof
assume x in AtomSet(X);
then
A1: ex x1 being Element of X st x=x1 & x1 is atom;
let z be Element of X;
(z\(z\x))\x=0.X by Th1;
hence thesis by A1;
end;
assume
A2: for z being Element of X holds z\(z\x)=x;
now
let z be Element of X;
assume z\x=0.X;
then z\0.X=x by A2;
hence z=x by Th2;
end;
then x is atom;
hence thesis;
end;
theorem
for x being Element of X holds x in AtomSet(X) iff for u,z being
Element of X holds (z\u)\(z\x)=x\u
proof
let x be Element of X;
thus x in AtomSet(X) implies for u,z being Element of X holds (z\u)\(z\x)=x\
u
proof
assume x in AtomSet(X);
then
A1: ex x1 being Element of X st x=x1 & x1 is atom;
let u,z be Element of X;
(z\(z\x))\x=0.X by Th1;
then (z\(z\x))=x by A1;
hence thesis by Th7;
end;
assume
A2: for u,z being Element of X holds (z\u)\(z\x)=x\u;
now
let z be Element of X;
assume z\x=0.X;
then (z\0.X)\0.X=x\0.X by A2;
then (z\0.X)\0.X=x by Th2;
then z\0.X=x by Th2;
hence z=x by Th2;
end;
then x is atom;
hence thesis;
end;
theorem
for x being Element of X holds x in AtomSet(X) iff for y,z being
Element of X holds x\(z\y)<=y\(z\x)
proof
let x be Element of X;
thus x in AtomSet(X) implies for y,z being Element of X holds x\(z\y)<=y\(z\
x)
proof
assume x in AtomSet(X);
then
A1: ex x1 being Element of X st x=x1 & x1 is atom;
let y,z be Element of X;
(z\(z\x))\x=0.X by Th1;
then (x\(z\y))\(y\(z\x))= ((z\(z\x))\(z\y))\(y\(z\x)) by A1;
then (x\(z\y))\(y\(z\x))= ((z\(z\y))\(z\x))\(y\(z\x))by Th7;
then (x\(z\y))\(y\(z\x))= ((z\(z\y))\(z\x))\(y\(z\x))\0.X by Th2;
then (x\(z\y))\(y\(z\x))=((z\(z\y))\(z\x))\(y\(z\x))\((z\(z\y))\y) by Th1;
then (x\(z\y))\(y\(z\x))=0.X by Def3;
hence thesis;
end;
assume
A2: for y,z being Element of X holds x\(z\y)<=y\(z\x);
now
let z be Element of X;
assume
A3: z\x=0.X;
(x\(z\0.X)) <= (z\x)` by A2;
then (x\(z\0.X))\(0.X)`=0.X by A3;
then (x\(z\0.X))\0.X = 0.X by Th2;
then x\(z\0.X) = 0.X by Th2;
then x\z = 0.X by Th2;
hence z=x by A3,Def7;
end;
then x is atom;
hence thesis;
end;
theorem
for x being Element of X holds x in AtomSet(X) iff for y,z,u being
Element of X holds (x\u)\(z\y)<=(y\u)\(z\x)
proof
let x be Element of X;
thus x in AtomSet(X) implies for y,z,u being Element of X holds (x\u)\(z\y)
<=(y\u)\(z\x)
proof
assume x in AtomSet(X);
then
A1: ex x1 being Element of X st x=x1 & x1 is atom;
let y,z,u be Element of X;
(z\(z\x))\x=0.X by Th1;
then
((x\u)\(z\y))\((y\u)\(z\x))=(((z\(z\x))\u)\(z\y))\((y\u)\(z\x)) by A1;
then ((x\u)\(z\y))\((y\u)\(z\x))=(((z\u)\(z\x))\(z\y))\((y\u)\(z\x))by Th7;
then ((x\u)\(z\y))\((y\u)\(z\x))=(((z\u)\(z\y))\(z\x))\((y\u)\(z\x))by Th7
.=((((z\u)\(z\y))\(z\x))\((y\u)\(z\x)))\0.X by Th2;
then
((x\u)\(z\y))\((y\u)\(z\x)) =((((z\u)\(z\y))\(z\x))\((y\u)\(z\x)))\(((
z\u)\(z\y))\(y\u)) by Th1;
then ((x\u)\(z\y))\((y\u)\(z\x))=0.X by Def3;
hence thesis;
end;
assume
A2: for y,z,u being Element of X holds (x\u)\(z\y)<=(y\u)\(z\x);
now
let z be Element of X;
assume
A3: z\x=0.X;
((x\0.X)\(z\0.X)) <= ((0.X)`\(z\x)) by A2;
then ((x\0.X)\(z\0.X)) \(((0.X)`\0.X))=0.X by A3;
then ((x\0.X)\(z\0.X)) \(0.X)`=0.X by Th2;
then ((x\0.X)\(z\0.X)) \0.X=0.X by Th2;
then (x\0.X)\(z\0.X)=0.X by Th2;
then (x\0.X)\z=0.X by Th2;
then x\z = 0.X by Th2;
hence z=x by A3,Def7;
end;
then x is atom;
hence thesis;
end;
theorem Th28:
for x being Element of X holds x in AtomSet(X) iff for z being
Element of X holds z`\x`=x\z
proof
let x be Element of X;
thus x in AtomSet(X) implies for z being Element of X holds z`\x`=x\z
proof
assume x in AtomSet(X);
then
A1: ex x1 being Element of X st x=x1 & x1 is atom;
let z be Element of X;
(z\(z\x))\x=0.X by Th1;
then (z\(z\x))=x by A1;
then x\z=(z\z)\(z\x) by Th7;
then x\z=(z\x)` by Def5;
hence thesis by Th9;
end;
assume
A2: for z being Element of X holds z`\x`=x\z;
now
let z be Element of X;
assume
A3: z\x=0.X;
then (z\x)`=0.X by Def5;
then z`\x`=0.X by Th9;
then x\z = 0.X by A2;
hence z=x by A3,Def7;
end;
then x is atom;
hence thesis;
end;
theorem Th29:
for x being Element of X holds x in AtomSet(X) iff x``=x
proof
let x be Element of X;
thus x in AtomSet(X) implies (x`)`=x
proof
assume x in AtomSet(X);
then (0.X)`\x`= x \ 0.X by Th28;
then (0.X)`\(x`)=x by Th2;
hence thesis by Def5;
end;
assume
A1: x``=x;
now
let z be Element of X;
assume
A2: z\x=0.X;
then ((z\x)\(x`))\(z\0.X)=x\z by A1,Th2;
then 0.X=x\z by Def3;
hence z=x by A2,Def7;
end;
then x is atom;
hence thesis;
end;
theorem Th30:
for x being Element of X holds x in AtomSet(X) iff for z being
Element of X holds (z\x)`=x\z
proof
let x be Element of X;
A1: (for z being Element of X holds z`\x`=x\z) implies for z being Element
of X holds (z\x)`=x\z
proof
assume
A2: for z being Element of X holds z`\x`=x\z;
let z be Element of X;
z`\x`=x\z by A2;
hence thesis by Th9;
end;
(for z being Element of X holds (z\x)`=x\z) implies for z being Element
of X holds z`\x`=x\z
proof
assume
A3: for z being Element of X holds (z\x)`=x\z;
let z be Element of X;
(z\x)`=x\z by A3;
hence thesis by Th9;
end;
hence thesis by A1,Th28;
end;
theorem Th31:
for x being Element of X holds x in AtomSet(X) iff for z being
Element of X holds ((x\z)`)`=x\z
proof
let x be Element of X;
thus x in AtomSet(X) implies for z being Element of X holds ((x\z)`)`=x\z
proof
assume
A1: x in AtomSet(X);
let z be Element of X;
A2: (z\(z\x))\x=0.X by Th1;
ex x1 being Element of X st x=x1 & x1 is atom by A1;
then (z\(z\x))=x by A2;
then ((x\z)`)`=(((z\z)\(z\x))`)` by Th7;
then ((x\z)`)`=(((z\x)`)`)` by Def5;
then ((x\z)`)`=(z\x)` by Th8;
hence thesis by A1,Th30;
end;
assume for z being Element of X holds (x\z)``=x\z;
then ((x\0.X)`)`=x\0.X;
then (x`)`=x\0.X by Th2;
then (x`)`=x by Th2;
hence thesis by Th29;
end;
theorem
for x being Element of X holds x in AtomSet(X) iff for z,u being
Element of X holds z\(z\(x\u))=x\u
proof
let x be Element of X;
thus x in AtomSet(X) implies for z,u being Element of X holds z\(z\(x\u))=x\
u
proof
assume
A1: x in AtomSet(X);
let z,u be Element of X;
x\u =((x\u)`)` by A1,Th31
.= ((z\z)\(x\u))` by Def5
.= ((z\(x\u))\z)` by Th7
.= (z\(x\u))`\z` by Th9;
then
A2: (x\u)\( z\(z\(x\u)))=0.X by Th1;
( z\(z\(x\u)))\(x\u)=0.X by Th1;
hence thesis by A2,Def7;
end;
assume for z,u being Element of X holds z\(z\(x\u))=x\u;
then (x\u)``=x\u;
hence thesis by Th31;
end;
theorem Th33: ::tuilun1.3.3
for a being Element of AtomSet(X),x being Element of X holds a\x
in AtomSet(X)
proof
let a be Element of AtomSet(X),x be Element of X;
((a\x)`)`=a\x by Th31;
hence thesis by Th29;
end;
definition
let X be BCI-algebra,a,b be Element of AtomSet(X);
redefine func a\b -> Element of AtomSet(X); :: redefines \ (BCIALG_1, definition)
coherence by Th33;
end;
theorem Th34:
for x being Element of X holds x` in AtomSet(X)
proof
let x be Element of X;
0.X in AtomSet(X) by Th23;
hence thesis by Th33;
end;
theorem Th35:
for x being Element of X holds ex a being Element of AtomSet(X) st a<=x
proof
let x be Element of X;
take a=x``;
a\x=0.X by Th1;
hence thesis by Th34;
end;
definition
let X be BCI-algebra;
attr X is generated_by_atom means
for x being Element of X holds ex a being Element of AtomSet(X) st a<=x;
end;
definition
let X be BCI-algebra,a be Element of AtomSet(X);
func BranchV(a) -> non empty Subset of X equals
{x where x is Element of X:a
<=x};
coherence
proof
set Y={x where x is Element of X:a<=x};
A1: now
let y be object;
assume y in Y;
then ex x being Element of X st y=x & a<=x;
hence y in the carrier of X;
end;
a\a=0.X by Def5;
then a <= a;
then a in Y;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem
for X being BCI-algebra holds X is generated_by_atom
by Th35;
theorem
for a,b being Element of AtomSet(X),x being Element of BranchV(b)
holds a\x =a\b
proof
let a,b be Element of AtomSet(X),x be Element of BranchV(b);
a\b in {x1 where x1 is Element of X:x1 is atom};
then
A1: ex x1 being Element of X st a\b=x1 & x1 is atom;
x in {yy where yy is Element of X:b<=yy};
then
A2: ex yy being Element of X st x=yy & b<= yy;
(a\x)\(a\b)=(a\(a\b))\x by Th7;
then (a\x)\(a\b)=b\x by Th24;
then (a\x)\(a\b)=0.X by A2;
hence thesis by A1;
end;
theorem Th38:
for a being Element of AtomSet(X),x being Element of BCK-part(X) holds a\x =a
proof
let a be Element of AtomSet(X),x be Element of BCK-part(X);
a\0.X in {x1 where x1 is Element of X:x1 is atom} by Th33;
then
A1: ex x1 being Element of X st a\0.X=x1 & x1 is atom;
(a\x)\(a\0.X)=(a\(a\0.X))\x by Th7;
then (a\x)\(a\0.X)=(a\a)\x by Th2;
then
A2: (a\x)\(a\0.X)=x` by Def5;
x in {x2 where x2 is Element of X:0.X<=x2};
then ex x2 being Element of X st x=x2 & 0.X<=x2;
then (a\x)\(a\0.X)=0.X by A2;
then a\x=a\0.X by A1;
hence thesis by Th2;
end;
Lm2: for a being Element of AtomSet(X),x being Element of BranchV(a) holds a\x
=0.X
proof
let a be Element of AtomSet(X),x be Element of BranchV(a);
x in {x1 where x1 is Element of X:a<=x1};
then ex x1 being Element of X st x=x1 & a<=x1;
hence thesis;
end;
theorem Th39:
for a,b being Element of AtomSet(X),x being Element of BranchV(a
), y being Element of BranchV(b) holds x\y in BranchV(a\b)
proof
let a,b be Element of AtomSet(X),x be Element of BranchV(a), y be Element of
BranchV(b);
(a\b)\(x\y)=(((a\b)`)`)\(x\y) by Th29;
then (a\b)\(x\y)=(x\y)`\(a\b)` by Th7;
then (a\b)\(x\y)=x`\y`\(a\b)` by Th9;
then (a\b)\(x\y)=((x`)\((a\b)`))\y` by Th7;
then (a\b)\(x\y)=((((a\b)`)`)\x)\(y`) by Th7;
then (a\b)\(x\y)=((a\b)\x)\(y`) by Th29;
then (a\b)\(x\y)=((a\x)\b)\(y`) by Th7;
then (a\b)\(x\y)=b`\y` by Lm2;
then (a\b)\(x\y)=(b\y)` by Th9;
then (a\b)\(x\y)=(0.X)` by Lm2;
then (a\b)\(x\y)=0.X by Def5;
then a\b <= x\y;
hence thesis;
end;
theorem
for a being Element of AtomSet(X),x,y being Element of BranchV(a)
holds x\y in BCK-part(X)
proof
let a be Element of AtomSet(X),x,y be Element of BranchV(a);
set b=a\a;
b=0.X & x\y in BranchV(b) by Def5,Th39;
hence thesis;
end;
theorem
for a,b being Element of AtomSet(X),x being Element of BranchV(a), y
being Element of BranchV(b) st a<>b holds not x\y in BCK-part(X)
proof
let a,b be Element of AtomSet(X),x be Element of BranchV(a), y be Element of
BranchV(b);
assume
A1: a<>b;
x\y in BranchV(a\b) by Th39;
then ex xy being Element of X st x\y=xy & a\b <= xy;
then (a\b)\(x\y) =0.X;
then (a\(x\y))\b =0.X by Th7;
then (a\(x\y))\((a\(x\y))\b) =a\(x\y) by Th2;
then
A2: b = a\(x\y) by Th24;
assume x\y in BCK-part(X);
hence contradiction by A1,A2,Th38;
end;
theorem
for a,b being Element of AtomSet(X) st a<>b holds BranchV(a) /\
BranchV(b) = {}
proof
let a,b be Element of AtomSet(X);
assume
A1: a<>b;
assume BranchV(a) /\ BranchV(b) <> {};
then consider c being object such that
A2: c in BranchV(a) /\ BranchV(b) by XBOOLE_0:def 1;
reconsider z2 = c as Element of BranchV(b) by A2,XBOOLE_0:def 4;
reconsider z1 = c as Element of BranchV(a) by A2,XBOOLE_0:def 4;
z1 \ z2 in BranchV(a\b) by Th39;
then 0.X in {x3 where x3 is Element of X:a\b<=x3}by Def5;
then ex x3 being Element of X st 0.X = x3 & a\b <= x3;
then (a\b)\0.X = 0.X;
then
A3: a\b = 0.X by Th2;
b in {xx where xx is Element of X:xx is atom};
then ex xx being Element of X st b=xx & xx is atom;
hence contradiction by A1,A3;
end;
::Ideal
definition
let X be BCI-algebra;
mode Ideal of X -> non empty Subset of X means
:Def18:
0.X in it & for x,y
being Element of X st x\y in it & y in it holds x in it;
existence
proof
take X1={0.X};
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;
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 Th2;
hence thesis by TARSKI:def 1;
end;
now
let xx be object;
assume xx in X1;
then xx=0.X by TARSKI:def 1;
hence xx in the carrier of X;
end;
hence thesis by A1,TARSKI:def 1,def 3;
end;
end;
definition
let X be BCI-algebra, IT be Ideal of X;
attr IT is closed means
:Def19:
for x being Element of IT holds x` in IT;
end;
Lm3: {0.X} is Ideal of X
proof
set X1={0.X};
now
let xx be object;
assume xx in X1;
then xx=0.X by TARSKI:def 1;
hence xx in the carrier of X;
end;
then
A1: X1 is Subset of X by TARSKI:def 3;
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 Th2;
hence thesis by TARSKI:def 1;
end;
0.X in {0.X} by TARSKI:def 1;
hence thesis by A1,A2,Def18;
end;
Lm4: for X1 being Ideal of X st X1={0.X} holds for x being Element of X1 holds
x` in { 0.X }
proof
let X1 be Ideal of X;
assume
A1: X1={0.X};
let x be Element of X1;
x=0.X by A1,TARSKI:def 1;
then x`=0.X by Def5;
hence thesis by TARSKI:def 1;
end;
registration
let X;
cluster closed for Ideal of X;
existence
proof
set X1={0.X};
reconsider X1 as Ideal of X by Lm3;
take X1;
for x being Element of X1 holds x` in X1 by Lm4;
hence thesis;
end;
end;
theorem
{0.X} is closed Ideal of X
proof
set X1={0.X};
reconsider X1 as Ideal of X by Lm3;
for x being Element of X1 holds x` in X1 by Lm4;
hence thesis by Def19;
end;
theorem
the carrier of X is closed Ideal of X
proof
A1: ( for x being Element of X holds x` in the carrier of X)& for x,y being
Element of X st x\y in the carrier of X & y in the carrier of X
holds x in the carrier of X;
the carrier of X is non empty Subset of X & 0.X in the carrier of X by
ZFMISC_1:def 1;
hence thesis by A1,Def18,Def19;
end;
theorem
BCK-part(X) is closed Ideal of X
proof
set X1=BCK-part(X);
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 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 Th9;
ex x2 being Element of X st y=x2 & 0.X<= x2 by A3;
then x`\0.X = 0.X by A4;
then x`=0.X by Th2;
then 0.X<= x;
hence thesis;
end;
0.X in BCK-part(X) by Th19;
then reconsider X1 as Ideal of X by A1,Def18;
now
let x be Element of X1;
x in X1;
then ex x1 being Element of X st x=x1 & 0.X<= x1;
then (x`)=0.X;
then (x`)`=0.X by Def5;
then 0.X <=x`;
hence x` in X1;
end;
hence thesis by Def19;
end;
Lm5: IT is Ideal of X implies for x,y being Element of IT holds {z where z is
Element of X : z\x<=y} c= IT
proof
assume
A1: IT is Ideal of X;
let x,y be Element of IT;
A2: 0.X in IT by A1,Def18;
let ss be object;
assume ss in {z where z is Element of X : z\x<=y};
then
A3: ex z being Element of X st ss=z & z\x <= y;
then reconsider ss as Element of X;
(ss\x)\y in IT by A2,A3;
then ss\x in IT by A1,Def18;
hence thesis by A1,Def18;
end;
theorem
IT is Ideal of X implies for x,y being Element of X st x in IT & y<=x
holds y in IT
proof
assume
A1: IT is Ideal of X;
let x,y be Element of X;
assume that
A2: x in IT and
A3: y<=x;
y\0.X <= x by A3,Th2;
then
A4: y in {z where z is Element of X : z\0.X<=x};
0.X is Element of IT by A1,Def18;
then {z where z is Element of X : z\0.X<=x} c= IT by A1,A2,Lm5;
hence thesis by A4;
end;
begin :: Several Classes of BCI-algebra---associative BCI-algebra
definition
let IT be BCI-algebra;
attr IT is associative means
:Def20:
for x,y,z being Element of IT holds x\y \z = x\(y\z);
attr IT is quasi-associative means
for x being Element of IT holds x ``=x`;
attr IT is positive-implicative means
for x,y being Element of IT holds (x\(x\y))\(y\x)=x\(x\(y\(y\x)));
attr IT is weakly-positive-implicative means
:Def23:
for x,y,z being Element of IT holds (x\y)\z=((x\z)\z)\(y\z);
attr IT is implicative means
:Def24:
for x,y being Element of IT holds (x\(x \y))\(y\x)=y\(y\x);
attr IT is weakly-implicative means
for x,y being Element of IT holds (x\(y\ x))\(y\x)`=x;
attr IT is p-Semisimple means
:Def26:
for x,y being Element of IT holds x\(x \y) = y;
attr IT is alternative means
for x,y being Element of IT holds x\(x\ y) = (x\x)\y & (x\y)\y=x\(y\y);
end;
registration
cluster BCI-EXAMPLE -> implicative positive-implicative p-Semisimple
associative weakly-implicative weakly-positive-implicative;
coherence
by STRUCT_0:def 10;
end;
registration
cluster implicative positive-implicative p-Semisimple associative
weakly-implicative weakly-positive-implicative for BCI-algebra;
existence
proof
take BCI-EXAMPLE;
thus thesis;
end;
end;
Lm6: (for x,y being Element of X holds y\x=x\y) implies X is associative
proof
assume
A1: for x,y being Element of X holds y\x=x\y;
let x,y,z be Element of X;
x\(y\z) = (y\z)\x by A1
.=(y\x)\z by Th7;
hence thesis by A1;
end;
Lm7: (for x holds x`=x) implies for x,y holds x\y=y\x
proof
assume
A1: for x holds x`=x;
let x,y;
A2: (y\x)\(x\y)=(y`\x)\(x\y) by A1
.=(y`\x`)\(x\y) by A1
.=0.X by Th1;
(x\y)\(y\x)=(x`\y)\(y\x) by A1
.=(x`\y`)\(y\x) by A1
.=0.X by Th1;
hence thesis by A2,Def7;
end;
theorem Th47:
X is associative iff for x being Element of X holds x`=x
proof
thus X is associative implies for x being Element of X holds x`=x
proof
assume
A1: X is associative;
let x be Element of X;
A2: x\x`=(x\0.X)\x by A1
.=x\x by Th2
.=0.X by Def5;
x`\x=(x\x)` by A1
.=(0.X)` by Def5
.=0.X by Def5;
hence thesis by A2,Def7;
end;
assume for x being Element of X holds x`=x;
then for x,y holds x\y=y\x by Lm7;
hence thesis by Lm6;
end;
theorem Th48:
(for x,y being Element of X holds y\x=x\y) iff X is associative
proof
thus (for x,y being Element of X holds y\x=x\y) implies X is associative by
Lm6;
assume X is associative;
then for x being Element of X holds x`=x by Th47;
hence thesis by Lm7;
end;
theorem Th49:
for X being non empty BCIStr_0 holds (X is associative
BCI-algebra iff for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x )
proof
let X be non empty BCIStr_0;
thus X is associative BCI-algebra implies for x,y,z being Element of X holds
(y\x)\(z\x)=z\y & x\0.X=x
proof
assume
A1: X is associative BCI-algebra;
let x,y,z be Element of X;
(z\y)\((y\x)\(z\x))=((z\y)\(y\x))\(z\x) by A1,Def20;
then (z\y)\((y\x)\(z\x)) = ((z\y)\(z\x))\(y\x) by A1,Th7;
then (z\y)\((y\x)\(z\x)) = ((z\y)\(z\x))\(x\y) by A1,Th48;
then
A2: (z\y)\((y\x)\(z\x)) = 0.X by A1,Th1;
((y\x)\(z\x))\(z\y)=((y\x)\(z\x))\(y\z) by A1,Th48;
then ((y\x)\(z\x))\(z\y)=0.X by A1,Def3;
hence thesis by A1,A2,Def7,Th2;
end;
thus (for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x) implies
X is associative BCI-algebra
proof
assume
A3: for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x;
A4: for x,y being Element of X holds y\x=x\y
proof
let x,y be Element of X;
(y\0.X)\(x\0.X)=x\y by A3;
then y\(x\0.X)=x\y by A3;
hence thesis by A3;
end;
A5: for a being Element of X holds a\a=0.X
proof
let a be Element of X;
a`\a`=(0.X)` by A3;
then (a\0.X)\a`=(0.X)` by A4;
then (a\0.X)\(a\0.X)=(0.X)` by A4;
then a\a=(0.X)` by A3;
hence thesis by A3;
end;
A6: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y)
)\y = 0.X
proof
let x,y,z be Element of X;
((x\y)\(x\z))\(z\y)=((y\x)\(x\z))\(z\y) by A4
.=((y\x)\(z\x))\(z\y) by A4
.=(z\y)\(z\y) by A3;
hence ((x\y)\(x\z))\(z\y)=0.X by A5;
x`\(y\x)=y\0.X by A3;
then (x\0.X)\(y\x)=y\0.X by A4;
then (x\0.X)\(x\y)=y\0.X by A4;
then x\(x\y)=y\0.X by A3;
then (x\(x\y))\y=y\y by A3;
hence (x\(x\y))\y = 0.X by A5;
end;
for x,y being Element of X holds (x\y=0.X&y\x=0.X implies x = y)
proof
let x,y be Element of X;
assume that
A7: x\y = 0.X and
y\x = 0.X;
x`\(y\x)=y\0.X by A3;
then (x\0.X)\(y\x)=y\0.X by A4;
then (x\0.X)\(x\y)=y\0.X by A4;
then x\(x\y)=y\0.X by A3;
then y=x\(x\y) by A3
.=x by A3,A7;
hence thesis;
end;
then
A8: X is being_BCI-4;
X is being_I by A5;
then reconsider Y=X as BCI-algebra by A6,A8,Th1;
Y is associative by A4,Th48;
hence thesis;
end;
end;
theorem Th50:
for X being non empty BCIStr_0 holds (X is associative
BCI-algebra iff for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x )
proof
let X be non empty BCIStr_0;
thus X is associative BCI-algebra implies for x,y,z being Element of X holds
(x\y)\(x\z)=z\y & x`=x
proof
assume
A1: X is associative BCI-algebra;
let x,y,z be Element of X;
(y\x)\(z\x)=z\y by A1,Th49;
then
A2: (x\y)\(z\x)=z\y by A1,Th48;
x\0.X=x by A1,Th49;
hence thesis by A1,A2,Th48;
end;
assume
A3: for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x;
for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x
proof
A4: for x,y being Element of X holds y\x=x\y
proof
let x,y be Element of X;
y`\x`=x\y by A3;
then y\x`=x\y by A3;
hence thesis by A3;
end;
let x,y,z be Element of X;
A5: x`=x by A3;
(x\y)\(x\z)=z\y by A3;
then (y\x)\(x\z)=z\y by A4;
hence thesis by A4,A5;
end;
hence thesis by Th49;
end;
theorem
for X being non empty BCIStr_0 holds (X is associative BCI-algebra iff
for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x )
proof
let X be non empty BCIStr_0;
thus X is associative BCI-algebra implies for x,y,z being Element of X holds
(x\y)\(x\z)=y\z & x\0.X=x
proof
assume
A1: X is associative BCI-algebra;
let x,y,z be Element of X;
(y\x)\(z\x)=z\y by A1,Th49;
then (x\y)\(z\x)=z\y by A1,Th48;
then (x\y)\(x\z)=z\y by A1,Th48;
hence thesis by A1,Th48,Th49;
end;
assume
A2: for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x;
for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x
proof
let x,y,z be Element of X;
A3: for x,y being Element of X holds y\x=x\y
proof
let x,y be Element of X;
(x\0.X)\(x\0.X)=(0.X)` by A2;
then x\(x\0.X)=(0.X)` by A2;
then x\x=(0.X)` by A2;
then
A4: x\x=0.X by A2;
(x\y)\(x\x)=y\x by A2;
hence thesis by A2,A4;
end;
(x\y)\(x\z)=y\z & x\0.X=x by A2;
hence thesis by A3;
end;
hence thesis by Th50;
end;
begin :: Several Classes of BCI-algebra----p-Semisimple BCI-algebra
theorem
X is p-Semisimple iff for x being Element of X holds x is atom
proof
thus X is p-Semisimple implies for x being Element of X holds x is atom
proof
assume
A1: X is p-Semisimple;
let x be Element of X;
now
let z be Element of X;
assume z\x=0.X;
then z\0.X = x by A1;
hence z=x by Th2;
end;
hence thesis;
end;
assume
A2: for x being Element of X holds x is atom;
for x,y being Element of X holds x\(x\y) = y
proof
let x,y be Element of X;
y is atom & (x\(x\y))\y=0.X by A2,Th1;
hence thesis;
end;
hence thesis;
end;
theorem
X is p-Semisimple implies BCK-part(X)={0.X}
proof
assume
A1: X is p-Semisimple;
thus BCK-part(X) c= {0.X}
proof
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;
(x`)`=x by A1;
then (0.X)`=x by A3;
then x=0.X by Def5;
hence thesis by TARSKI:def 1;
end;
thus {0.X} c= BCK-part(X)
proof
let x be object;
assume
A4: x in {0.X};
then reconsider x as Element of X by TARSKI:def 1;
x=0.X by A4,TARSKI:def 1;
then x`=0.X by Def5;
then 0.X <= x;
hence thesis;
end;
end;
Lm8: (for x,y holds y\(y\x) = x) iff for x,y,z holds (z\y)\(z\x) = x\y
proof
thus (for x,y holds y\(y\x) = x) implies for x,y,z holds (z\y)\(z\x) = x\y
proof
assume
A1: for x,y holds y\(y\x) = x;
let x,y,z;
(z\y)\(z\x)= (z\(z\x))\y by Th7;
hence thesis by A1;
end;
assume
A2: for x,y,z holds (z\y)\(z\x) = x\y;
let x,y;
(y\0.X)\(y\x) = x\0.X by A2;
then y\(y\x) = x\0.X by Th2;
hence thesis by Th2;
end;
theorem Th54:
X is p-Semisimple iff for x being Element of X holds x`` = x
proof
(for x being Element of X holds x`` = x) implies X is p-Semisimple
proof
assume
A1: for x being Element of X holds x`` = x;
now
let x,y be Element of X;
A2: (x\(x\y))\y=0.X by Th1;
y\(x\(x\y))=(y\(x\(x\y)))`` by A1
.=(y`\(x\(x\y))`)` by Th9
.=0.X \(((0.X \y)\((x\(x\y))`))\0.X) by Th2
.=0.X \(((0.X \y)\((x\(x\y))`))\((x\(x\y))\y)) by Th1
.=0.X \0.X by Th1
.=0.X by Def5;
hence x\(x\y) = y by A2,Def7;
end;
hence thesis;
end;
hence thesis;
end;
theorem
X is p-Semisimple iff for x,y holds y\(y\x) = x;
theorem Th56:
X is p-Semisimple iff for x,y,z holds (z\y)\(z\x) = x\y
proof
X is p-Semisimple iff for x,y holds y\(y\x) = x;
hence thesis by Lm8;
end;
theorem Th57:
X is p-Semisimple iff for x,y,z holds x\(z\y) = y\(z\x)
proof
thus X is p-Semisimple implies for x,y,z holds x\(z\y) = y\(z\x)
proof
assume
A1: X is p-Semisimple;
let x,y,z;
y\(z\x) =(z\(z\y))\(z\x) by A1;
then
A2: (y\(z\x))\(x\(z\y))=0.X by Th1;
x\(z\y) =(z\(z\x))\(z\y)by A1;
then (x\(z\y))\(y\(z\x))=0.X by Th1;
hence thesis by A2,Def7;
end;
assume
A3: for x,y,z holds x\(z\y) = y\(z\x);
for x holds x`` = x
proof
let x;
x`` = x\(0.X)` by A3
.=x\0.X by Def5;
hence thesis by Th2;
end;
hence thesis by Th54;
end;
Lm9: X is p-Semisimple implies for x,y,z,u holds (x\u)\(z\y)=(y\u)\(z\x)&(x\u
)\(z\y)=(x\z)\(u\y)
proof
assume
A1: X is p-Semisimple;
let x,y,z,u;
A2: (x\u)\(z\y)=(x\(z\y))\u by Th7
.=(y\(z\x))\u by A1,Th57;
(x\u)\(z\y)=y\(z\(x\u)) by A1,Th57
.=y\(u\(x\z)) by A1,Th57
.=(x\z)\(u\y) by A1,Th57;
hence thesis by A2,Th7;
end;
Lm10: X is p-Semisimple implies for x,y holds y`\(0.X \x)=x\y
proof
assume
A1: X is p-Semisimple;
let x,y;
y`\(0.X \x)=(x\y)\(0.X \0.X) by A1,Lm9
.=(x\y)\0.X by Def5;
hence thesis by Th2;
end;
Lm11: X is p-Semisimple implies for x,y,z holds (x\y)\(z\y)=x\z
proof
assume
A1: X is p-Semisimple;
let x,y,z;
(x\y)\(z\y)=(x\z)\(y\y) by A1,Lm9
.=(x\z)\0.X by Def5;
hence thesis by Th2;
end;
Lm12: X is p-Semisimple implies for x,y,z st x\y=x\z holds y=z
proof
assume
A1: X is p-Semisimple;
let x,y,z;
assume
A2: x\y=x\z;
(x\z)\(x\y)=(y\z)\(x\x) by A1,Lm9;
then (x\z)\(x\y)=(y\z)\0.X by Def5;
then (x\z)\(x\y)=y\z by Th2;
then
A3: 0.X=y\z by A2,Def5;
(x\y)\(x\z)=(z\y)\(x\x) by A1,Lm9;
then (x\y)\(x\z)=(z\y)\0.X by Def5;
then (x\y)\(x\z)=z\y by Th2;
then 0.X=z\y by A2,Def5;
hence thesis by A3,Def7;
end;
Lm13: X is p-Semisimple implies for x,y,z holds x\(y\z)=(z\y)\x`
proof
assume
A1: X is p-Semisimple;
let x,y,z;
x\(y\z)=z\(y\x) by A1,Th57
.=(z\0.X)\(y\x) by Th2;
hence thesis by A1,Lm9;
end;
Lm14: X is p-Semisimple implies for x,y,z st y\x=z\x holds y=z
proof
assume
A1: X is p-Semisimple;
let x,y,z;
assume
A2: y\x=z\x;
A3: z\y=(z\x)\(y\x) by A1,Lm11
.=0.X by A2,Def5;
y\z=(y\x)\(z\x) by A1,Lm11
.=0.X by A2,Def5;
hence thesis by A3,Def7;
end;
theorem
X is p-Semisimple iff for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x)
proof
thus X is p-Semisimple implies for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x)
by Lm9;
thus (for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x)) implies X is p-Semisimple
proof
assume
A1: for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x);
for x,y,z holds x\(z\y) = y\(z\x)
proof
let x,y,z;
(x\0.X)\(z\y) = (y\0.X)\(z\x) by A1;
then x\(z\y)= (y\0.X)\(z\x) by Th2;
hence thesis by Th2;
end;
hence thesis by Th57;
end;
end;
theorem Th59:
X is p-Semisimple iff for x,z holds z`\x` = x\z
proof
thus X is p-Semisimple implies for x,z holds z`\x` = x\z by Lm10;
assume
A1: for x,z holds z`\x` = x\z;
for x holds x`` = x
proof
let x;
(0.X)`\x` = x\0.X by A1;
then (x`)` = x\0.X by Th2;
hence thesis by Th2;
end;
hence thesis by Th54;
end;
theorem
X is p-Semisimple iff for x,z holds (x\z)`` = x\z
proof
thus X is p-Semisimple implies for x,z holds (x\z)`` = x\z;
assume
A1: for x,z holds (x\z)`` = x\z;
now
let x;
(x\0.X)``=x\0.X by A1;
then (x`)`=x\0.X by Th2;
hence x``=x by Th2;
end;
hence thesis by Th54;
end;
theorem
X is p-Semisimple iff for x,u,z holds z\(z\(x\u)) = x\u
proof
thus X is p-Semisimple implies for x,u,z holds z\(z\(x\u)) = x\u;
assume
A1: for x,u,z holds z\(z\(x\u)) = x\u;
now
let x;
((x\0.X)`)` = x\0.X by A1;
then ((x\0.X)`)` = x by Th2;
hence x`` = x by Th2;
end;
hence thesis by Th54;
end;
theorem Th62: ::TL2232:
X is p-Semisimple iff for x st x`=0.X holds x=0.X
proof
thus X is p-Semisimple implies for x st x`=0.X holds x=0.X
proof
assume
A1: X is p-Semisimple;
let x;
assume x`=0.X;
then (x`)`=0.X by Def5;
hence thesis by A1;
end;
assume
A2: for x st x`=0.X holds x=0.X;
for x holds x`` = x
proof
let x;
(x\x``)`=x`\x``` by Th9
.=x`\x` by Th8
.=0.X by Def5;
then
A3: x\((x)`)`=0.X by A2;
((x)`)`\x=0.X by Th1;
hence thesis by A3,Def7;
end;
hence thesis by Th54;
end;
theorem Th63:
X is p-Semisimple iff for x,y holds x\y`=y\x`
proof
thus X is p-Semisimple implies for x,y holds x\y`=y\x` by Th57;
assume
A1: for x,y holds x\y`=y\x`;
now
let x;
x\(0.X)`=(x`)` by A1;
then x\0.X=(x`)` by Th2;
hence x=x`` by Th2;
end;
hence thesis by Th54;
end;
theorem
X is p-Semisimple iff for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u)
proof
thus X is p-Semisimple implies for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u) by
Lm9;
assume
A1: for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u);
for x,z holds z`\x` = x\z
proof
let x,z;
(z\x)`=(x\x)\(z\x) by Def5;
then (z\x)`=(x\z)\(x\x) by A1;
then (z\x)`=(x\z)\0.X by Def5;
then (z\x)`=x\z by Th2;
hence thesis by Th9;
end;
hence thesis by Th59;
end;
theorem
X is p-Semisimple iff for x,y,z holds (x\y)\(z\y)=x\z
proof
thus X is p-Semisimple implies for x,y,z holds (x\y)\(z\y)=x\z by Lm11;
assume
A1: for x,y,z holds (x\y)\(z\y)=x\z;
for x,z holds z`\x` = x\z
proof
let x,z;
(z\x)`=(x\x)\(z\x)by Def5;
then (z\x)`=x\z by A1;
hence thesis by Th9;
end;
hence thesis by Th59;
end;
theorem
X is p-Semisimple iff for x,y,z holds x\(y\z)=(z\y)\x`
proof
thus X is p-Semisimple implies for x,y,z holds x\(y\z)=(z\y)\x` by Lm13;
assume
A1: for x,y,z holds x\(y\z)=(z\y)\x`;
for x,y holds x\y`=y\x`
proof
let x,y;
x\y`=(y\0.X)\x` by A1;
hence thesis by Th2;
end;
hence thesis by Th63;
end;
theorem
X is p-Semisimple iff for x,y,z st y\x=z\x holds y=z
proof
thus X is p-Semisimple implies for x,y,z st y\x=z\x holds y=z by Lm14;
assume
A1: for x,y,z st y\x=z\x holds y=z;
for x,y holds x\(x\y) = y
proof
let x,y;
(x\(x\y))\y = 0.X by Th1;
then (x\(x\y))\y = y\y by Def5;
hence thesis by A1;
end;
hence thesis;
end;
theorem
X is p-Semisimple iff for x,y,z st x\y=x\z holds y=z
proof
thus X is p-Semisimple implies for x,y,z st x\y=x\z holds y=z by Lm12;
assume
A1: for x,y,z st x\y=x\z holds y=z;
for x st x`=0.X holds x=0.X
proof
let x;
assume x`=0.X;
then x`=(0.X)` by Def5;
hence thesis by A1;
end;
hence thesis by Th62;
end;
theorem
for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra
iff for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x\0.X=x )
proof
let X be non empty BCIStr_0;
thus X is p-Semisimple BCI-algebra implies for x,y,z being Element of X
holds (x\y)\(x\z)=z\y & x\0.X=x by Th2,Th56;
assume
A1: for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x\0.X=x;
A2: now
let x,y,z be Element of X;
((x\y)\(x\z))\(z\y)=(z\y)\(z\y) by A1
.=((z\y)\0.X)\(z\y) by A1
.=((z\y)\0.X)\((z\y)\0.X) by A1
.=(0.X)` by A1;
hence ((x\y)\(x\z))\(z\y)=0.X by A1;
(x\(x\y))\y=((x\0.X)\(x\y))\y by A1
.=(y\0.X)\y by A1
.=(y\0.X)\(y\0.X) by A1
.=(0.X)` by A1;
hence (x\(x\y))\y = 0.X by A1;
thus for x,y being Element of X holds x\(x\y) = y
proof
let x,y be Element of X;
x\(x\y)=(x\0.X)\(x\y) by A1;
then x\(x\y)= y\0.X by A1;
hence thesis by A1;
end;
end;
now
let x,y be Element of X;
assume that
A3: x\y = 0.X and
y\x = 0.X;
x=x\0.X by A1
.=(x\0.X)\(x\y) by A1,A3
.= y\0.X by A1;
hence x=y by A1;
end;
then
A4: X is being_BCI-4;
now
let x be Element of X;
x\x=(x\0.X)\x by A1
.=(x\0.X)\(x\0.X) by A1
.=(0.X)` by A1;
hence x\x=0.X by A1;
end;
then X is being_I;
hence thesis by A4,A2,Def26,Th1;
end;
theorem
for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra
iff (X is being_I &for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x
))
proof
let X be non empty BCIStr_0;
thus X is p-Semisimple BCI-algebra implies (X is being_I & for x,y,z being
Element of X holds x\(y\z)=z\(y\x) & x\0.X=x) by Th2,Th57;
assume that
A1: X is being_I and
A2: for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x;
A3: now
let x,y,z be Element of X;
thus x\x=0.X by A1;
((x\y)\(x\z))\(z\y)=(z\(x\(x\y)))\(z\y) by A2
.=(z\(y\(x\x)))\(z\y) by A2
.=(z\(y\0.X))\(z\y) by A1
.=(z\y)\(z\y) by A2;
hence ((x\y)\(x\z))\(z\y)=0.X by A1;
(x\(x\y))\y=(y\(x\x))\y by A2
.=(y\0.X)\y by A1
.=y\y by A2;
hence (x\(x\y))\y = 0.X by A1;
thus for x,y being Element of X holds x\(x\y) = y
proof
let x,y be Element of X;
x\(x\y)=y\(x\x) by A2;
then x\(x\y)= y\0.X by A1;
hence thesis by A2;
end;
end;
now
let x,y be Element of X;
assume that
A4: x\y = 0.X and
y\x = 0.X;
x=x\0.X by A2
.=y\(x\x) by A2,A4
.= y\0.X by A1;
hence x=y by A2;
end;
then X is being_BCI-4;
hence thesis by A1,A3,Def26,Th1;
end;
begin :: Several Classes of BCI-algebra----quasi-associative BCI-algebra
Lm15: (for x being Element of X holds x`<=x) implies for x,y being Element of
X holds (x\y)`=(y\x)`
proof
assume
A1: for x being Element of X holds x`<=x;
let x,y be Element of X;
(y\x)`=(y\x)``` by Th8
.=(y`\x`)`` by Th9
.=(y``\x``)` by Th9
.=((((x`)`)`)\y`)` by Th7
.=(x`\y`)` by Th8
.=(x\y)`` by Th9;
then (y\x)`<= (x\y)` by A1;
then
A2: ((y\x)`)\((x\y)`)=0.X;
(x\y)`=(((x\y)`)`)` by Th8
.=((x`\y`)`)` by Th9
.=(x``\y``)` by Th9
.=((((y)`)`)`\x`)` by Th7
.=(y`\x`)` by Th8
.=(y\x)`` by Th9;
then (x\y)`<= (y\x)` by A1;
then ((x\y)`)\((y\x)`)=0.X;
hence thesis by A2,Def7;
end;
Lm16: (for x,y being Element of X holds (x\y)`=(y\x)`)implies for x,y being
Element of X holds x`\y=(x\y)`
proof
assume
A1: for x,y being Element of X holds (x\y)`=(y\x)`;
let x,y be Element of X;
thus (x\y)`=x`\y` by Th9
.=y``\x by Th7
.=(y\0.X)`\x by A1
.=y`\x by Th2
.=x`\y by Th7;
end;
Lm17: (for x,y being Element of X holds x`\y=(x\y)`) implies for x,y being
Element of X holds (x\y)\(y\x) in BCK-part(X)
proof
assume
A1: for x,y being Element of X holds x`\y=(x\y)`;
let x,y be Element of X;
((x\y)\(y\x))`=(x\y)`\(y\x) by A1
.=(x`\y`)\(y\x) by Th9
.=(y``\x)\(y\x) by Th7
.=(y`\x)`\(y\x) by A1
.=((y\x)``)\(y\x) by A1
.=0.X by Th1;
then 0.X <= (x\y)\(y\x);
hence thesis;
end;
Lm18: (for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X))implies X
is quasi-associative
proof
assume
A1: for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X);
for x being Element of X holds (x`)`=x`
proof
let x be Element of X;
x\x`=(x\0.X)\x` by Th2;
then x\x` in {x2 where x2 is Element of X:0.X<=x2}by A1;
then ex x2 being Element of X st x\x`=x2 & 0.X<=x2;
then (x\x`)`=0.X;
then
A2: x`\(x`)`=0.X by Th9;
x`\x=x`\(x\0.X) by Th2;
then x`\x in {x1 where x1 is Element of X:0.X<=x1} by A1;
then ex x1 being Element of X st x`\x=x1 & 0.X<=x1;
then (x`\x)`=0.X;
then (x`)`\x`=0.X by Th9;
hence thesis by A2,Def7;
end;
hence thesis;
end;
Lm19: (for x being Element of X holds x`<=x) iff for x,y,z being Element of X
holds (x\y)\z<=x\(y\z)
proof
thus (for x being Element of X holds x`<=x) implies for x,y,z being Element
of X holds (x\y)\z<=x\(y\z)
proof
assume
A1: for x being Element of X holds x`<=x;
let x,y,z be Element of X;
(x\(x\(y\z)))\(y\z) =0.X by Th1;
then
A2: ((x\(x\(y\z)))\y)\((y\z)\y) =0.X by Th4;
((x\y)\z)\(x\(y\z)) = ((x\y)\(x\(y\z)))\z by Th7
.=((x\(x\(y\z)))\y)\z by Th7;
then ((x\y)\z)\(x\(y\z))\(((y\z)\y)\z) =0.X by A2,Th4;
then
A3: ((x\y)\z)\(x\(y\z))\(((y\y)\z)\z) =0.X by Th7;
z`<=z by A1;
then z`\z=0.X;
then ((x\y)\z)\(x\(y\z))\0.X =0.X by A3,Def5;
then ((x\y)\z)\(x\(y\z)) =0.X by Th2;
hence thesis;
end;
assume
A4: for x,y,z being Element of X holds (x\y)\z<=x\(y\z);
let x be Element of X;
(0.X)`\x <= (x`)` by A4;
then x`<=(x`)`by Def5;
then x`\((x`)`)=0.X;
then ((x`)`)`\x=0.X by Th7;
then x`\x=0.X by Th8;
hence thesis;
end;
theorem Th71:
X is quasi-associative iff for x being Element of X holds x`<=x
proof
thus X is quasi-associative implies for x being Element of X holds x`<=x
proof
assume
A1: X is quasi-associative;
let x be Element of X;
(x`)`\x=0.X by Th1;
then x`\x=0.X by A1;
hence thesis;
end;
assume for x being Element of X holds x`<=x;
then for x,y being Element of X holds (x\y)`=(y\x)` by Lm15;
then for x,y being Element of X holds x`\y=(x\y)` by Lm16;
then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm17;
hence thesis by Lm18;
end;
theorem Th72:
X is quasi-associative iff for x,y being Element of X holds (x\y )`=(y\x)`
proof
thus X is quasi-associative implies for x,y being Element of X holds (x\y)`=
(y\x)`
proof
assume X is quasi-associative;
then for x being Element of X holds x`<=x by Th71;
hence thesis by Lm15;
end;
assume for x,y being Element of X holds (x\y)`=(y\x)`;
then for x,y being Element of X holds x`\y=(x\y)` by Lm16;
then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm17;
hence thesis by Lm18;
end;
theorem Th73:
X is quasi-associative iff for x,y being Element of X holds x`\y =(x\y)`
proof
thus X is quasi-associative implies for x,y being Element of X holds x`\y=(x
\y)`
proof
assume X is quasi-associative;
then for x,y being Element of X holds (x\y)`=(y\x)` by Th72;
hence thesis by Lm16;
end;
assume for x,y being Element of X holds x`\y=(x\y)`;
then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm17;
hence thesis by Lm18;
end;
theorem
X is quasi-associative iff for x,y being Element of X holds (x\y)\(y\x
) in BCK-part(X)
proof
thus X is quasi-associative implies for x,y being Element of X holds (x\y)\(
y\x) in BCK-part(X)
proof
assume X is quasi-associative;
then for x,y being Element of X holds x`\y=(x\y)` by Th73;
hence thesis by Lm17;
end;
thus thesis by Lm18;
end;
theorem
X is quasi-associative iff for x,y,z being Element of X holds (x\y)\z
<=x\(y\z)
proof
thus X is quasi-associative implies for x,y,z being Element of X holds (x\y)
\z<=x\(y\z)
proof
assume X is quasi-associative;
then for x being Element of X holds x`<=x by Th71;
hence thesis by Lm19;
end;
assume for x,y,z being Element of X holds (x\y)\z<=x\(y\z);
then for x being Element of X holds x`<=x by Lm19;
hence thesis by Th71;
end;
begin :: Several Classes of BCI-algebra----alternative BCI-algebra
theorem Th76:
X is alternative implies x` = x & x\(x\y) = y & (x\y)\y = x
proof
assume
A1: X is alternative;
then x\(x\x) = (x\x)\x;
then x\0.X = (x\x)\x by Def5;
then x\0.X = x` by Def5;
hence x` = x by Th2;
y\(y\y) = (y\y)\y by A1;
then y\0.X = (y\y)\y by Def5;
then y\0.X = y` by Def5;
then
A2: y = y` by Th2;
x\(x\y) = (x\x)\y by A1;
hence x\(x\y) = y by A2,Def5;
(x\y)\y=x\(y\y) by A1;
then (x\y)\y=x\0.X by Def5;
hence thesis by Th2;
end;
theorem
X is alternative & x\a=x\b implies a=b
proof
assume that
A1: X is alternative and
A2: x\a=x\b;
(x\x)\a=x\(x\b) by A1,A2;
then (x\x)\a=(x\x)\b by A1;
then a`=(x\x)\b by Def5;
then a`=b` by Def5;
then a=b` by A1,Th76;
hence thesis by A1,Th76;
end;
theorem
X is alternative & a\x=b\x implies a=b
proof
assume that
A1: X is alternative and
A2: a\x=b\x;
a\(x\x)=(b\x)\x by A1,A2;
then a\(x\x)=b\(x\x) by A1;
then a\0.X=b\(x\x) by Def5;
then a\0.X=b\0.X by Def5;
then a=b\0.X by Th2;
hence thesis by Th2;
end;
theorem
X is alternative & x\y=0.X implies x=y
proof
assume that
A1: X is alternative and
A2: x\y=0.X;
x\(x\y)=x by A2,Th2;
then (x\x)\y=x by A1;
then y`=x by Def5;
hence thesis by A1,Th76;
end;
theorem
X is alternative & (x\a)\b = 0.X implies a=x\b & b=x\a
proof
assume that
A1: X is alternative and
A2: (x\a)\b = 0.X;
(x\a)\(b\b) = b` by A1,A2;
then (x\a)\0.X = b` by Def5;
then x\a = b` by Th2;
then x\(x\a) = x\b by A1,Th76;
then (x\x)\a = x\b by A1;
then a` = x\b by Def5;
then a=x\b by A1,Th76;
hence thesis by A1,Th76;
end;
Lm20: X is alternative iff X is associative
proof
thus X is alternative implies X is associative
proof
assume
A1: X is alternative;
for x,y,z being Element of X holds (x\y)\z = x\(y\z)
proof
let x,y,z be Element of X;
(((x\y)\y)\((x\y)\z))\(z\y)=0.X by Th1;
then ((((x\y)\y)\((x\y)\z))\(y\z))\((z\y)\(y\z))=0.X by Th4;
then ((((x\y)\y)\((x\y)\z))\(y\z))\((z\(y\z))\y)=0.X by Th7;
then ((((x\y)\y)\((x\y)\z))\(y\z))\((z`\(y\z))\y)=0.X by A1,Th76;
then ((((x\y)\y)\((x\y)\z))\(y\z))\((z`\(y\z))\y`)=0.X by A1,Th76;
then
A2: ((((x\y)\y)\((x\y)\z))\(y\z))\0.X=0.X by Def3;
((x\y)\z)\(x\(y\z))=((x\y)\(x\(y\z)))\z by Th7;
then ((x\y)\z)\(x\(y\z))=((x\(x\(y\z)))\y)\z by Th7;
then ((x\y)\z)\(x\(y\z))=(((x\x)\(y\z))\y)\z by A1;
then ((x\y)\z)\(x\(y\z))=(((y\z)`)\y)\z by Def5;
then ((x\y)\z)\(x\(y\z))=((y\z)\y)\z by A1,Th76;
then ((x\y)\z)\(x\(y\z))=((y\y)\z)\z by Th7;
then ((x\y)\z)\(x\(y\z))=z`\z by Def5;
then
A3: ((x\y)\z)\(x\(y\z))=0.X by A1,Th76;
(x\(y\z))\((x\y)\z)=(((x\y)\y)\(y\z))\((x\y)\z) by A1,Th76
.=(((x\y)\y)\((x\y)\z))\(y\z) by Th7;
then (x\(y\z))\((x\y)\z)=0.X by A2,Th2;
hence thesis by A3,Def7;
end;
hence thesis;
end;
assume X is associative;
then
for x,y being Element of X holds x\(x\y) = (x\x)\y & (x\y)\y=x\(y\y);
hence thesis;
end;
Lm21: X is alternative implies X is implicative
by Th76;
registration
cluster alternative -> associative for BCI-algebra;
coherence by Lm20;
cluster associative -> alternative for BCI-algebra;
coherence;
cluster alternative -> implicative for BCI-algebra;
coherence by Lm21;
end;
theorem
X is alternative implies (x\(x\y))\(y\x) = x
proof
assume
A1: X is alternative;
then x\(x\y)=y by Th76;
hence thesis by A1,Th76;
end;
theorem
X is alternative implies y\(y\(x\(x\y))) = y
proof
assume X is alternative;
then y\(y\(x\(x\y)))=y\(y\y) by Th76
.=y\0.X by Def5
.= y by Th2;
hence thesis;
end;
begin
:: Several Classes of BCI-algebra-
::-implicative & positive-implicative & weakly-positive-implicative BCI-algebra
Lm22: X is associative implies X is weakly-positive-implicative
proof
assume
A1: X is associative;
for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
proof
let x,y,z be Element of X;
(x\y)\z=x\(y\z) by A1;
then (x\y)\z=(x\0.X)\(y\z) by Th2;
then (x\y)\z=(x\(z\z))\(y\z) by Def5;
hence thesis by A1;
end;
hence thesis;
end;
Lm23: X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative
BCI-algebra
proof
assume
A1: X is p-Semisimple BCI-algebra;
for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
proof
let x,y,z be Element of X;
((x\z)\z)\(y\z)=(x\z)\y by A1,Lm11
.=(x\z)\(y\0.X) by Th2
.=(x\y)\(z\0.X) by A1,Lm9;
hence thesis by Th2;
end;
hence thesis by Def23;
end;
registration
cluster associative -> weakly-positive-implicative for BCI-algebra;
coherence by Lm22;
cluster p-Semisimple -> weakly-positive-implicative for BCI-algebra;
coherence by Lm23;
end;
theorem
for X being non empty BCIStr_0 holds (X is implicative BCI-algebra iff
for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x &(x\(x\y))
\(y\x)=y\(y\x) )
proof
let X be non empty BCIStr_0;
thus X is implicative BCI-algebra implies for x,y,z being Element of X holds
((x\y)\(x\z))\(z\y)=0.X & x\0.X=x & (x\(x\y))\(y\x)=y\(y\x) by Def24,Th1,Th2;
thus (for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x &
(x\(x\y))\(y\x)=y\(y\x)) implies X is implicative BCI-algebra
proof
assume
A1: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X
=x &(x\(x\y))\(y\x)=y\(y\x);
A2: now
let x,y,z be Element of X;
thus ((x\y)\(x\z))\(z\y)=0.X by A1;
(x\(x\y))\y=((x\0.X)\(x\y))\y by A1
.=((x\0.X)\(x\y))\(y\0.X) by A1;
hence (x\(x\y))\y = 0.X by A1;
end;
now
let x,y be Element of X;
assume that
A3: x\y = 0.X and
A4: y\x = 0.X;
x=x\0.X by A1
.=(y\(y\x))\(x\y) by A1,A3
.=y\0.X by A1,A3,A4;
hence x=y by A1;
end;
then
A5: X is being_BCI-4;
now
let x be Element of X;
x\x=(x\0.X)\x by A1
.=(x\0.X)\(x\0.X) by A1
.=((x\0.X)\(x\0.X))\0.X by A1
.=((x\0.X)\(x\0.X))\(0.X)` by A1;
hence x\x=0.X by A1;
end;
then X is being_I;
hence thesis by A1,A5,A2,Def24,Th1;
end;
end;
theorem Th84:
X is weakly-positive-implicative iff for x,y being Element of X
holds x\y=((x\y)\y)\y`
proof
thus X is weakly-positive-implicative implies for x,y being Element of X
holds x\y=((x\y)\y)\y`
proof
assume
A1: X is weakly-positive-implicative;
let x,y be Element of X;
(x\0.X)\y=((x\y)\y)\y` by A1;
hence thesis by Th2;
end;
assume
A2: for x,y being Element of X holds x\y=((x\y)\y)\y`;
for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
proof
let x,y,z be Element of X;
((x\z)\(y\z))\(x\y)=0.X by Def3;
then (((x\z)\(y\z))\z)\((x\y)\z)=0.X by Th4;
then
A3: (((x\z)\z)\(y\z))\((x\y)\z)=0.X by Th7;
(((x\z)\z)\(((x\z)\z)\(y\z)))\(y\z)=0.X by Th1;
then ((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\((y\z)\z`)=0.X by Th4;
then (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\(((y\z)\z`)\y) =0.X by Th4;
then (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\(((y\z)\z`)\(y\0.X))=0.X by Th2
;
then
A4: (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\0.X=0.X by Def3;
((x\y)\z)\(((x\z)\z)\(y\z)) =((x\z)\y)\(((x\z)\z)\(y\z)) by Th7
.=((((x\z)\z)\z`)\y)\(((x\z)\z)\(y\z)) by A2
.=((((x\z)\z)\z`)\(((x\z)\z)\(y\z)))\y by Th7
.=(((x\z)\z)\(((x\z)\z)\(y\z))\z`)\y by Th7;
then ((x\y)\z)\(((x\z)\z)\(y\z))=0.X by A4,Th2;
hence thesis by A3,Def7;
end;
hence thesis;
end;
Lm24: X is weakly-positive-implicative implies (x\(x\y))\(y\x)=((y\(y\x))\(y\x
))\(x\y)
proof
assume
A1: X is weakly-positive-implicative;
((x\(x\y))\(y\(x\y)))\(x\y)=0.X by Def3;
then ((x\(x\y))\(x\y))\(y\(x\y))=0.X by Th7;
then (((x\(x\y))\(x\y))\((x\y)`))\((y\(x\y))\((x\y)`))=0.X by Th4;
then ((((x\(x\y))\(x\y))\((x\y)`))\(y\x))\(((y\(x\y)) \((x\y)`))\(y\x))=0.X
by Th4;
then ((x\(x\y))\(y\x))\(((y\(x\y))\((x\y)`))\(y\x))=0.X by A1,Th84;
then
((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\((x\y)`\(y\x))) =0.X by A1;
then
((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\(((x\x)\(x\y))\(y\x))) =0.
X by Def5;
then ((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\0.X) =0.X by Th1;
then ((x\(x\y))\(y\x))\(((y\(x\y))\(y\x))\(y\x)) =0.X by Th2;
then ((x\(x\y))\(y\x))\(((y\(y\x))\(x\y))\(y\x)) =0.X by Th7;
then
A2: ((x\(x\y))\(y\x))\(((y\(y\x))\(y\x))\(x\y))=0.X by Th7;
((y\(y\x))\(y\x))\(x\(y\x))=0.X by Th1;
then (((y\(y\x))\(y\x))\(x\y))\((x\(y\x))\(x\y))=0.X by Th4;
then (((y\(y\x))\(y\x))\(x\y))\((x\(x\y))\(y\x))=0.X by Th7;
hence thesis by A2,Def7;
end;
Lm25: X is positive-implicative iff X is weakly-positive-implicative
proof
thus X is positive-implicative implies X is weakly-positive-implicative
proof
assume
A1: X is positive-implicative;
for x,y being Element of X holds x\y=((x\y)\y)\y`
proof
let x,y be Element of X;
((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\((x\y)\(x\(x\(x\y)))) by A1;
then ((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\((x\y)\(x\y)) by Th8;
then ((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\0.X by Def5;
then ((x\y)\((x\y)\x))\(x\(x\y))=x\y by Th2;
then ((x\y)\((x\x)\y))\(x\(x\y))=x\y by Th7;
then ((x\y)\(x\(x\y)))\((x\x)\y)=x\y by Th7;
then ((x\(x\(x\y)))\y)\((x\x)\y)=x\y by Th7;
then ((x\y)\y)\((x\x)\y)=x\y by Th8;
hence thesis by Def5;
end;
hence thesis by Th84;
end;
assume
A2: X is weakly-positive-implicative;
for x,y being Element of X holds (x\(x\y))\(y\x)=x\(x\(y\(y\x)))
proof
let x,y be Element of X;
A3: (x\(x\(y\(y\x)))) \ ((x\(x\y))\(y\x)) =(x\(x\(y\(y\x)))) \ (((y\(y\x)
)\(y\x))\(x\y)) by A2,Lm24;
(y\(y\x))\x = 0.X by Th1;
then (x\x)\(x\(y\(y\x)))=0.X by Th4;
then (x\(y\(y\x)))`=0.X by Def5;
then x\(x\(y\(y\x)))=((x\(x\(y\(y\x))))\(x\(y\(y\x))))\0.X by A2,Th84;
then x\(x\(y\(y\x)))=(x\(x\(y\(y\x))))\(x\(y\(y\x))) by Th2;
then (x\(x\(y\(y\x))))\( (y\(y\x))\(x\(y\(y\x))) )=0.X by Th1;
then
(x\(x\(y\(y\x)))) \(((y\(y\x))\(y\x))\(x\y)) \(((y\(y\x))\(x\(y\(y\x)
)))\(((y\(y\x))\(y\x))\(x\y)))=0.X by Th4;
then
A4: (x\(x\(y\(y\x)))) \(((y\(y\x))\(y\x))\(x\y)) \(((y\(y\x))\(((y\(y\x))
\(y\x))\(x\y)))\(x\(y\(y\x))))=0.X by Th7;
((y\(y\x))\(((y\(y\x))\(y\x))\(x\y)))\((x\y)\(y\x)`) =((((y\(y\x))\(y
\x))\((y\x)`))\(((y\(y\x))\(y\x))\(x\y))) \((x\y)\((y\x)`)) by A2,Th84
.=0.X by Th1;
then
(((y\(y\x))\(((y\(y\x))\(y\x))\(x\y)))\(x\(y\(y\x)))) \(((x\y)\((y\x)
`))\(x\(y\(y\x))))=0.X by Th4;
then
(x\(x\(y\(y\x)))) \(((y\(y\x))\(y\x))\(x\y)) \(((x\y)\((y\x)`))\(x\(y
\(y\x))))=0.X by A4,Th3;
then
A5: (x\(x\(y\(y\x)))) \(((y\(y\x))\(y\x))\(x\y)) \(((x\y)\(x\(y\(y\x))))\
((y\x)`))=0.X by Th7;
((x\y)\(x\(y\(y\x))))\((y\(y\x))\y)=0.X by Th1;
then ((x\y)\(x\(y\(y\x))))\((y\y)\(y\x))=0.X by Th7;
then (x\(x\(y\(y\x)))) \(((y\(y\x))\(y\x))\(x\y))\0.X=0.X by A5,Def5;
then
A6: (x\(x\(y\(y\x))))\((x\(x\y))\(y\x))=0.X by A3,Th2;
((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X by Th10;
hence thesis by A6,Def7;
end;
hence thesis;
end;
registration
cluster positive-implicative -> weakly-positive-implicative for BCI-algebra;
coherence by Lm25;
cluster alternative -> weakly-positive-implicative for BCI-algebra;
coherence;
end;
theorem
X is weakly-positive-implicative BCI-algebra implies for x,y being
Element of X holds (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y) by Lm24;
theorem
for X being non empty BCIStr_0 holds (X is positive-implicative
BCI-algebra iff for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\
0.X=x & x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y) )
proof
let X be non empty BCIStr_0;
thus X is positive-implicative BCI-algebra implies for x,y,z being Element
of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x & x\y=((x\y)\y)\y` & (x\(x\y))\(y\
x)=((y\(y\x))\(y\x))\(x\y) by Lm24,Th1,Th2,Th84;
assume
A1: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x
& x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y);
now
let x be Element of X;
((x\0.X)\(x\0.X))\(0.X)`=0.X by A1;
then ((x\0.X)\(x\0.X))\0.X=0.X by A1;
then ((x\0.X)\x)\0.X=0.X by A1;
then (x\x)\0.X=0.X by A1;
hence x\x=0.X by A1;
end;
then
A2: X is being_I;
now
let x,y be Element of X;
assume x\y = 0.X & y\x = 0.X;
then (x\0.X)\0.X=((y\0.X)\0.X)\0.X by A1;
then (x\0.X)=((y\0.X)\0.X)\0.X by A1;
then x=((y\0.X)\0.X)\0.X by A1;
then x=(y\0.X)\0.X by A1;
then x=y\0.X by A1;
hence x=y by A1;
end;
then
A3: X is being_BCI-4;
now
let x,y,z be Element of X;
thus ((x\y)\(x\z))\(z\y)=0.X by A1;
((x\0.X)\(x\y))\(y\0.X)=0.X by A1;
then (x\(x\y))\(y\0.X)=0.X by A1;
hence (x\(x\y))\y = 0.X by A1;
end;
then X is weakly-positive-implicative BCI-algebra by A1,A2,A3,Th1,Th84;
hence thesis by Lm25;
end;