:: BCI-Algebras with Condition (S) and Their Properties
:: by Tao Sun , Junjie Zhao and Xiquan Liang
::
:: Received November 24, 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 BCIALG_1, STRUCT_0, BINOP_1, SUBSET_1, XBOOLE_0, RELAT_1,
FUNCT_1, FUNCT_5, ZFMISC_1, NUMBERS, FINSEQ_1, XXREAL_0, SUPINF_2,
VECTSP_1, ALGSTR_0, RLVECT_1, ARYTM_3, SETWISEO, GROUP_1, CARD_1, NAT_1,
NEWTON, POWER, FINSOP_1, ORDINAL4, BCIALG_2, TARSKI, FILTER_0, BCIALG_4;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_5, STRUCT_0,
ALGSTR_0, BCIALG_1, RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, FINSEQ_1,
FINSOP_1, SETWISEO, FUNCT_1, FUNCT_2, FINSEQ_4, XCMPLX_0, RLVECT_1,
NAT_1, BCIALG_2, VECTSP_1;
constructors BINOP_1, VECTSP_2, FINSOP_1, SETWISEO, FINSEQ_4, BCIALG_2,
FUNCT_5, NAT_1;
registrations BCIALG_1, RELAT_1, STRUCT_0, ORDINAL1, XXREAL_0, VECTSP_1,
BCIALG_2, CARD_1, FINSEQ_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions STRUCT_0, RLVECT_1, ALGSTR_0;
equalities STRUCT_0, BINOP_1, BCIALG_1, FINSEQ_1, ALGSTR_0;
expansions STRUCT_0, BINOP_1, BCIALG_1;
theorems TARSKI, STRUCT_0, BCIALG_1, FINSEQ_1, FINSOP_1, SETWISEO, NAT_1,
BINOP_1, BCIALG_2;
schemes BINOP_1, NAT_1, CLASSES1;
begin :: Definition and Elementary Properties of BCI-Algebras with Condition(S)
definition
struct (BCIStr_0,ZeroStr) BCIStr_1 (# carrier -> set, ExternalDiff,
InternalDiff -> BinOp of the carrier, ZeroF -> Element of the carrier #);
end;
registration
cluster non empty strict for BCIStr_1;
existence
proof
set A = the non empty set,m = the BinOp of A,u = the Element of A;
take BCIStr_1(#A,m,m,u#);
thus the carrier of BCIStr_1(#A,m,m,u#) is non empty;
thus thesis;
end;
end;
definition
let A be BCIStr_1;
let x,y be Element of A;
func x * y -> Element of A equals
(the ExternalDiff of A).(x,y);
coherence;
end;
definition
let IT be non empty BCIStr_1;
attr IT is with_condition_S means
:Def2:
for x,y,z being Element of IT holds (x\y)\z = x\(y*z);
end;
definition
func BCI_S-EXAMPLE -> BCIStr_1 equals
BCIStr_1 (# {0}, op2, op2, op0 #);
coherence;
end;
registration
cluster BCI_S-EXAMPLE -> strict 1-element;
coherence;
end;
Lm1: BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is
being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 &
BCI_S-EXAMPLE is with_condition_S
by STRUCT_0:def 10;
registration
cluster BCI_S-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5
with_condition_S;
coherence by Lm1;
end;
registration
cluster strict being_B being_C being_I being_BCI-4 with_condition_S for non
empty BCIStr_1;
existence by Lm1;
end;
definition
mode BCI-Algebra_with_Condition(S) is being_B being_C being_I being_BCI-4
with_condition_S non empty BCIStr_1;
end;
reserve X for non empty BCIStr_1;
reserve d for Element of X;
reserve n,m,k for Nat;
reserve f for sequence of the carrier of X;
definition
let X be BCI-Algebra_with_Condition(S);
let x,y be Element of X;
func Condition_S(x,y) -> non empty Subset of X equals
{t where t is Element
of X: t\x <= y};
coherence
proof
set a = 0.X\((0.X\x)\y);
set Y={t where t is Element of X: t\x <= y};
A1: now
let y1 be object;
assume y1 in Y;
then ex x1 being Element of X st y1=x1 & x1\x <= y;
hence y1 in the carrier of X;
end;
(a\x)\y = ((0.X\x)\((0.X\x)\y))\y by BCIALG_1:7
.= (((0.X\x)\0.X)\((0.X\x)\y))\y by BCIALG_1:2
.= (((0.X\x)\0.X)\((0.X\x)\y))\(y\0.X) by BCIALG_1:2
.= 0.X by BCIALG_1:1;
then a\x <= y;
then a in Y;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem
for X be BCI-Algebra_with_Condition(S),x,y,u,v being Element of X st u
in Condition_S(x,y) & v <= u holds v in Condition_S(x,y)
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,u,v be Element of X;
assume that
A1: u in Condition_S(x,y) and
A2: v <= u;
v\x <= u\x by A2,BCIALG_1:5;
then
A3: (v\x)\(u\x) = 0.X;
ex u1 being Element of X st u=u1 & u1\x <= y by A1;
then (u\x)\y = 0.X;
then (v\x)\y = 0.X by A3,BCIALG_1:3;
then v\x <= y;
hence thesis;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,y being Element
of X holds ex a be Element of Condition_S(x,y) st for z being Element of
Condition_S(x,y) holds z <= a
proof
let X be BCI-Algebra_with_Condition(S);
let x,y be Element of X;
((x*y)\x)\y = (x*y)\(x*y) by Def2
.= 0.X by BCIALG_1:def 5;
then (x*y)\x <= y;
then (x*y) in {t where t is Element of X: t\x <= y};
then consider u being Element of Condition_S(x,y) such that
A1: u =x * y;
take u;
for z being Element of Condition_S(x,y) holds z <= u
proof
let z be Element of Condition_S(x,y);
z in {t where t is Element of X: t\x <= y};
then consider z1 being Element of X such that
A2: z=z1 and
A3: z1\x <= y;
z\u = (z1\x)\y by A1,A2,Def2
.= 0.X by A3;
hence thesis;
end;
hence thesis;
end;
Lm2: for X being BCI-Algebra_with_Condition(S) holds for x,y being Element of
X holds ((x*y)\x <= y & for t being Element of X st t\x <= y holds t <= (x*y))
proof
let X be BCI-Algebra_with_Condition(S);
let x,y be Element of X;
A1: for t being Element of X holds (t\x <= y implies t <= (x*y))
by Def2;
((x*y)\x)\y = (x*y)\(x*y) by Def2
.= 0.X by BCIALG_1:def 5;
hence thesis by A1;
end;
Lm3: X is BCI-algebra & (for x,y being Element of X holds ((x*y)\x <= y & for
t being Element of X st t\x <= y holds t <= (x*y))) implies X is
BCI-Algebra_with_Condition(S)
proof
assume that
A1: X is BCI-algebra and
A2: for x,y being Element of X holds ((x*y)\x <= y & for t being Element
of X st t\x <= y holds t <= (x*y));
for x,y,z being Element of X holds (x\y)\z = x\(y*z)
proof
let x,y,z be Element of X;
(y*z)\y <= z by A2;
then
A3: ((y*z)\y)\z = 0.X;
(x\((x\y)\z))\y = (x\y)\((x\y)\z) by A1,BCIALG_1:7
.= ((x\y)\0.X)\((x\y)\z) by A1,BCIALG_1:2;
then ((x\((x\y)\z))\y)\(z\0.X) = 0.X by A1,BCIALG_1:11;
then (x\((x\y)\z))\y <= z\0.X;
then (x\((x\y)\z))\y <= z by A1,BCIALG_1:2;
then x\((x\y)\z) <= y*z by A2;
then (x\((x\y)\z))\(y*z) = 0.X;
then
A4: (x\(y*z))\((x\y)\z) = 0.X by A1,BCIALG_1:7;
((x\y)\(x\(y*z)))\((y*z)\y) = 0.X by A1,BCIALG_1:11;
then ((x\y)\(x\(y*z)))\z = 0.X by A1,A3,BCIALG_1:3;
then ((x\y)\z)\(x\(y*z)) = 0.X by A1,BCIALG_1:7;
hence thesis by A1,A4,BCIALG_1:def 7;
end;
hence thesis by A1,Def2;
end;
theorem
X is BCI-algebra & (for x,y being Element of X holds ((x*y)\x <= y &
for t being Element of X st t\x <= y holds t <= (x*y))) iff X is
BCI-Algebra_with_Condition(S) by Lm2,Lm3;
definition
let X be p-Semisimple BCI-algebra;
func Adjoint_pGroup X -> strict AbGroup means
the carrier of it = the
carrier of X & (for x,y being Element of X holds (the addF of it).(x,y) = x\(0.
X\y)) & 0.it = 0.X;
existence
proof
reconsider A0=0.X as Element of X;
defpred P[Element of X, Element of X, Element of X] means ex x,y being
Element of X st $1=x & $2=y & $3 = x\(0.X\y);
A1: for a,b being Element of X ex c being Element of X st P[a,b,c]
proof
let a,b be Element of X;
reconsider x=a,y=b as Element of X;
reconsider c = x\(0.X\y) as Element of X;
take c;
thus thesis;
end;
consider h being BinOp of the carrier of X such that
A2: for a,b being Element of X holds P[a,b,h.(a,b)] from BINOP_1:sch 3
(A1);
set G=addLoopStr (# the carrier of X,h,A0 #);
A3: for x,y being Element of X holds h.(x,y)=x\(0.X\y)
proof
let x,y be Element of X;
ex x9,y9 being Element of X st x=x9 & y=y9 & h.(x,y)= x9\(0.X\y9) by A2;
hence thesis;
end;
A4: for a being Element of X ex b being Element of X st ex x being Element
of X st a=x & x\(0.X\b) = 0.X & b\(0.X\x) = 0.X
proof
let a be Element of X;
reconsider x=a as Element of X;
reconsider b=0.X\x as Element of X;
A5: b\(0.X\x) = 0.X by BCIALG_1:def 5;
take b;
x\(0.X\b) = x\x`` .= x\x by BCIALG_1:54
.= 0.X by BCIALG_1:def 5;
hence thesis by A5;
end;
G is Abelian add-associative right_zeroed right_complementable
proof
thus G is Abelian
proof
let a,b be Element of G;
reconsider x=a,y=b as Element of X;
thus a+b=x\(0.X\y) by A3
.=y\(0.X\x) by BCIALG_1:57
.=b+a by A3;
end;
hereby
let a,b,c be Element of G;
reconsider x=a,y=b,z=c as Element of X;
thus (a+b)+c =h.(x\(0.X\y),z) by A3
.=(x\(0.X\y))\(0.X\z) by A3
.= (y\(0.X\x))\(0.X\z) by BCIALG_1:57
.= (y\(0.X\z))\(0.X\x) by BCIALG_1:7
.= x\(0.X\(y\(0.X\z))) by BCIALG_1:57
.= h.(x,y\(0.X\z)) by A3
.=a+(b+c) by A3;
end;
hereby
let a be Element of G;
reconsider x=a as Element of X;
thus a+0.G = x\(0.X\0.X) by A3
.= x\0.X by BCIALG_1:2
.= a by BCIALG_1:2;
end;
let a be Element of G;
consider b being Element of X such that
A6: ex x being Element of X st a=x & x\(0.X\b) = 0.X & b\(0.X\x) = 0.X by A4;
reconsider b as Element of G;
take b;
thus thesis by A3,A6;
end;
then reconsider G as strict AbGroup;
take G;
thus thesis by A3;
end;
uniqueness
proof
thus for G1,G2 being strict AbGroup st the carrier of G1 = the carrier of
X & (for x,y being Element of X holds (the addF of G1).(x,y) = x\(0.X\y)) & 0.
G1 = 0.X & the carrier of G2 = the carrier of X & (for x,y being Element of X
holds (the addF of G2).(x,y) = x\(0.X\y)) & 0.G2 = 0.X holds G1=G2
proof
let G1,G2 be strict AbGroup;
assume that
A7: the carrier of G1 = the carrier of X and
A8: for x,y being Element of X holds (the addF of G1).(x,y) = x\(0. X\y) and
A9: 0.G1 = 0.X & the carrier of G2 = the carrier of X and
A10: for x,y being Element of X holds (the addF of G2).(x,y) = x\(0. X\y) and
A11: 0.G2 = 0.X;
now
let a,b be Element of G1;
reconsider x = a, y = b as Element of X by A7;
thus (the addF of G1).(a,b) = x\(0.X\y) by A8
.= (the addF of G2).(a,b) by A10;
end;
hence thesis by A7,A9,A11,BINOP_1:2;
end;
end;
end;
::$CT
theorem Th4:
for X being BCI-algebra holds X is p-Semisimple iff for x,y being
Element of X st x\y = 0.X holds x=y
proof
let X be BCI-algebra;
thus X is p-Semisimple implies for x,y being Element of X st x\y = 0.X holds
x=y
proof
assume
A1: X is p-Semisimple;
for x,y being Element of X st x\y = 0.X holds x=y
proof
let x,y be Element of X;
assume
A2: x\y = 0.X;
0.X\(x\y) = (y\x)\(0.X)` by A1,BCIALG_1:66
.= (y\x)\0.X by BCIALG_1:def 5
.= y\x by BCIALG_1:2;
then y\x = 0.X by A2,BCIALG_1:def 5;
hence thesis by A2,BCIALG_1:def 7;
end;
hence thesis;
end;
assume
A3: for x,y being Element of X st x\y = 0.X holds x=y;
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\y)\(x\y) by BCIALG_1:7
.= 0.X by BCIALG_1:def 5;
hence thesis by A3;
end;
hence thesis;
end;
theorem
for X being BCI-Algebra_with_Condition(S) st X is p-Semisimple holds
for x,y being Element of X holds x*y = x\(0.X\y)
proof
let X be BCI-Algebra_with_Condition(S);
assume
A1: X is p-Semisimple;
for x,y being Element of X holds x*y = x\(0.X\y)
proof
let x,y be Element of X;
set z1 = x\(0.X\y);
set z2 = x * y;
((x\(0.X\y))\x)\y = ((x\x)\(0.X\y))\y by BCIALG_1:7
.= (0.X\(0.X\y))\y by BCIALG_1:def 5
.= (0.X\y)\(0.X\y) by BCIALG_1:7
.= 0.X by BCIALG_1:def 5;
then (x\(0.X\y))\x <= y;
then z1 <= z2 by Lm2;
then
A2: z1\z2 = 0.X;
A3: for t being Element of X st t\x <= y holds t <= (x\(0.X\y))
proof
let t be Element of X;
assume t\x <= y;
then (t\x)\y = 0.X;
then t\(x\(0.X\y)) = t\(x\(0.X\(t\x))) by A1,Th4
.= t\(x\(x\(t\0.X))) by A1,BCIALG_1:57
.= t\(t\0.X) by A1
.= t\t by BCIALG_1:2
.= 0.X by BCIALG_1:def 5;
hence thesis;
end;
(x*y)\x <= y by Lm2;
then z2 <= z1 by A3;
then z2\z1 = 0.X;
hence thesis by A2,BCIALG_1:def 7;
end;
hence thesis;
end;
theorem Th6: :: Commutativity
for X being BCI-Algebra_with_Condition(S) holds for x,y being
Element of X holds x*y = y*x
proof
let X be BCI-Algebra_with_Condition(S);
let x,y be Element of X;
(y*x)\y <= x by Lm2;
then ((y*x)\y)\x = 0.X;
then ((y*x)\x)\y = 0.X by BCIALG_1:7;
then (y*x)\x <= y;
then (y*x) <= (x*y) by Lm2;
then
A1: (y*x)\(x*y) = 0.X;
(x*y)\x <= y by Lm2;
then ((x*y)\x)\y = 0.X;
then ((x*y)\y)\x = 0.X by BCIALG_1:7;
then (x*y)\y <= x;
then (x*y) <= (y*x) by Lm2;
then (x*y)\(y*x) = 0.X;
hence thesis by A1,BCIALG_1:def 7;
end;
theorem Th7: :: Isotonic Property
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds x <= y implies x*z <= y*z & z*x <= z*y
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
assume x <= y;
then (x*z)\y <= (x*z)\x by BCIALG_1:5;
then
A1: ((x*z)\y)\((x*z)\x) = 0.X;
(x*z)\x <= z by Lm2;
then ((x*z)\x)\z = 0.X;
then ((x*z)\y)\z = 0.X by A1,BCIALG_1:3;
then
A2: (x*z)\y <= z;
x*z = z*x & y*z = z*y by Th6;
hence thesis by A2,Lm2;
end;
theorem Th8: :: Unit Element
for X being BCI-Algebra_with_Condition(S) holds for x being
Element of X holds 0.X*x = x & x*0.X = x
proof
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
(x\0.X)\x = (x\x)\0.X by BCIALG_1:7
.= 0.X\0.X by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 5;
then x\0.X <= x;
then x <= 0.X*x by Lm2;
then
A1: x\(0.X*x) = 0.X;
(0.X*x)\0.X <= x by Lm2;
then (0.X*x) <= x by BCIALG_1:2;
then (0.X*x)\x = 0.X;
then 0.X*x = x by A1,BCIALG_1:def 7;
hence thesis by Th6;
end;
theorem Th9: :: Associativity
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds (x*y)*z = x*(y*z)
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
A1: (z*(x*y))\z <= (x*y) by Lm2;
(((x*y)*z)\x)\z = (((x*y)*z)\z)\x by BCIALG_1:7
.= ((z*(x*y))\z)\x by Th6;
then (((x*y)*z)\x)\z <= (x*y)\x by A1,BCIALG_1:5;
then
A2: ((((x*y)*z)\x)\z)\((x*y)\x) = 0.X;
A3: (x*(z*y))\x <= (z*y) by Lm2;
(((z*y)*x)\z)\x = (((z*y)*x)\x)\z by BCIALG_1:7
.= ((x*(z*y))\x)\z by Th6;
then (((z*y)*x)\z)\x <= (z*y)\z by A3,BCIALG_1:5;
then
A4: ((((z*y)*x)\z)\x)\((z*y)\z) = 0.X;
(z*y)\z <= y by Lm2;
then ((z*y)\z)\y = 0.X;
then ((((z*y)*x)\z)\x)\y = 0.X by A4,BCIALG_1:3;
then (((z*y)*x)\z)\x <= y;
then ((z*y)*x)\z <= x*y by Lm2;
then (z*y)*x <= z*(x*y) by Lm2;
then (y*z)*x <= z*(x*y) by Th6;
then x*(y*z) <= z*(x*y) by Th6;
then x*(y*z) <= (x*y)*z by Th6;
then
A5: (x*(y*z))\((x*y)*z) = 0.X;
(x*y)\x <= y by Lm2;
then ((x*y)\x)\y = 0.X;
then ((((x*y)*z)\x)\z)\y = 0.X by A2,BCIALG_1:3;
then (((x*y)*z)\x)\z <= y;
then ((x*y)*z)\x <= z*y by Lm2;
then (x*y)*z <= x*(z*y) by Lm2;
then (x*y)*z <= x*(y*z) by Th6;
then ((x*y)*z)\(x*(y*z)) = 0.X;
hence thesis by A5,BCIALG_1:def 7;
end;
theorem Th10:
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds (x*y)*z = (x*z)*y
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
(x*y)*z = x*(y*z) by Th9
.= (y*z)*x by Th6
.= y*(z*x) by Th9
.= (z*x)*y by Th6;
hence thesis by Th6;
end;
theorem Th11:
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds (x\y)\z = x\(y*z)
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
(x\((x\y)\z))\y = (x\y)\((x\y)\z) by BCIALG_1:7
.= ((x\y)\0.X)\((x\y)\z) by BCIALG_1:2;
then ((x\((x\y)\z))\y)\(z\0.X) = 0.X by BCIALG_1:11;
then (x\((x\y)\z))\y <= z\0.X;
then (x\((x\y)\z))\y <= z by BCIALG_1:2;
then x\((x\y)\z) <= y*z by Lm2;
then (x\((x\y)\z))\(y*z) = 0.X;
then
A1: (x\(y*z))\((x\y)\z) = 0.X by BCIALG_1:7;
(y*z)\y <= z by Lm2;
then ((x\y)\(x\(y*z)))\((y*z)\y) = 0.X & ((y*z)\y)\z = 0.X by BCIALG_1:11;
then ((x\y)\(x\(y*z)))\z = 0.X by BCIALG_1:3;
then ((x\y)\z)\(x\(y*z)) = 0.X by BCIALG_1:7;
hence thesis by A1,BCIALG_1:def 7;
end;
theorem Th12:
for X being BCI-Algebra_with_Condition(S) holds for x,y being
Element of X holds y <= x*(y\x)
proof
let X be BCI-Algebra_with_Condition(S);
let x,y be Element of X;
(y\x)\(y\x) = 0.X by BCIALG_1:def 5;
then y\x <= (y\x);
hence thesis by Lm2;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds (x*z)\(y*z) <= x\y
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
x <= y*(x\y) by Th12;
then x*z <= (y*(x\y))*z by Th7;
then x*z <= (y*z)*(x\y) by Th10;
then (x*z)\(y*z) <= ((y*z)*(x\y))\(y*z) by BCIALG_1:5;
then
A1: ((x*z)\(y*z)) \ (((y*z)*(x\y))\(y*z)) = 0.X;
(((y*z)*(x\y))\(y*z)) <= x\y by Lm2;
then (((y*z)*(x\y))\(y*z)) \ (x\y) = 0.X;
then ((x*z)\(y*z)) \ (x\y) = 0.X by A1,BCIALG_1:3;
hence thesis;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds x\y <= z iff x <= y*z
by Th11;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds x\y <= (x\z)*(z\y)
proof
let X be BCI-Algebra_with_Condition(S);
let x,y,z be Element of X;
((x\y)\(x\z))\(z\y) = 0.X by BCIALG_1:11;
then (x\y)\((x\z)*(z\y)) = 0.X by Th11;
hence thesis;
end;
Lm4: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is
commutative
proof
let X be BCI-Algebra_with_Condition(S);
now
let a,b be Element of X;
thus (the ExternalDiff of X).(a,b)=a*b .= b*a by Th6
.=(the ExternalDiff of X).(b,a);
end;
hence thesis;
end;
Lm5: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is
associative
proof
let X be BCI-Algebra_with_Condition(S);
now
let a,b,c be Element of X;
thus (the ExternalDiff of X).(a,(the ExternalDiff of X).(b,c))=a*(b*c)
.=(a*b)*c by Th9
.=(the ExternalDiff of X).((the ExternalDiff of X).(a,b),c);
end;
hence thesis;
end;
registration
let X be BCI-Algebra_with_Condition(S);
cluster the ExternalDiff of X -> commutative associative;
coherence by Lm4,Lm5;
end;
theorem Th16:
for X being BCI-Algebra_with_Condition(S) holds 0.X
is_a_unity_wrt the ExternalDiff of X
proof
let X be BCI-Algebra_with_Condition(S);
now
let a be Element of X;
thus (the ExternalDiff of X).(0.X,a) = 0.X * a .= a by Th8;
thus (the ExternalDiff of X).(a,0.X) = a * 0.X .= a by Th8;
end;
hence thesis by BINOP_1:3;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds the_unity_wrt the
ExternalDiff of X = 0.X
proof
let X be BCI-Algebra_with_Condition(S);
reconsider e=0.X as Element of X;
e is_a_unity_wrt the ExternalDiff of X by Th16;
hence thesis by BINOP_1:def 8;
end;
theorem Th18:
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff
of X is having_a_unity
proof
let X be BCI-Algebra_with_Condition(S);
reconsider e=0.X as Element of X;
e is_a_unity_wrt the ExternalDiff of X by Th16;
hence thesis by SETWISEO:def 2;
end;
definition
let X be BCI-Algebra_with_Condition(S);
func power X -> Function of [:the carrier of X,NAT:], the carrier of X means
:Def6:
for h being Element of X holds it.(h,0) = 0.X &
for n holds it.(h,n + 1) = it.(h,n) * h;
existence
proof
defpred P[object,object] means
ex g0 being sequence of the carrier of X, h being Element of X
st $1 = h & g0 = $2 & g0.0 = 0.X & for n holds g0.(n + 1) = (g0.n) * h;
A1: for x be object st x in the carrier of X ex y be object st P[x,y]
proof
let x be object;
assume x in the carrier of X;
then reconsider b = x as Element of X;
deffunc F(Nat,Element of X) = $2 * b;
consider g0 being sequence of the carrier of X such that
A2: g0.0 = 0.X and
A3: for n being Nat holds g0.(n + 1) = F(n,g0.n) from NAT_1:sch 12;
reconsider y = g0 as set;
take y;
take g0;
take b;
thus x = b & g0 = y & g0.0 = 0.X by A2;
let n;
thus thesis by A3;
end;
consider f being Function such that
dom f = the carrier of X and
A4: for x be object st x in the carrier of X holds P[x,f.x] from CLASSES1
:sch 1(A1);
defpred P[Element of X,Nat,set] means ex g0 being sequence of
the carrier of X st g0 = f.$1 & $3 = g0.$2;
A5: for a being Element of X, n being Nat ex b being Element of
X st P[a,n,b]
proof
let a be Element of X, n be Nat;
consider g0 being sequence of the carrier of X, h being Element of
X such that
a = h and
A6: g0 = f.a and
g0.0 = 0.X and
for n holds g0.(n + 1) = (g0.n) * h by A4;
take g0.n, g0;
thus thesis by A6;
end;
consider F being Function of [:the carrier of X,NAT:], the carrier of X
such that
A7: for a being Element of X, n being Nat holds P[a,n,F.(a, n)]
from NAT_1:sch 19(A5);
take F;
let h be Element of X;
A8: ex g2 being sequence of the carrier of X, b being Element of X
st h = b & g2 = f.h & g2.0 = 0.X & for n holds g2.(n + 1) = (g2.n) * b by A4;
ex g1 being sequence of the carrier of X st g1 = f.h & F.(h,0) =
g1.0 by A7;
hence F.(h,0) = 0.X by A8;
let n;
A9: ex g2 being sequence of the carrier of X, b being Element of X st
h = b & g2 = f.h & g2.0 = 0.X & for n holds g2.(n + 1) = ( g2.n) * b by A4;
( ex g0 being sequence of the carrier of X st g0 = f.h & F.(h,n)
= g0.n)& ex g1 being sequence of the carrier of X st g1 = f.h & F.(h,n + 1
) = g1.(n + 1) by A7;
hence thesis by A9;
end;
uniqueness
proof
let f,g be Function of [:the carrier of X,NAT:], the carrier of X;
assume that
A10: for h being Element of X holds f.(h,0) = 0.X & for n holds f.(h,n
+ 1) = (f.(h,n)) * h and
A11: for h being Element of X holds g.(h,0) = 0.X & for n holds g.(h,n
+ 1) = (g.(h,n)) * h;
now
let h be Element of X, n be Nat;
defpred P[Nat] means f.[h,$1] = g.[h,$1];
A12: now
let n;
assume
A13: P[n];
A14: g.[h,n] = g.(h,n);
f.[h,n + 1] = f.(h,n + 1) .= (f.(h,n)) * h by A10
.= g.(h,n + 1) by A11,A13,A14
.= g.[h,n + 1];
hence P[n+1];
end;
f.[h,0] = f.(h,0) .= 0.X by A10
.= g.(h,0) by A11
.= g.[h,0];
then
A15: P[0];
for n holds P[n] from NAT_1:sch 2(A15,A12);
hence f.(h,n) = g.(h,n);
end;
hence thesis;
end;
end;
definition
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
let n be Nat;
func x |^ n -> Element of X equals
power(X).(x,n);
correctness;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x being Element of
X holds x |^ 0 = 0.X by Def6;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x being Element of
X holds x |^ (n + 1) = (x|^n) * x by Def6;
theorem Th21:
for X being BCI-Algebra_with_Condition(S) holds for x being
Element of X holds x |^ 1 = x
proof
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
thus x|^1 = x|^(0 + 1) .=(x|^0) * x by Def6
.=0.X * x by Def6
.= x by Th8;
end;
theorem Th22:
for X being BCI-Algebra_with_Condition(S) holds for x being
Element of X holds x |^ 2 = x * x
proof
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
thus x |^ 2 = x |^ (1 + 1) .=(x |^ 1) * x by Def6
.= x*x by Th21;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x being Element of
X holds x |^ 3 = x * x * x
proof
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
thus x|^3 = x|^(2 + 1) .=(x|^2) * x by Def6
.= x * x * x by Th22;
end;
theorem Th24:
for X being BCI-Algebra_with_Condition(S) holds (0.X) |^ 2 = 0.X
proof
let X be BCI-Algebra_with_Condition(S);
0.X*0.X = (0.X*0.X) \ 0.X by BCIALG_1:2;
then 0.X*0.X <= 0.X by Lm2;
then
A1: (0.X*0.X) \ 0.X = 0.X;
0.X <= 0.X*(0.X\0.X) by Th12;
then 0.X <= 0.X*0.X by BCIALG_1:def 5;
then 0.X \ (0.X*0.X) = 0.X;
then 0.X*0.X = 0.X by A1,BCIALG_1:def 7;
hence thesis by Th22;
end;
Lm6: for X being BCI-Algebra_with_Condition(S) holds (0.X) |^ (n+1) = 0.X
proof
let X be BCI-Algebra_with_Condition(S);
defpred P[set] means for m holds m=$1 & m<= n implies (0.X) |^ (m+1) = 0.X;
now
let k;
assume
A1: for m st m=k & m<= n holds (0.X) |^ (m+1) = 0.X;
let m;
assume that
A2: m=k+1 and
A3: m<=n;
k<=n by A2,A3,NAT_1:13;
then
A4: (0.X) |^ (k+1) = 0.X by A1;
A5: (0.X)|^2 = 0.X by Th24;
(0.X) |^ (m+1) = ((0.X) |^ (k+1)) * 0.X by A2,Def6;
hence (0.X) |^ (m+1) = 0.X by A5,A4,Th22;
end;
then
A6: for k st P[k] holds P[k+1];
A7: P[0] by Th21;
for n holds P[n] from NAT_1:sch 2(A7,A6);
hence thesis;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds (0.X)|^n = 0.X
proof
let X be BCI-Algebra_with_Condition(S);
defpred P[set] means for m holds m=$1 & m<= n implies (0.X)|^m = 0.X;
A1: for k st P[k] holds P[k+1] by Lm6;
A2: P[0] by Def6;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,a being Element
of X holds ((x\a)\a)\a = x\(a|^3)
proof
let X be BCI-Algebra_with_Condition(S);
let x,a be Element of X;
(x\a)\a = x\(a*a) by Th11;
then ((x\a)\a)\a = x\((a*a)*a) by Th11
.= x\((a|^2)*a) by Th22
.= x\(a|^(2+1)) by Def6;
hence thesis;
end;
Lm7: for X being BCI-Algebra_with_Condition(S) holds for x,a being Element of
X holds (x,a) to_power 0 = x\(a|^0)
proof
let X be BCI-Algebra_with_Condition(S);
let x,a be Element of X;
x\(a|^0) = x\0.X by Def6
.= x by BCIALG_1:2;
hence thesis by BCIALG_2:1;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,a being Element
of X holds (x,a) to_power n = x\(a|^n)
proof
let X be BCI-Algebra_with_Condition(S);
let x,a be Element of X;
defpred P[set] means for m holds m=$1 & m<= n implies (x,a) to_power m = x\(
a|^m);
now
let k;
assume
A1: for m st m=k & m<= n holds (x,a) to_power m = x\(a|^m);
let m;
assume that
A2: m=k+1 and
A3: m<=n;
A4: (x,a) to_power m = (x,a) to_power k \ a & k<=n by A2,A3,BCIALG_2:4,NAT_1:13
;
x\(a|^m) = x\((a|^k)*a) by A2,Def6
.= (x\(a|^k))\a by Th11;
hence (x,a) to_power m = x\(a|^m) by A1,A4;
end;
then
A5: for k st P[k] holds P[k+1];
A6: P[0] by Lm7;
for n holds P[n] from NAT_1:sch 2(A6,A5);
hence thesis;
end;
definition
let X be non empty BCIStr_1;
let F be FinSequence of the carrier of X;
func Product_S F -> Element of X equals
(the ExternalDiff of X) "**" F;
correctness;
end;
theorem
(the ExternalDiff of X) "**" <* d *> = d
proof
A1: len<* d *> = 1 by FINSEQ_1:39;
then
ex f st f.1 = <* d *>.1 & (for n st 0 <> n & n < len<* d *> holds f.(n +
1) = (the ExternalDiff of X).(f.n,<* d *>.(n + 1))) & (the ExternalDiff of X)
"**" <* d *> = f.len<* d *> by FINSOP_1:def 1;
hence thesis by A1;
end;
theorem
for X being BCI-Algebra_with_Condition(S), F1,F2 being FinSequence of
the carrier of X holds Product_S(F1 ^ F2) = Product_S(F1) * Product_S(F2) by
Th18,FINSOP_1:5;
theorem
for X being BCI-Algebra_with_Condition(S), F being FinSequence of the
carrier of X, a being Element of X holds Product_S(F ^ <* a *>) = Product_S(F)
* a by Th18,FINSOP_1:4;
theorem
for X being BCI-Algebra_with_Condition(S), F being FinSequence of the
carrier of X, a being Element of X holds Product_S(<* a *> ^ F) = a * Product_S
(F) by Th18,FINSOP_1:6;
theorem Th32:
for X being BCI-Algebra_with_Condition(S) holds for a1,a2 being
Element of X holds Product_S<*a1,a2*> = a1 * a2
proof
let X be BCI-Algebra_with_Condition(S);
let a1,a2 be Element of X;
thus Product_S<*a1,a2*> = Product_S<*a1*> * a2 by Th18,FINSOP_1:4
.= a1 * a2 by FINSOP_1:11;
end;
theorem Th33:
for X being BCI-Algebra_with_Condition(S) holds for a1,a2,a3
being Element of X holds Product_S<*a1,a2,a3*> = a1 * a2 * a3
proof
let X be BCI-Algebra_with_Condition(S);
let a1,a2,a3 be Element of X;
thus Product_S<*a1,a2,a3*> = Product_S<*a1,a2*> * a3 by Th18,FINSOP_1:4
.= a1 * a2 * a3 by FINSOP_1:12;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,a1,a2 being
Element of X holds (x\a1)\a2 = x\Product_S<*a1,a2*>
proof
let X be BCI-Algebra_with_Condition(S);
let x,a1,a2 be Element of X;
(x\a1)\a2 = x\(a1 * a2) by Th11;
hence thesis by Th32;
end;
theorem
for X being BCI-Algebra_with_Condition(S) holds for x,a1,a2,a3 being
Element of X holds ((x\a1)\a2)\a3 = x\Product_S<*a1,a2,a3*>
proof
let X be BCI-Algebra_with_Condition(S);
let x,a1,a2,a3 be Element of X;
((x\a1)\a2)\a3 = (x\(a1 * a2))\a3 by Th11
.= x\(a1 * a2 * a3) by Th11;
hence thesis by Th33;
end;
theorem
for X being BCI-Algebra_with_Condition(S), a,b being Element of
AtomSet(X) holds for ma being Element of X st (for x being Element of BranchV(a
) holds x <= ma) holds ex mb being Element of X st for y being Element of
BranchV(b) holds y <= mb
proof
let X be BCI-Algebra_with_Condition(S);
let a,b be Element of AtomSet(X);
let ma be Element of X;
assume
A1: for x being Element of BranchV(a) holds x <= ma;
ex mb being Element of X st for y being Element of BranchV(b) holds y <= mb
proof
set mb = (b * (0.X\a)) * ma;
for y being Element of BranchV(b) holds y <= mb
proof
a\a = 0.X by BCIALG_1:def 5;
then a <= a;
then a in {yy2 where yy2 is Element of X:a <= yy2};
then
A2: a is Element of BranchV(a);
let y be Element of BranchV(b);
0.X in AtomSet(X);
then consider x0 being Element of AtomSet(X) such that
A3: x0 = 0.X;
y in {yy where yy is Element of X:b<=yy};
then ex yy being Element of X st y=yy & b<= yy;
then b\b <= y\b by BCIALG_1:5;
then y\b in {yy1 where yy1 is Element of X:b\b <= yy1};
then
A4: y\b is Element of BranchV(b\b);
A5: (b\b)\(x0\a) = x0\(x0\a) by A3,BCIALG_1:def 5
.= a by BCIALG_1:24;
x0\x0 = 0.X by BCIALG_1:def 5;
then x0 <= x0;
then x0 in {yy2 where yy2 is Element of X:x0 <= yy2};
then x0 is Element of BranchV(x0);
then x0\a is Element of BranchV(x0\a) by A2,BCIALG_1:39;
then (y\b)\(x0\a) is Element of BranchV(a) by A4,A5,BCIALG_1:39;
then
A6: (y\b)\(x0\a) <= ma by A1;
y\mb = (y\(b * (0.X\a))) \ ma by Th11
.= ((y\b)\(x0\a))\ma by A3,Th11
.= 0.X by A6;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
:: Commutative BCK-Algebras with Condition(S)
registration
cluster strict being_BCK-5 for BCI-Algebra_with_Condition(S);
existence by Lm1;
end;
definition
mode BCK-Algebra_with_Condition(S) is being_BCK-5
BCI-Algebra_with_Condition(S);
end;
theorem Th37:
for X being BCK-Algebra_with_Condition(S) holds for x,y being
Element of X holds x <= x*y & y <= x*y
proof
let X be BCK-Algebra_with_Condition(S);
for x,y being Element of X holds x <= x*y & y <= x*y
proof
let x,y be Element of X;
A1: (x\x)\y = y` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
A2: (y\y)\x = x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
A3: (x\x)\y = x\(x*y) by Th11;
(y\y)\x = y\(y*x) by Th11
.= y\(x*y) by Th6;
hence thesis by A3,A1,A2;
end;
hence thesis;
end;
theorem
for X being BCK-Algebra_with_Condition(S) holds for x,y,z being
Element of X holds ((x*y)\(y*z))\(z*x) = 0.X
proof
let X be BCK-Algebra_with_Condition(S);
for x,y,z being Element of X holds ((x*y)\(y*z))\(z*x) = 0.X
proof
let x,y,z be Element of X;
(y*x) \ y <= x by Lm2;
then
A1: ((y*x) \ y) \ z <= x\z by BCIALG_1:5;
(x*y) = y*x by Th6;
then (x*y)\(y*z) <= x\z by A1,Th11;
then
A2: ((x*y)\(y*z))\(z*x) <= (x\z)\(z*x) by BCIALG_1:5;
(x\z)\(z*x) = ((x\z)\z)\x by Th11
.= ((x\z)\x)\z by BCIALG_1:7
.= ((x\x)\z)\z by BCIALG_1:7
.= z`\z by BCIALG_1:def 5
.= z` by BCIALG_1:def 8
.= 0.X by BCIALG_1:def 8;
then (((x*y)\(y*z))\(z*x)) \ 0.X = 0.X by A2;
hence thesis by BCIALG_1:2;
end;
hence thesis;
end;
theorem
for X being BCK-Algebra_with_Condition(S) holds for x,y being Element
of X holds (x\y)*(y\x) <= x*y
proof
let X be BCK-Algebra_with_Condition(S);
for x,y being Element of X holds (x\y)*(y\x) <= x*y
proof
let x,y be Element of X;
((x\y)*(y\x))\(x\y) <= (y\x) by Lm2;
then
A1: (((x\y)*(y\x))\(x\y))\y <= (y\x)\y by BCIALG_1:5;
(y\x)\y = (y\y)\x by BCIALG_1:7
.= x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
then ((x\y)*(y\x))\((x\y)*y) <= 0.X by A1,Th11;
then ((x\y)*(y\x))\((x\y)*y) \ 0.X = 0.X;
then
A2: ((x\y)*(y\x))\((x\y)*y) = 0.X by BCIALG_1:2;
(y*(x\y))\y <= x\y by Lm2;
then
A3: ((y*(x\y))\y)\x <= (x\y)\x by BCIALG_1:5;
(x\y)\x = (x\x)\y by BCIALG_1:7
.= y` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
then (y*(x\y))\(y*x) <= 0.X by A3,Th11;
then ((y*(x\y))\(y*x)) \ 0.X = 0.X;
then
A4: (y*(x\y))\(y*x) = 0.X by BCIALG_1:2;
(x\y)*y = y*(x\y) by Th6;
then ((x\y)*(y\x))\(y*x) = 0.X by A2,A4,BCIALG_1:3;
then (x\y)*(y\x) <= (y*x);
hence thesis by Th6;
end;
hence thesis;
end;
theorem
for X being BCK-Algebra_with_Condition(S) holds for x being Element of
X holds (x\0.X)*(0.X\x) = x
proof
let X be BCK-Algebra_with_Condition(S);
for x being Element of X holds (x\0.X)*(0.X\x) = x
proof
let x be Element of X;
A1: (0.X\x) = x` .= 0.X by BCIALG_1:def 8;
(x\0.X) = x by BCIALG_1:2;
hence thesis by A1,Th8;
end;
hence thesis;
end;
definition
let IT be BCK-Algebra_with_Condition(S);
attr IT is commutative means
:Def9:
for x,y being Element of IT holds x\(x\y ) = y\(y\x);
end;
registration
cluster commutative for BCK-Algebra_with_Condition(S);
existence
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);
IT is commutative
by STRUCT_0:def 10;
hence thesis;
end;
end;
theorem
for X being non empty BCIStr_1 holds (X is commutative
BCK-Algebra_with_Condition(S) iff for x,y,z being Element of X holds x\(0.X\y)
= x & (x\z)\(x\y) = (y\z)\(y\x) & (x\y)\z = x\(y*z) )
proof
let X be non empty BCIStr_1;
thus X is commutative BCK-Algebra_with_Condition(S) implies for x,y,z being
Element of X holds x\(0.X\y) = x & (x\z)\(x\y) = (y\z)\(y\x) & (x\y)\z = x\(y*z
)
proof
assume
A1: X is commutative BCK-Algebra_with_Condition(S);
let x,y,z be Element of X;
(x\(x\y))\z = (y\(y\x))\z by A1,Def9;
then
A2: (x\z)\(x\y) = (y\(y\x))\z by A1,BCIALG_1:7
.= (y\z)\(y\x) by A1,BCIALG_1:7;
0.X\y = y` .= 0.X by A1,BCIALG_1:def 8;
hence thesis by A1,A2,Th11,BCIALG_1:2;
end;
thus (for x,y,z being Element of X holds x\(0.X\y) = x & (x\z)\(x\y) = (y\z)
\(y\x) & (x\y)\z = x\(y*z) ) implies X is commutative
BCK-Algebra_with_Condition(S)
proof
assume
A3: for x,y,z being Element of X holds x\(0.X\y) = x & (x\z)\(x\y) = (
y\z)\(y\x) & (x\y)\z = x\(y*z);
A4: for x,y being Element of X holds x\0.X = x
proof
let x,y be Element of X;
0.X\(0.X\0.X) = 0.X by A3;
hence thesis by A3;
end;
A5: 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 x\y=0.X & y\x=0.X;
then (x\0.X)\0.X = (y\0.X)\0.X by A3;
then (x\0.X) = (y\0.X)\0.X by A4
.= (y\0.X) by A4;
hence x = (y\0.X) by A4
.= y by A4;
end;
A6: for x being Element of X holds x\x = 0.X
proof
let x be Element of X;
x = (x\0.X) by A4;
then x\x = (0.X\0.X)\(0.X\x) by A3
.= 0.X\(0.X\x) by A4
.= 0.X by A3;
hence thesis;
end;
A7: for x being Element of X holds 0.X\x = 0.X
proof
let x be Element of X;
0.X = (0.X\x)\(0.X\x) by A6
.= 0.X\x by A3;
hence thesis;
end;
A8: for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X
proof
let x,y,z be Element of X;
((x\y)\(x\z))\(z\y) = ((z\y)\(z\x))\(z\y) by A3
.= ((z\y)\(z\x))\((z\y)\0.X) by A4
.= (0.X\(z\x))\(0.X\(z\y)) by A3
.= 0.X\(0.X\(z\y)) by A7
.= 0.X by A7;
hence thesis;
end;
A9: 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
A10: x\y=0.X and
A11: y\z=0.X;
((x\z)\(x\y))\(y\z)=0.X by A8;
then (x\z)\(x\y)=0.X by A4,A11;
hence thesis by A4,A10;
end;
A12: 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 A8;
then (((x\y)\z)\((x\y)\(x\(x\z))))\((x\(x\z))\(z\0.X))=0.X by A4;
then
(((x\y)\z)\((x\y)\(x\(x\z))))\(((x\0.X)\(x\z))\(z\0.X))=0.X by A4;
then (((x\y)\z)\((x\y)\(x\(x\z))))\0.X=0.X by A8;
then
A13: ((x\y)\z)\((x\y)\(x\(x\z)))=0.X by A4;
((x\y)\(x\(x\z)))\((x\z)\y) = 0.X by A8;
hence thesis by A9,A13;
end;
A14: for x,y being Element of X holds x\(x\y) = y\(y\x)
proof
let x,y be Element of X;
x\(x\y) = (x\(0.X\y))\(x\y) by A3
.= (y\(0.X\y))\(y\x) by A3
.= y\(y\x) by A3;
hence thesis;
end;
A15: 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
A16: x\y=0.X;
((z\y)\(z\x))\(x\y)=0.X & ((x\z)\(x\y))\(y\z)=0.X by A8;
hence thesis by A4,A16;
end;
A17: 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 A8;
then ((x\y)\(z\y))\((x\y)\((x\y)\(x\z))) = 0.X by A15;
then (((x\y)\(z\y))\(x\z))\(((x\y)\((x\y)\(x\z)))\(x\z)) = 0.X by A15;
then (((x\y)\(z\y))\(x\z))\((((x\y)\0.X)\((x\y)\(x\z)))\(x\z)) = 0.X by
A4;
then (((x\y)\(z\y))\(x\z))\((((x\y)\0.X)\((x\y)\(x\z)))\((x\z)\0.X)) =
0.X by A4;
then (((x\y)\(z\y))\(x\z))\ 0.X = 0.X by A8;
hence thesis by A4;
end;
for x being Element of X holds x`=0.X by A7;
hence thesis by A3,A6,A5,A14,A12,A17,Def2,Def9,BCIALG_1:def 3,def 4,def 5
,def 7,def 8;
end;
end;
theorem
for X being commutative BCK-Algebra_with_Condition(S), a being Element
of X st a is greatest holds for x,y being Element of X holds x*y = a\((a\x)\y)
proof
let X be commutative BCK-Algebra_with_Condition(S);
let a be Element of X;
assume
A1: a is greatest;
for x,y being Element of X holds x*y = a\((a\x)\y)
proof
let x,y be Element of X;
A2: (x*y)<=a by A1,BCIALG_2:def 5;
a\((a\x)\y) = a\(a\(x*y)) by Th11
.= (x*y)\((x*y)\a) by Def9
.= (x*y)\0.X by A2;
hence thesis by BCIALG_1:2;
end;
hence thesis;
end;
definition
let X be BCI-algebra;
let a be Element of X;
func Initial_section(a) -> non empty Subset of X equals
{t where t is
Element of X: t <= a};
coherence
proof
set Y={t where t is Element of X: t <= a};
A1: now
let y1 be object;
assume y1 in Y;
then ex x1 being Element of X st y1=x1 & x1 <= a;
hence y1 in the carrier of X;
end;
a\a = 0.X by BCIALG_1:def 5;
then a <= a;
then a in Y;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem
for X being commutative BCK-Algebra_with_Condition(S), a,b,c being
Element of X st Condition_S(a,b) c= Initial_section(c) holds for x being
Element of Condition_S(a,b) holds x <= c\((c\a)\b)
proof
let X be commutative BCK-Algebra_with_Condition(S);
let a,b,c be Element of X;
assume
A1: Condition_S(a,b) c= Initial_section(c);
for x being Element of Condition_S(a,b) holds x <= c\((c\a)\b)
proof
set u = c\((c\a)\b);
let x be Element of Condition_S(a,b);
A2: (c\(c\x)) \ x = (c\x)\(c\x) by BCIALG_1:7
.= 0.X by BCIALG_1:def 5;
x in {t2 where t2 is Element of X: t2 <= c} by A1,TARSKI:def 3;
then consider x2 being Element of X such that
A3: x=x2 and
A4: x2 <= c;
A5: x \ (c\(c\x)) = x\(x\(x\c)) by Def9
.= x2\c by A3,BCIALG_1:8
.= 0.X by A4;
then
A6: ((c\(c\x)) \ (c\((c\a)\b))) \ (((c\a)\b)\(c\x)) = 0.X & x\u = (c\(c\x
)) \ (c \((c\a)\b)) by A2,BCIALG_1:1,def 7;
x in {t1 where t1 is Element of X: t1\a <= b};
then
A7: ex x1 being Element of X st x=x1 & x1\a <= b;
(((c\a)\b)\(c\x)) = ((c\a)\(c\x))\b by BCIALG_1:7
.= ((c\(c\x))\a)\b by BCIALG_1:7
.= (x\a)\b by A5,A2,BCIALG_1:def 7
.= 0.X by A7;
then x\u = 0.X by A6,BCIALG_1:2;
hence thesis;
end;
hence thesis;
end;
:: Positive-Implicative BCK-Algebras with Condition(S)
definition
let IT be BCK-Algebra_with_Condition(S);
attr IT is positive-implicative means
for x,y being Element of IT holds (x\y)\y = x\y;
end;
registration
cluster positive-implicative for BCK-Algebra_with_Condition(S);
existence
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);
IT is positive-implicative
by STRUCT_0:def 10;
hence thesis;
end;
end;
theorem Th44:
for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x being Element of X holds x*x = x )
proof
let X be BCK-Algebra_with_Condition(S);
A1: X is positive-implicative implies for x being Element of X holds x*x = x
proof
assume
A2: X is positive-implicative;
let x be Element of X;
A3: (x*x)\x <= x by Lm2;
(x*x)\x = ((x*x)\x)\x by A2;
then (x*x)\x <= x\x by A3,BCIALG_1:5;
then x\x = 0.X & ((x*x)\x) \ (x\x) = 0.X by BCIALG_1:def 5;
then
A4: (x*x)\x = 0.X by BCIALG_1:2;
x\(x*x) = (x\x)\x by Th11
.= x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
hence thesis by A4,BCIALG_1:def 7;
end;
(for x being Element of X holds x*x = x) implies X is positive-implicative
proof
assume
A5: for x being Element of X holds x*x = x;
for x,y being Element of X holds (x\y)\y = x\y
proof
let x,y be Element of X;
x\(y*y) = x\y by A5;
hence thesis by Th11;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th45:
for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x,y being Element of X holds (x <= y implies x*y =
y) )
proof
let X be BCK-Algebra_with_Condition(S);
A1: X is positive-implicative implies for x,y being Element of X holds (x <=
y implies x*y = y)
proof
assume
A2: X is positive-implicative;
let x,y be Element of X;
A3: (y*x)\y <= x by Lm2;
(x*y)\y = (y*x)\y by Th6
.= ((y*x)\y)\y by A2;
then (x*y)\y <= x\y by A3,BCIALG_1:5;
then
A4: ((x*y)\y) \ (x\y) = 0.X;
A5: y\(x*y) = y\(y*x) by Th6
.= (y\y)\x by Th11
.= x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
assume x <= y;
then (x\y) = 0.X;
then (x*y)\y = 0.X by A4,BCIALG_1:2;
hence thesis by A5,BCIALG_1:def 7;
end;
(for x,y being Element of X holds (x <= y implies x*y = y)) implies X
is positive-implicative
proof
assume
A6: for x,y being Element of X holds (x <= y implies x*y = y);
for x being Element of X holds x*x = x
proof
let x be Element of X;
x\x = 0.X by BCIALG_1:def 5;
then x <= x;
hence thesis by A6;
end;
hence thesis by Th44;
end;
hence thesis by A1;
end;
theorem Th46:
for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x,y,z being Element of X holds (x*y)\z = (x\z)*(y\
z) )
proof
let X be BCK-Algebra_with_Condition(S);
A1: X is positive-implicative implies for x,y,z being Element of X holds (x*
y)\z = (x\z)*(y\z)
proof
assume
A2: X is positive-implicative;
let x,y,z be Element of X;
(((x*y)\z)\(x\z))\((x*y)\x) = 0.X by BCIALG_1:def 3;
then (((x*y)\z)\(x\z)) <= ((x*y)\x);
then (((x*y)\z)\(x\z))\z <= ((x*y)\x)\z by BCIALG_1:5;
then
A3: ((((x*y)\z)\(x\z))\z) \ (((x*y)\x)\z) = 0.X;
(x*y)\x <= y by Lm2;
then ((x*y)\x)\z <= y\z by BCIALG_1:5;
then
A4: (((x*y)\x)\z)\(y\z) = 0.X;
(x*y)\z = (x*y)\(z*z) by A2,Th44
.= ((x*y)\z)\z by Th11;
then ((x*y)\z) \ (x\z) = (((x*y)\z)\(x\z))\z by BCIALG_1:7;
then (((x*y)\z)\(x\z))\(y\z) = 0.X by A3,A4,BCIALG_1:3;
then
A5: ((x*y)\z)\((x\z)*(y\z)) = 0.X by Th11;
y <= x*y by Th37;
then y\z <= (x*y)\z by BCIALG_1:5;
then ((x*y)\z)*(y\z) <= ((x*y)\z)*((x*y)\z) by Th7;
then
A6: (((x*y)\z)*(y\z)) \ (((x*y)\z)*((x*y)\z)) = 0.X;
x <= x*y by Th37;
then x\z <= (x*y)\z by BCIALG_1:5;
then (x\z)*(y\z) <= ((x*y)\z)*(y\z) by Th7;
then ((x\z)*(y\z)) \ (((x*y)\z)*(y\z)) = 0.X;
then ((x\z)*(y\z)) \ (((x*y)\z)*((x*y)\z)) = 0.X by A6,BCIALG_1:3;
then ((x\z)*(y\z))\((x*y)\z) = 0.X by A2,Th44;
hence thesis by A5,BCIALG_1:def 7;
end;
(for x,y,z being Element of X holds (x*y)\z = (x\z)*(y\z)) implies X is
positive-implicative
proof
assume
A7: for x,y,z being Element of X holds (x*y)\z = (x\z)*(y\z);
for x being Element of X holds x*x = x
proof
let x be Element of X;
(x*x)\x = (x\x)*(x\x) by A7;
then (x*x)\x = 0.X*(x\x) by BCIALG_1:def 5;
then (x*x)\x = 0.X*0.X by BCIALG_1:def 5;
then
A8: (x*x)\x = 0.X by Th8;
x\(x*x) = (x\x)\x by Th11
.= x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
hence thesis by A8,BCIALG_1:def 7;
end;
hence thesis by Th44;
end;
hence thesis by A1;
end;
theorem Th47:
for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x,y being Element of X holds x*y = x*(y\x) )
proof
let X be BCK-Algebra_with_Condition(S);
A1: X is positive-implicative implies for x,y being Element of X holds x*y =
x*(y\x)
proof
assume
A2: X is positive-implicative;
let x,y be Element of X;
(y\x)\y = (y\y)\x by BCIALG_1:7
.= x` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
then y\x <= y;
then x*(y\x) <= x*y by Th7;
then
A3: (x*(y\x))\(x*y) = 0.X;
(x*y)\x = (x\x)*(y\x) by A2,Th46
.= 0.X*(y\x) by BCIALG_1:def 5
.= y\x by Th8;
then ((x*y)\x)\(y\x) = 0.X by BCIALG_1:def 5;
then (x*y)\(x*(y\x)) = 0.X by Th11;
hence thesis by A3,BCIALG_1:def 7;
end;
(for x,y being Element of X holds x*y = x*(y\x)) implies X is
positive-implicative
proof
assume
A4: for x,y being Element of X holds x*y = x*(y\x);
for x,y being Element of X holds (x\y)\y = x\y
proof
let x,y be Element of X;
(y*y) = y*(y\y) by A4
.= y*0.X by BCIALG_1:def 5
.= y by Th8;
hence thesis by Th11;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th48:
for X being positive-implicative BCK-Algebra_with_Condition(S)
holds for x,y being Element of X holds x = (x\y)*(x\(x\y))
proof
let X be positive-implicative BCK-Algebra_with_Condition(S);
for x,y being Element of X holds x = (x\y)*(x\(x\y))
proof
let x,y be Element of X;
(x\y)\x = (x\x)\y by BCIALG_1:7
.= y` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
then x\y <= x;
then x = (x\y)*x by Th45;
hence thesis by Th47;
end;
hence thesis;
end;
definition
let IT be non empty BCIStr_1;
attr IT is being_SB-1 means
:Def12:
for x being Element of IT holds x * x = x;
attr IT is being_SB-2 means
:Def13:
for x,y being Element of IT holds x * y = y * x;
attr IT is being_SB-4 means
:Def14:
for x,y being Element of IT holds (x\y) * y = x * y;
end;
Lm8: BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE
is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S
by STRUCT_0:def 10;
registration
cluster BCI_S-EXAMPLE -> being_SB-1 being_SB-2 being_SB-4 being_I
with_condition_S;
coherence by Lm8;
end;
registration
cluster strict being_SB-1 being_SB-2 being_SB-4 being_I with_condition_S for
non empty BCIStr_1;
existence by Lm8;
end;
definition
mode semi-Brouwerian-algebra is being_SB-1 being_SB-2 being_SB-4 being_I
with_condition_S non empty BCIStr_1;
end;
theorem
for X being non empty BCIStr_1 holds (X is positive-implicative
BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra)
proof
let X be non empty BCIStr_1;
A1: X is semi-Brouwerian-algebra implies X is positive-implicative
BCK-Algebra_with_Condition(S)
proof
assume
A2: X is semi-Brouwerian-algebra;
A3: 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
A4: x\y=0.X and
A5: y\x=0.X;
A6: x = x*x by A2,Def12
.= (x\x)*x by A2,Def14
.= 0.X * x by A2,BCIALG_1:def 5
.= y*x by A2,A5,Def14;
y = y*y by A2,Def12
.= (y\y)*y by A2,Def14
.= y*(y\y) by A2,Def13
.= y*0.X by A2,BCIALG_1:def 5
.= (x\y)*y by A2,A4,Def13
.= x*y by A2,Def14;
hence thesis by A2,A6,Def13;
end;
A7: 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\(y*z) by A2,Def2
.= x\(z*y) by A2,Def13;
hence thesis by A2,Def2;
end;
A8: 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\z)\y) = ((x\y)\z)\((x\y)\z) by A7;
hence thesis by A2,BCIALG_1:def 5;
end;
A9: for x,y being Element of X holds x*y = x*(y\x)
proof
let x,y be Element of X;
x*(y\x) = (y\x)*x by A2,Def13
.= y*x by A2,Def14;
hence thesis by A2,Def13;
end;
A10: for x being Element of X holds x`=0.X
proof
let x be Element of X;
0.X \ x = (x\x)\x by A2,BCIALG_1:def 5
.= x\(x*x) by A2,Def2
.= x\x by A2,Def12
.= 0.X by A2,BCIALG_1:def 5;
hence thesis;
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)\(z\y))\(x\z) = (x\(y*(z\y)))\(x\z) by A2,Def2
.= (x\((z\y)*y))\(x\z) by A2,Def13
.= (x\(z*y))\(x\z) by A2,Def14
.= ((x\z)\y)\(x\z) by A2,Def2
.= ((x\z)\(x\z))\y by A7
.= y` by A2,BCIALG_1:def 5;
hence thesis by A10;
end;
hence thesis by A2,A10,A3,A8,A9,Th47,BCIALG_1:def 3,def 4,def 7,def 8;
end;
X is positive-implicative BCK-Algebra_with_Condition(S) implies X is
semi-Brouwerian-algebra
proof
assume
A11: X is positive-implicative BCK-Algebra_with_Condition(S);
A12: for x,y being Element of X holds (x\y) * y = x * y
proof
let x,y be Element of X;
y*x = y*(x\y) by A11,Th47;
then x*y = y*(x\y) by A11,Th6;
hence thesis by A11,Th6;
end;
( for x being Element of X holds x*x = x)& for x,y being Element of X
holds x * y = y * x by A11,Th6,Th44;
hence thesis by A11,A12,Def12,Def13,Def14;
end;
hence thesis by A1;
end;
:: Implicative BCK-Algebras with Condition(S)
definition
let IT be BCK-Algebra_with_Condition(S);
attr IT is implicative means
for x,y being Element of IT holds x\(y\ x) = x;
end;
registration
cluster implicative for BCK-Algebra_with_Condition(S);
existence
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);
IT is implicative
by STRUCT_0:def 10;
hence thesis;
end;
end;
theorem Th50:
for X being BCK-Algebra_with_Condition(S) holds (X is
implicative iff X is commutative & X is positive-implicative )
proof
let X be BCK-Algebra_with_Condition(S);
thus X is implicative implies X is commutative & X is positive-implicative
proof
assume
A1: X is implicative;
A2: for x,y being Element of X holds x\(x\y) <= y\(y\x)
proof
let x,y be Element of X;
(x\(x\y))\y = (x\y)\(x\y) by BCIALG_1:7
.= 0.X by BCIALG_1:def 5;
then (x\(x\y)) <= y;
then (x\(x\y))\(y\x) <= y\(y\x) by BCIALG_1:5;
then (x\(y\x))\(x\y) <= y\(y\x) by BCIALG_1:7;
hence thesis by A1;
end;
A3: for x,y being Element of X holds x\(x\y) = y\(y\x)
proof
let x,y be Element of X;
y\(y\x) <= x\(x\y) by A2;
then
A4: (y\(y\x))\(x\(x\y)) = 0.X;
x\(x\y) <= y\(y\x) by A2;
then (x\(x\y))\(y\(y\x)) = 0.X;
hence thesis by A4,BCIALG_1:def 7;
end;
for x,y being Element of X holds x\y = (x\y)\y
proof
let x,y be Element of X;
(x\y)\(y\(x\y))=(x\y) by A1;
hence thesis by A1;
end;
hence thesis by A3;
end;
assume that
A5: X is commutative and
A6: X is positive-implicative;
for x,y being Element of X holds x\(y\x)=x
proof
let x,y be Element of X;
x\(x\(x\(y\x))) = x\(y\x) by BCIALG_1:8;
then
A7: x\(y\x) = x\((y\x)\((y\x)\x)) by A5;
(y\x)\((y\x)\x) = (y\x)\(y\x) by A6
.= 0.X by BCIALG_1:def 5;
hence thesis by A7,BCIALG_1:2;
end;
hence thesis;
end;
theorem
for X being BCK-Algebra_with_Condition(S) holds ( X is implicative iff
for x,y,z being Element of X holds x\(y\z) = ((x\y)\z)*(z\(z\x)) )
proof
let X be BCK-Algebra_with_Condition(S);
A1: X is implicative implies for x,y,z being Element of X holds x\(y\z) = ((
x\y)\z)*(z\(z\x))
proof
assume
A2: X is implicative;
then
A3: X is positive-implicative by Th50;
let x,y,z be Element of X;
A4: X is commutative by A2,Th50;
x = (x\z)*(x\(x\z)) by A3,Th48;
then
A5: x\(y\z) = ((x\z)*(z\(z\x)))\(y\z) by A4;
(y\z)\y = (y\y)\z by BCIALG_1:7
.= z` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 8;
then y\z <= y;
then (x\z)\y <= (x\z)\(y\z) by BCIALG_1:5;
then ((x\z)\y)\((x\z)\(y\z)) = 0.X;
then
A6: ((x\y)\z)\((x\z)\(y\z)) = 0.X by BCIALG_1:7;
((x\z)\(y\z))\((x\y)\z) = (((x\z)\z)\(y\z))\((x\y)\z) by A3
.= (((x\z)\z)\(y\z))\((x\z)\y) by BCIALG_1:7
.= 0.X by BCIALG_1:def 3;
then
A7: (x\y)\z=(x\z)\(y\z) by A6,BCIALG_1:def 7;
(z\(z\x))\(y\z) = (z\(y\z))\(z\x) by BCIALG_1:7
.= z\(z\x) by A2;
hence thesis by A3,A5,A7,Th46;
end;
(for x,y,z being Element of X holds x\(y\z) = ((x\y)\z)*(z\(z\x)))
implies X is implicative
proof
assume
A8: for x,y,z being Element of X holds x\(y\z) = ((x\y)\z)*(z\(z\x));
for x,y being Element of X holds x\(y\x) = x
proof
let x,y be Element of X;
x\(y\x) = ((x\y)\x)*(x\(x\x)) by A8
.= ((x\y)\x)*(x\0.X) by BCIALG_1:def 5
.= ((x\y)\x)*x by BCIALG_1:2
.= ((x\x)\y)*x by BCIALG_1:7
.= (y`)*x by BCIALG_1:def 5
.= 0.X*x by BCIALG_1:def 8;
hence thesis by Th8;
end;
hence thesis;
end;
hence thesis by A1;
end;