:: Congruences and Quotient Algebras of {BCI}-algebras :: by Yuzhong Ding and Zhiyong Pang :: :: Received August 28, 2007 :: Copyright (c) 2007-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies BCIALG_1, CARD_FIL, SUBSET_1, FUNCT_1, NUMBERS, STRUCT_0, POWER, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, FUNCOP_1, NAT_1, SUPINF_2, RELAT_1, CHORD, WAYBEL15, GROUP_4, GROUP_1, ALG_1, EQREL_1, PARTFUN1, RELAT_2, ZFMISC_1, RCOMP_1, TARSKI, BINOP_1, GROUP_6, BCIALG_2, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FUNCT_2, XXREAL_0, FUNCOP_1, BINOP_1, STRUCT_0, BCIALG_1, RELAT_2, PARTFUN1, EQREL_1, ALG_1; constructors BCIALG_1, BINOP_1, NAT_1, BINARITH, EQREL_1, RELSET_1, XREAL_0, NUMBERS, FUNCOP_1; registrations BCIALG_1, SUBSET_1, NAT_1, RELSET_1, STRUCT_0, PARTFUN1, ORDINAL1, XREAL_0, CARD_1; requirements NUMERALS, ARITHM, SUBSET, BOOLE; begin :: Basic Properties of The Element P16-P19 reserve X for BCI-algebra; reserve I for Ideal of X; reserve a,x,y,z,u for Element of X; reserve f,f9,g for sequence of the carrier of X; reserve j,i,k,n,m for Nat; :: x*y to_power n = x*y|^n :: n=0: it=x; n=1:it =x*y; n=2:it=(x*y)*y... definition let X,x,y; let n be Nat; func (x,y) to_power n -> Element of X means :: BCIALG_2:def 1 ex f st it = f.n & f.0 = x & for j being Nat st j positive minimal; end; theorem :: BCIALG_2:23 a is minimal iff for x holds a\x=x`\a`; theorem :: BCIALG_2:24 x` is minimal iff for y holds y<=x implies x` = y`; theorem :: BCIALG_2:25 x` is minimal iff for y,z holds (((x\z)\(y\z))`)` = y`\x`; theorem :: BCIALG_2:26 0.X is maximal implies for a holds a is minimal; theorem :: BCIALG_2:27 (ex x st x is greatest) implies for a holds a is positive; theorem :: BCIALG_2:28 x\(x``) is positive Element of X; theorem :: BCIALG_2:29 a is minimal iff a`` = a; theorem :: BCIALG_2:30 a is minimal iff ex x st a=x`; :: p38 definition let X,x; attr x is nilpotent means :: BCIALG_2:def 6 ex k being non zero Nat st (0.X ,x) to_power k = 0.X; end; definition let X; attr X is nilpotent means :: BCIALG_2:def 7 for x being Element of X holds x is nilpotent; end; definition let X,x; assume x is nilpotent; func ord x -> non zero Nat means :: BCIALG_2:def 8 (0.X,x) to_power it = 0. X & for m being Nat st (0.X,x) to_power m=0.X & m <> 0 holds it <= m; end; registration let X; cluster 0.X -> nilpotent; end; theorem :: BCIALG_2:31 :: P39 x is positive Element of X iff x is nilpotent & ord x=1; theorem :: BCIALG_2:32 X is BCK-algebra iff for x holds ord x=1 & x is nilpotent; theorem :: BCIALG_2:33 (0.X,x`) to_power n is minimal; theorem :: BCIALG_2:34 x is nilpotent implies ord x = ord (x`); begin :: Congruence and Quotient Algebras P58-65 definition let X be BCI-algebra; mode Congruence of X -> Equivalence_Relation of X means :: BCIALG_2:def 9 for x,y,u,v being Element of X st [x,y] in it & [u,v] in it holds [x\u,y\v] in it; end; :: Left Congruence definition let X be BCI-algebra; mode L-congruence of X -> Equivalence_Relation of X means :: BCIALG_2:def 10 for x,y being Element of X st [x,y] in it holds for u being Element of X holds [u\x,u\y ] in it; end; :: Right Congruence definition let X be BCI-algebra; mode R-congruence of X -> Equivalence_Relation of X means :: BCIALG_2:def 11 for x,y being Element of X st [x,y] in it holds for u being Element of X holds [x\u,y\u ] in it; end; ::Ideal Congruence definition let X be BCI-algebra,A be Ideal of X; mode I-congruence of X,A -> Relation of X means :: BCIALG_2:def 12 for x,y being Element of X holds [x,y] in it iff x\y in A & y\x in A; end; registration let X be BCI-algebra, A be Ideal of X; cluster -> total symmetric transitive for I-congruence of X,A; end; definition let X be BCI-algebra; func IConSet(X) -> set means :: BCIALG_2:def 13 for A1 being set holds A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I; end; definition let X be BCI-algebra; func ConSet(X) -> set equals :: BCIALG_2:def 14 the set of all R where R is Congruence of X; func LConSet(X) -> set equals :: BCIALG_2:def 15 the set of all R where R is L-congruence of X; func RConSet(X) -> set equals :: BCIALG_2:def 16 the set of all R where R is R-congruence of X; end; reserve R for Equivalence_Relation of X; reserve RI for I-congruence of X,I; reserve E for Congruence of X; reserve RC for R-congruence of X; reserve LC for L-congruence of X; :: huang-P58:P1.5.1 theorem :: BCIALG_2:35 for X,E holds Class(E,0.X) is closed Ideal of X; theorem :: BCIALG_2:36 R is Congruence of X iff R is R-congruence of X&R is L-congruence of X; theorem :: BCIALG_2:37 RI is Congruence of X; definition let X be BCI-algebra, I be Ideal of X; redefine mode I-congruence of X,I -> Congruence of X; end; theorem :: BCIALG_2:38 Class(RI,0.X) c= I; theorem :: BCIALG_2:39 I is closed iff I = Class(RI,0.X); theorem :: BCIALG_2:40 [x,y] in E implies x\y in Class(E,0.X) & y\x in Class(E,0.X); theorem :: BCIALG_2:41 for A,I being Ideal of X,IA being I-congruence of X,A, II being I-congruence of X,I st Class(IA,0.X)=Class(II,0.X) holds IA = II; theorem :: BCIALG_2:42 [x,y] in E & u in Class(E,0.X) implies [x,(y,u)to_power k] in E; theorem :: BCIALG_2:43 (for X,x,y holds ex i,j,m,n st ((x,x\y) to_power i,y\x) to_power j = ( (y,y\x)to_power m,x\y) to_power n) implies for E,I st I=Class(E,0.X) holds E is I-congruence of X,I; theorem :: BCIALG_2:44 IConSet(X) c= ConSet(X); theorem :: BCIALG_2:45 ConSet(X) c= LConSet(X); theorem :: BCIALG_2:46 ConSet(X) c= RConSet(X); theorem :: BCIALG_2:47 ConSet(X) = LConSet(X)/\RConSet(X); theorem :: BCIALG_2:48 (for LC holds LC is I-congruence of X,I) implies E = RI; theorem :: BCIALG_2:49 (for RC holds RC is I-congruence of X,I) implies E = RI; theorem :: BCIALG_2:50 Class(LC,0.X) is closed Ideal of X; :: Quotient Algebras reserve E for Congruence of X; reserve RI for I-congruence of X,I; registration let X,E; cluster Class E -> non empty; end; definition let X,E; func EqClaOp E -> BinOp of Class E means :: BCIALG_2:def 17 for W1,W2 being Element of Class(E) for x,y st W1=Class(E,x) & W2=Class(E,y) holds it.(W1,W2)=Class(E,x\y) ; end; definition let X,E; func zeroEqC(E) -> Element of Class E equals :: BCIALG_2:def 18 Class(E,0.X); end; ::Quotient Algebras definition let X,E; func X./.E -> BCIStr_0 equals :: BCIALG_2:def 19 BCIStr_0(#Class E,EqClaOp E,zeroEqC(E)#); end; registration let X; let E be Congruence of X; cluster X./.E -> non empty; end; reserve W1,W2 for Element of Class E; definition let X,E,W1,W2; func W1\W2 -> Element of Class E equals :: BCIALG_2:def 20 (EqClaOp E).(W1,W2); end; theorem :: BCIALG_2:51 X./.RI is BCI-algebra; registration let X,I,RI; cluster X./.RI -> strict being_B being_C being_I being_BCI-4; end; theorem :: BCIALG_2:52 for X,I st I = BCK-part(X) holds for RI being I-congruence of X,I holds X./.RI is p-Semisimple BCI-algebra;