:: Congruences and Quotient Algebras of {BCI}-algebras
:: by Yuzhong Ding and Zhiyong Pang
::
:: Received August 28, 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, 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;
definitions XBOOLE_0, TARSKI, RELAT_1;
equalities STRUCT_0, BCIALG_1, RELAT_1;
expansions BCIALG_1;
theorems BCIALG_1, FUNCOP_1, NAT_1, XREAL_1, TARSKI, XBOOLE_0, RELAT_2,
RELAT_1, XXREAL_0, ORDERS_1, XBOOLE_1, BINOP_1, EQREL_1, RELSET_1,
ZFMISC_1, ORDINAL1;
schemes FUNCT_2, NAT_1, RELSET_1, XBOOLE_0, BINOP_1;
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
:Def1:
ex f st it = f.n & f.0 = x & for j being Nat st j<n holds f.(j+1) = f.j\y;
existence
proof
defpred P[set] means for x,y being Element of X,n being Nat st
n=$1 ex u being Element of X st ex f being sequence of the carrier of X st
u = f.n & f.0 = x & for j being Nat st j<n holds f.(j+1) = f.j\y;
now
let n be Nat;
assume
A1: for x,y,k st k=n ex u st ex f st u = f.k & f.0 = x & for j st j<
k holds f.(j+1) = f.j\y;
let x,y,k;
consider u,f such that
u = f.n and
A2: f.0= x and
A3: for j st j<n holds f.(j+1) = f.j\y by A1;
defpred P[set,set] means for j st $1=j holds (j<n + 1 implies $2 = f.$1)
&(n+1<=j implies $2=f.n\y);
assume k = n + 1;
A4: for k being Element of NAT ex v being Element of X st P[k,v]
proof
let k be Element of NAT;
reconsider i = k as Nat;
A5: now
assume
A6: n + 1 <= i;
take v = f.n \ y;
let j;
assume k = j;
hence j < n + 1 implies v = f.k by A6;
assume n + 1 <= j;
thus v = f.n \ y;
end;
now
assume
A7: i < n + 1;
take v = f.k;
let j such that
A8: k = j;
thus j < n + 1 implies v = f.k;
thus n + 1 <= j implies v = f.n \ y by A7,A8;
end;
hence thesis by A5;
end;
consider f9 being sequence of the carrier of X such that
A9: for k being Element of NAT holds P[k,f9.k] from FUNCT_2:sch 3(A4);
A10: for k being Nat holds P[k,f9.k]
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A9;
end;
take z = f9.(n + 1);
take f99 = f9;
thus z = f99.(n+1);
0<n+1 by NAT_1:5;
hence f99.0 = x by A2,A10;
let j;
A11: now
assume
A12: j < n;
then f.(j + 1) = f.j \ y & j < n + 1 by A3,NAT_1:13;
then
A13: f.(j + 1) = f9.j \ y by A10;
j + 1 < n + 1 by A12,XREAL_1:6;
hence f99.(j + 1) = f99.j \ y by A10,A13;
end;
A14: n <n+1 by NAT_1:13;
A15: now
assume
A16: j = n;
then f99.(j + 1) = f.j \ y by A10;
hence f99.(j + 1) = f99.j \ y by A14,A10,A16;
end;
assume j < n+1;
then j <= n by NAT_1:13;
hence f99.(j + 1) = f99.j \ y by A11,A15,XXREAL_0:1;
end;
then
A17: for n be Nat st P[n] holds P[n+1];
now
let x,y be Element of X,n be Nat;
assume
A18: n = 0;
reconsider f = NAT-->x as sequence of the carrier of X;
take u = f.n;
take f9 = f;
thus u = f9.n & f9.0 = x by FUNCOP_1:7;
thus for j being Nat st j<n holds f9.(j+1) = f9.j\y by A18,NAT_1:3;
end;
then
A19: P[0];
for n holds P[n] from NAT_1:sch 2(A19,A17);
hence thesis;
end;
uniqueness
proof
let v1,v2 be Element of X;
given f such that
A20: v1 = f.n and
A21: f.0 = x and
A22: for j st j < n holds f.(j + 1) = f.j \ y;
given f9 such that
A23: v2 = f9.n and
A24: f9.0 = x and
A25: for j st j < n holds f9.(j + 1) = f9.j \ y;
defpred P[Nat] means $1 <= n implies f.$1 = f9.$1;
now
let k;
assume
A26: k <= n implies f.k = f9.k;
assume k + 1 <= n;
then
A27: k < n by NAT_1:13;
then f.(k + 1) = f.k \y by A22;
hence f.(k + 1) = f9.(k + 1) by A25,A26,A27;
end;
then
A28: for k st P[k] holds P[k+1];
A29: P[0] by A21,A24;
for k holds P[k] from NAT_1:sch 2(A29,A28);
hence thesis by A20,A23;
end;
end;
theorem Th1:
(x,y) to_power 0 = x
proof
ex f st (x,y) to_power 0 = f.0 & f.0 = x & for j st j < 0 holds f.(j + 1
) = f.j \ y by Def1;
hence thesis;
end;
theorem Th2:
(x,y) to_power 1 = x\y
proof
consider f such that
A1: (x,y) to_power 1 = f.1 and
A2: f.0 = x & for j st j < 1 holds f.(j + 1) = f.j \ y by Def1;
f.(0+1) = x\y by A2,NAT_1:3;
hence thesis by A1;
end;
theorem
(x,y) to_power 2 = x\y\y
proof
consider f such that
A1: (x,y) to_power 2 = f.2 & f.0 = x and
A2: for j st j < 2 holds f.(j + 1) = f.j \ y by Def1;
1<1+1 by NAT_1:13;
then f.(1+1) = f.(0+1) \y by A2;
hence thesis by A1,A2,NAT_1:3;
end;
theorem Th4:
(x,y) to_power (n+1) = (x,y) to_power n \ y
proof
A1: n<n+1 by NAT_1:3,XREAL_1:29;
consider g such that
A2: (x,y) to_power n = g.n and
A3: g.0 = x and
A4: for j st j < n holds g.(j + 1) = g.j \ y by Def1;
consider f such that
A5: (x,y) to_power (n+1) = f.(n+1) and
A6: f.0 = x and
A7: for j st j < n+1 holds f.(j + 1) = f.j \ y by Def1;
defpred P[set] means for m holds m=$1 & m <= n implies f.m=g.m;
now
let k;
assume
A8: for m st m=k & m<=n holds f.m=g.m;
let m;
assume that
A9: m=k+1 and
A10: m<=n;
k +1 <= n+1 by A9,A10,NAT_1:13;
then k<n+1 by NAT_1:13;
then
A11: f.(k + 1) = f.k \y by A7;
A12: k<n by A9,A10,NAT_1:13;
then g.(k + 1) = g.k \y by A4;
hence f.m=g.m by A8,A9,A12,A11;
end;
then
A13: for k st P[k] holds P[k+1];
A14: P[0] by A6,A3;
for n holds P[n] from NAT_1:sch 2(A14,A13);
then f.n = g.n;
hence thesis by A5,A7,A2,A1;
end;
theorem Th5:
(x,0.X) to_power (n+1) = x
proof
defpred P[set] means for m holds m=$1 & m<= n implies (x,0.X) to_power (m+1)
= x;
now
let k;
assume
A1: for m st m=k & m<= n holds (x,0.X) to_power (m+1) = x;
let m;
assume that
A2: m=k+1 and
A3: m<=n;
(x,0.X) to_power (m+1)=((x,0.X) to_power (k+1))\0.X by A2,Th4;
then
A4: (x,0.X) to_power (m+1)=(x,0.X) to_power (k+1) by BCIALG_1:2;
k<=n by A2,A3,NAT_1:13;
hence (x,0.X) to_power (m+1)= x by A1,A4;
end;
then
A5: for k st P[k] holds P[k+1];
(x,0.X) to_power (0+1) = x \ 0.X by Th2;
then
A6: P[0] by BCIALG_1:2;
for n holds P[n] from NAT_1:sch 2(A6,A5);
hence thesis;
end;
theorem Th6:
(0.X,0.X) to_power n=0.X
proof
defpred P[set] means for m holds m=$1 & m<= n implies (0.X,0.X) to_power m =
0.X;
A1: for k st P[k] holds P[k+1] by Th5;
A2: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th7:
(x,y) to_power n\z = (x\z,y) to_power n
proof
defpred P[set] means for m holds m=$1 & m<= n implies (x,y) to_power m\z = (
x\z,y) to_power m;
now
let k;
assume
A1: for m st m=k & m<= n holds (x,y) to_power m\z = (x\z,y) to_power m;
let m;
assume that
A2: m=k+1 and
A3: m<=n;
(x,y) to_power m\z=((x,y) to_power k\y)\z by A2,Th4;
then
A4: (x,y) to_power m\z=((x,y) to_power k\z)\y by BCIALG_1:7;
k<=n by A2,A3,NAT_1:13;
then (x,y) to_power m\z= ((x\z,y) to_power k)\y by A1,A4;
hence (x,y) to_power m\z= (x\z,y) to_power (k+1) by Th4;
end;
then
A5: for k st P[k] holds P[k+1];
(x,y) to_power 0\z = x\z by Th1;
then
A6: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A6,A5);
hence thesis;
end;
theorem
(x,x\(x\y)) to_power n = (x,y) to_power n
proof
defpred P[set] means for m holds m=$1 & m<= n implies (x,x\(x\y)) to_power m
= (x,y) to_power m;
now
let k;
assume
A1: for m holds m=k & m<= n implies (x,x\(x\y)) to_power m = (x,y) to_power m;
let m;
A2: (x,x\(x\y)) to_power (k+1) =(x,x\(x\y)) to_power k\(x\(x\y)) by Th4;
assume m=k+1 & m<=n;
then k<=n by NAT_1:13;
hence (x,x\(x\y)) to_power (k+1)=(x,y) to_power k \(x\(x\y)) by A1,A2
.=(x\(x\(x\y)),y) to_power k by Th7
.=(x\y,y) to_power k by BCIALG_1:8
.=(x,y) to_power k\y by Th7
.=(x,y) to_power (k+1) by Th4;
end;
then
A3: for k st P[k] holds P[k+1];
(x,x\(x\y)) to_power 0 = x by Th1;
then
A4: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem Th9:
((0.X,x) to_power n)` = (0.X,x`) to_power n
proof
defpred P[set] means for m holds m=$1 & m<= n implies ((0.X,x) to_power m)`
= (0.X,x`) to_power m;
now
let k;
assume
A1: for m holds m=k & m<= n implies ((0.X,x) to_power m)` = (0.X,x`)
to_power m;
let m;
A2: ((0.X,x) to_power (k+1))`=((0.X,x) to_power k\x)` by Th4
.=((0.X,x) to_power k)`\x` by BCIALG_1:9;
assume m=k+1 & m<=n;
then k<=n by NAT_1:13;
hence ((0.X,x) to_power (k+1))` = ((0.X,x`) to_power k)\x` by A1,A2
.=(0.X,x`) to_power (k+1) by Th4;
end;
then
A3: for k st P[k] holds P[k+1];
((0.X,x) to_power 0)`= (0.X)` by Th1;
then ((0.X,x) to_power 0)`= 0.X by BCIALG_1:2;
then
A4: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem Th10:
((x,y) to_power n,y) to_power m =(x,y) to_power (n+m)
proof
defpred P[set] means for m1 being Nat holds m1=$1 & m1<= n
implies ((x,y) to_power m1,y) to_power m =(x,y) to_power (m1+m);
now
let k;
assume
A1: for m1 being Nat st m1=k & m1<=n holds((x,y) to_power
m1,y) to_power m =(x,y) to_power (m1+m);
let m1 be Nat;
assume that
A2: m1=k+1 and
A3: m1<=n;
k<=n by A2,A3,NAT_1:13;
then ((x,y) to_power k,y) to_power m =(x,y) to_power (k+m) by A1;
then (((x,y) to_power k,y) to_power m)\y=(x,y) to_power (k+m+1) by Th4;
then (((x,y) to_power k)\y,y) to_power m=(x,y) to_power (k+m+1) by Th7;
hence ((x,y) to_power m1,y) to_power m=(x,y) to_power (m1+m) by A2,Th4;
end;
then
A4: for k st P[k] holds P[k+1];
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A4);
hence thesis;
end;
theorem
((x,y) to_power n,z) to_power m =((x,z) to_power m,y)to_power n
proof
defpred P[set] means for m1 being Nat holds m1=$1 & m1<= n
implies ((x,y) to_power m1,z) to_power m =((x,z) to_power m,y)to_power m1;
now
let k;
assume
A1: for m1 being Nat st m1=k & m1<=n holds ((x,y) to_power
m1,z) to_power m =((x,z) to_power m,y)to_power m1;
let m1 be Nat;
assume m1=k+1 & m1<=n;
then k<=n by NAT_1:13;
then
(((x,y) to_power k,z) to_power m)\y =((x,z) to_power m,y)to_power k \
y by A1
.=((x,z) to_power m,y)to_power (k+1) by Th4;
then
((x,z) to_power m,y)to_power (k+1) =((x,y) to_power k\y,z) to_power m
by Th7;
hence
((x,y) to_power (k+1),z) to_power m =((x,z) to_power m,y)to_power (k+
1) by Th4;
end;
then
A2: for k st P[k] holds P[k+1];
((x,y) to_power 0,z)to_power m =(x,z)to_power m by Th1;
then
A3: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem Th12:
((0.X,x) to_power n)``=(0.X,x) to_power n
proof
defpred P[set] means for m being Nat holds m=$1 & m<=n implies ((
(0.X,x)to_power m)`)`=(0.X,x)to_power m;
now
let k;
assume
A1: for m being Nat st m=k & m<=n holds (((0.X,x)to_power m
)`)`=(0.X,x)to_power m;
let m be Nat;
assume m=k+1 & m<=n;
then
A2: k<=n by NAT_1:13;
(((0.X,x)to_power (k+1))`)` =(((0.X,x)to_power k\x)`)` by Th4
.=(((0.X,x) to_power k)`\x`)` by BCIALG_1:9
.=(((0.X,x)to_power k)`)`\((x`)`) by BCIALG_1:9
.=(0.X,x)to_power k\((x`)`) by A1,A2
.=(((x`)`)`,x)to_power k by Th7
.=(x`,x)to_power k by BCIALG_1:8
.=(0.X,x)to_power k\x by Th7;
hence (((0.X,x)to_power (k+1))`)` =(0.X,x)to_power (k+1) by Th4;
end;
then
A3: for k st P[k] holds P[k+1];
(((0.X,x)to_power 0)`)`=((0.X)`)` by Th1
.=(0.X)` by BCIALG_1:def 5
.=0.X by BCIALG_1:def 5;
then
A4: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem Th13:
(0.X,x)to_power (n+m)=((0.X,x)to_power n)\((0.X,x)to_power m)`
proof
defpred P[set] means for j being Nat holds j=$1 & j<=n implies (
0.X,x)to_power (j+m)=((0.X,x)to_power j)\((0.X,x)to_power m)`;
now
let k;
assume
A1: for j being Nat st j=k & j<=n holds (0.X,x)to_power (j+
m)=((0.X,x)to_power j)\((0.X,x)to_power m)`;
let j be Nat;
assume j=k+1 & j<=n;
then
A2: k<=n by NAT_1:13;
(0.X,x)to_power (k+m+1)=((0.X,x)to_power (k+m))\x by Th4
.=(((0.X,x)to_power k)\((0.X,x)to_power m)`)\x by A1,A2
.=(((0.X,x)to_power k)\x)\((0.X,x)to_power m)` by BCIALG_1:7;
hence
(0.X,x)to_power ((k+1)+m) =((0.X,x)to_power (k+1))\((0.X,x)to_power m
)` by Th4;
end;
then
A3: for k st P[k] holds P[k+1];
(0.X,x)to_power (0+m) =(((0.X,x)to_power m)`)` by Th12;
then
A4: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem
((0.X,x) to_power (m+n))` = ((0.X,x)to_power m)`\(0.X,x)to_power n
proof
((0.X,x)to_power (m+n))` =(((0.X,x)to_power m)\((0.X,x)to_power n)`)` by Th13
.=(((0.X,x)to_power m)`)\(((0.X,x)to_power n)`)` by BCIALG_1:9;
hence thesis by Th12;
end;
theorem
((0.X,(0.X,x)to_power m)to_power n)`=(0.X,x)to_power (m*n)
proof
defpred P[set] means for j being Nat holds j=$1 & j<=n implies ((
0.X,(0.X,x)to_power m)to_power j)`=(0.X,x)to_power (m*j);
now
let k;
assume
A1: for j being Nat st j=k & j<=n holds ((0.X,(0.X,x)
to_power m)to_power j)`=(0.X,x)to_power (m*j);
let j be Nat;
assume j=k+1 & j<=n;
then
A2: k<=n by NAT_1:13;
((0.X,(0.X,x)to_power m)to_power (k+1))` =(((0.X,(0.X,x)to_power m)
to_power k)\((0.X,x)to_power m))`by Th4
.=((0.X,(0.X,x)to_power m)to_power k)`\((0.X,x)to_power m)` by BCIALG_1:9
.=((0.X,x)to_power (m*k))\((0.X,x)to_power m)`by A1,A2
.=(0.X,x)to_power (m*k+m)by Th13;
hence ((0.X,(0.X,x)to_power m)to_power (k+1))` =(0.X,x)to_power (m*(k+1));
end;
then
A3: for k st P[k] holds P[k+1];
((0.X,(0.X,x)to_power m)to_power 0)` =(0.X)` by Th1
.= 0.X by BCIALG_1:def 5;
then
A4: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem
(0.X,x)to_power m=0.X implies(0.X,x)to_power (m*n)=0.X
proof
defpred P[set] means for j being Nat holds j=$1 & j<=n implies (
0.X,x)to_power (m*j)=0.X;
assume
A1: (0.X,x)to_power m=0.X;
now
let k;
assume
A2: for j st j=k & j<=n holds (0.X,x)to_power (m*j)=0.X;
let j;
assume j=k+1 & j<=n;
then
A3: k<=n by NAT_1:13;
(0.X,x)to_power (m*(k+1)) = (0.X,x)to_power (m*k+m)
.= ((0.X,x)to_power (m*k),x)to_power m by Th10
.= (0.X,x)to_power m by A2,A3;
hence (0.X,x)to_power (m*(k+1))=0.X by A1;
end;
then
A4: for k st P[k] holds P[k+1];
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A4);
hence thesis;
end;
theorem
x\y=x implies (x,y) to_power n = x
proof
defpred P[set] means for m holds m=$1 & m<=n implies (x,y) to_power m = x;
assume
A1: x\y=x;
now
let k;
assume
A2: for m holds m=k & m<= n implies (x,y) to_power m = x;
let m;
A3: (x,y) to_power (k+1)=(x,y) to_power k \ y by Th4;
assume m=k+1 & m<=n;
then k<=n by NAT_1:13;
hence (x,y) to_power (k+1)=x by A1,A2,A3;
end;
then
A4: for k st P[k] holds P[k+1];
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A4);
hence thesis;
end;
theorem
(0.X,x\y) to_power n=((0.X,x) to_power n)\((0.X,y) to_power n)
proof
defpred P[set] means for m holds m=$1 & m<=n implies (0.X,x\y) to_power m=((
0.X,x) to_power m)\((0.X,y) to_power m);
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for m holds m=k & m<= n implies (0.X,x\y) to_power m=((0.X,x)
to_power m)\((0.X,y) to_power m);
let m;
assume that
A3: m=k+1 and
A4: m<=n;
k<=n by A3,A4,NAT_1:13;
then
(0.X,x\y) to_power k =((0.X,x) to_power k)\((0.X,y) to_power k) by A2;
then
(0.X,x\y) to_power (k+1) =(((0.X,x) to_power k)\((0.X,y) to_power k))
\(x\y)by Th4
.= ((0.X,x) to_power k)\(x\y)\((0.X,y) to_power k)by BCIALG_1:7
.= (((x\y)`,x) to_power k)\((0.X,y) to_power k)by Th7
.=((x`\y`,x) to_power k)\((0.X,y) to_power k)by BCIALG_1:9
.=((x`,x) to_power k)\y`\((0.X,y) to_power k)by Th7
.=((x`,x) to_power k)\((0.X,y) to_power k)\y` by BCIALG_1:7
.=((0.X,x) to_power k)\x\((0.X,y) to_power k)\y` by Th7;
then (0.X,x\y) to_power (k+1) =((0.X,x) to_power (k+1))\((0.X,y) to_power
k)\y` by Th4
.=((0.X,x) to_power (k+1))\y`\((0.X,y) to_power k)by BCIALG_1:7
.=(((y`)`,x) to_power (k+1))\((0.X,y) to_power k)by Th7
.=(((y`)`\((0.X,y) to_power k),x) to_power (k+1))by Th7
.=(((0.X,y) to_power k)`\y`,x) to_power (k+1)by BCIALG_1:7
.=((((0.X,y) to_power k)\y)`,x) to_power (k+1)by BCIALG_1:9
.=(((0.X,y) to_power (k+1))`,x) to_power (k+1)by Th4;
hence thesis by A3,Th7;
end;
(0.X)`=0.X by BCIALG_1:def 5;
then (0.X,x\y) to_power 0=(0.X)` by Th1;
then (0.X,x\y) to_power 0=((0.X,x) to_power 0)\0.X by Th1;
then
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
::P20-P22
theorem
x<=y implies (x,z) to_power n <= (y,z) to_power n
proof
defpred P[set] means for m being Nat holds m=$1 & m<=n implies (x
,z) to_power m <= (y,z) to_power m;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for m being Nat holds m=k & m<= n implies (x,z)
to_power m <= (y,z) to_power m;
let m be Nat;
assume that
A3: m=k+1 and
A4: m<=n;
k<=n by A3,A4,NAT_1:13;
then (x,z) to_power k <= (y,z) to_power k by A2;
then (x,z) to_power k\z<=(y,z) to_power k \ z by BCIALG_1:5;
then (x,z) to_power (k+1)<=(y,z) to_power k\z by Th4;
hence thesis by A3,Th4;
end;
assume x<=y;
then (x,z) to_power 0 <= y by Th1;
then
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem
x<=y implies (z,y) to_power n <= (z,x) to_power n
proof
defpred P[set] means for m being Nat holds m=$1 & m<=n implies (z
,y) to_power m <= (z,x) to_power m;
assume
A1: x<=y;
A2: for k st P[k] holds P[k+1]
proof
let k;
assume
A3: for m holds m=k & m<= n implies (z,y) to_power m <= (z,x) to_power m;
((z,x) to_power k)\y<=(z,x) to_power k\x by A1,BCIALG_1:5;
then (z,x) to_power k\y<=(z,x) to_power (k+1) by Th4;
then
A4: ((z,x) to_power k\y)\((z,x) to_power (k+1))=0.X;
let m;
assume that
A5: m=k+1 and
A6: m<=n;
k<=n by A5,A6,NAT_1:13;
then (z,y) to_power k <= (z,x) to_power k by A3;
then (z,y) to_power k\y <= (z,x) to_power k\y by BCIALG_1:5;
then (z,y) to_power (k+1)<= (z,x) to_power k\y by Th4;
then ((z,y) to_power (k+1))\((z,x) to_power k\y)=0.X;
then ((z,y) to_power (k+1))\((z,x) to_power (k+1))=0.X by A4,BCIALG_1:3;
hence thesis by A5;
end;
z\z=0.X by BCIALG_1:def 5;
then z<=z;
then (z,y) to_power 0 <= z by Th1;
then
A7: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
theorem
((x,z) to_power n)\((y,z) to_power n) <= x\y
proof
defpred P[set] means for m being Nat holds m=$1 & m<=n implies ((
x,z) to_power m)\((y,z) to_power m) <= x\y;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for m being Nat holds m=k & m<= n implies((x,z)
to_power m)\((y,z) to_power m) <= x\y;
let m be Nat;
assume that
A3: m=k+1 and
A4: m<=n;
k<=n by A3,A4,NAT_1:13;
then ((x,z) to_power k)\((y,z) to_power k) <= x\y by A2;
then (((x,z) to_power k)\((y,z) to_power k))\(x\y)=0.X;
then (((x,z) to_power k)\(x\y))\((y,z) to_power k)=0.X by BCIALG_1:7;
then (((x,z) to_power k)\(x\y))\z\(((y,z) to_power k)\z)=0.X by BCIALG_1:4;
then (((x,z) to_power k)\z)\(x\y)\(((y,z) to_power k)\z)=0.X by BCIALG_1:7;
then ((x,z) to_power (k+1))\(x\y)\(((y,z) to_power k)\z)=0.X by Th4;
then ((x,z) to_power (k+1))\(x\y)\((y,z) to_power (k+1))=0.X by Th4;
then ((x,z) to_power (k+1))\((y,z) to_power (k+1))\(x\y)=0.X by BCIALG_1:7;
hence thesis by A3;
end;
(x\y)\(x\y)=0.X by BCIALG_1:def 5;
then x\y <= x\y;
then ((x,z) to_power 0)\y <= x\y by Th1;
then
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem
(((x,x\y) to_power n),y\x) to_power n <= x
proof
defpred P[set] means for m being Nat holds m=$1 & m<=n implies ((
(x,x\y) to_power m),y\x) to_power m <= x;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for m being Nat holds m=k & m<= n implies (((x,x\y)
to_power m),y\x) to_power m <= x;
let m be Nat;
assume that
A3: m=k+1 and
A4: m<=n;
k<=n by A3,A4,NAT_1:13;
then (((x,x\y) to_power k),y\x) to_power k <= x by A2;
then ((((x,x\y) to_power k),y\x) to_power k)\x=0.X;
then ((((x,x\y) to_power k)\x,y\x) to_power k)\(y\x)=(y\x)`by Th7;
then ((((x,x\y) to_power k)\x,y\x)to_power (k+1))\(x\y) =(y\x)`\(x\y)by Th4
;
then (((x,x\y) to_power k)\x\(x\y),y\x) to_power (k+1)=(y\x)`\(x\y)by Th7;
then
(((x,x\y) to_power k)\(x\y)\x,y\x) to_power (k+1)=(y\x)`\(x\y) by BCIALG_1:7;
then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1)=(y\x)`\(x\y)by Th4;
then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1) =(y\y)\(y\x)\(x\y)by
BCIALG_1:def 5;
then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1)=0.X by BCIALG_1:1;
then (((x,x\y) to_power (k+1),y\x) to_power (k+1))\x=0.X by Th7;
hence thesis by A3;
end;
x\x=0.X by BCIALG_1:def 5;
then x<=x;
then (x,y\x) to_power 0<=x by Th1;
then
A5: P[0] by Th1;
for n holds P[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
notation
let X,a;
synonym a is minimal for a is atom;
end;
::P17 proposition 1.1.10
definition
let X,a;
attr a is positive means
:Def2:
0.X <= a;
attr a is least means
for x holds a<=x;
attr a is maximal means
for x holds a<=x implies x=a;
attr a is greatest means
for x holds x<=a;
end;
Lm1: a is minimal iff for x holds x<=a implies x=a
by BCIALG_1:def 11;
Lm2: 0.X is positive
proof
(0.X)`=0.X by BCIALG_1:2;
then 0.X <= 0.X;
hence thesis;
end;
registration
let X;
cluster positive for Element of X;
existence
proof
take 0.X;
thus thesis by Lm2;
end;
end;
Lm3: 0.X is minimal
by BCIALG_1:2;
registration
let X;
cluster 0.X -> positive minimal;
coherence by Lm2,Lm3;
end;
theorem
a is minimal iff for x holds a\x=x`\a`
proof
thus a is minimal implies for x holds a\x=x`\a`
proof
assume
A1: a is minimal;
let x;
x\(x\a)\a=0.X by BCIALG_1:1;
then x\(x\a)<=a;
then
A2: (a\x)\(x`\a`)=((x\(x\a))\x)\(x`\a`)by A1
.=((x\x)\(x\a))\(x`\a`) by BCIALG_1:7
.=((x\a)`)\(x`\a`) by BCIALG_1:def 5
.=((x\a)`)\((x\a)`) by BCIALG_1:9
.=0.X by BCIALG_1:def 5;
(x`\a`)\(a\x)=0.X by BCIALG_1:1;
hence thesis by A2,BCIALG_1:def 7;
end;
thus (for x holds a\x=x`\a`) implies a is minimal
proof
assume
A3: for x holds a\x=x`\a`;
now
let x;
assume x<=a;
then
A4: x\a=0.X;
a\x=x`\a` by A3;
then a\x=(0.X)` by A4,BCIALG_1:9;
then a\x=0.X by BCIALG_1:def 5;
hence a=x by A4,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
x` is minimal iff for y holds y<=x implies x` = y`
proof
thus x` is minimal implies for y holds y<=x implies x` = y`
proof
assume
A1: x` is minimal;
let y;
assume y<=x;
then y\x=0.X;
then (y\x)`=0.X by BCIALG_1:def 5;
then y`\x`=0.X by BCIALG_1:9;
then y`<=x`;
hence thesis by A1;
end;
thus (for y holds y<=x implies x` = y`)implies x` is minimal
proof
assume
A2: for y holds y<=x implies x` = y`;
now
let xx be Element of X;
assume xx<=x`;
then
A3: xx\x`=0.X;
then (xx\x`)`=0.X by BCIALG_1:def 5;
then xx`\((x`)`)=0.X by BCIALG_1:9;
then (xx`\((x`)`))`=0.X by BCIALG_1:def 5;
then ((xx`)`)\(((x`)`)`)=0.X by BCIALG_1:9;
then ((xx`)`)\x`=0.X by BCIALG_1:8;
then (xx`\x)`=0.X by BCIALG_1:9;
then (x`\xx)`=0.X by BCIALG_1:7;
then (xx\xx)\(x`\xx)=0.X by BCIALG_1:def 5;
then (xx\x`)`=0.X by BCIALG_1:def 3;
then xx`\((x`)`)=0.X by BCIALG_1:9;
then xx`\x\(((x`)`)\x)=0.X by BCIALG_1:4;
then xx`\x\0.X=0.X by BCIALG_1:1;
then xx`\x=0.X by BCIALG_1:2;
then xx`<=x;
then (xx`)`=x` by A2;
then 0.X = x`\xx by BCIALG_1:1;
hence xx=x` by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
x` is minimal iff for y,z holds (((x\z)\(y\z))`)` = y`\x`
proof
thus x` is minimal implies for y,z holds (((x\z)\(y\z))`)` = y`\x`
proof
assume
A1: x` is minimal;
let y,z;
y`\(x\y)\x`=0.X by BCIALG_1:def 3;
then
A2: y`\(x\y)<=x`;
(((x\z)\(y\z))`)` = ((x\z)`\(y\z)`)` by BCIALG_1:9
.= ((x`\z`)\((y\z)`))` by BCIALG_1:9;
then (((x\z)\(y\z))`)` = ((y`\(x\y)\z`)\(y\z)`)` by A1,A2
.= ((y`\z`\(x\y))\(y\z)`)` by BCIALG_1:7
.= (((y\z)`\(x\y))\(y\z)`)` by BCIALG_1:9
.= (((y\z)`)\((y\z)`)\(x\y))` by BCIALG_1:7
.= ((x\y)`)` by BCIALG_1:def 5
.= (x`\y`)` by BCIALG_1:9
.= ((y`)`\x)` by BCIALG_1:7
.= ((y`)`)`\x` by BCIALG_1:9
.= y`\x` by BCIALG_1:8;
hence thesis;
end;
thus (for y,z holds (((x\z)\(y\z))`)` = y`\x`) implies x` is minimal
proof
assume
A3: for y,z holds (((x\z)\(y\z))`)` = y`\x`;
now
let x1 be Element of X;
assume x1<=x`;
then
A4: x1\x`=0.X;
then (x1`\x`)\(x1`\x1)=0.X by BCIALG_1:4;
then ((((x\0.X)\(x1\0.X))`)`)\(x1`\x1)=0.X by A3;
then ((x1`\x1)`)\(((x\0.X)\(x1\0.X))`)=0.X by BCIALG_1:7;
then ((x1`\x1)`)\((x\(x1\0.X))`)=0.X by BCIALG_1:2;
then ((x1`\x1)`)\((x\x1)`)=0.X by BCIALG_1:2;
then (((x1`)`)\x1`)\((x\x1)`)=0.X by BCIALG_1:9;
then (((x1`)`)\x1`)\(x`\x1`)=0.X by BCIALG_1:9;
then (((x1`)`)\x`)`=0.X by BCIALG_1:def 3;
then (((x1`)`)`)\((x`)`)=0.X by BCIALG_1:9;
then x1`\((x`)`)=0.X by BCIALG_1:8;
then (((x`)`)`)\x1=0.X by BCIALG_1:7;
then x`\x1=0.X by BCIALG_1:8;
hence x1=x` by A4,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
0.X is maximal implies for a holds a is minimal
proof
assume
A1: 0.X is maximal;
let a;
now
let x;
assume x<=a;
then
A2: x\a=0.X;
then (a\x)`=0.X by BCIALG_1:6;
then 0.X <= a\x;
then 0.X = a\x by A1;
hence x=a by A2,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
theorem
(ex x st x is greatest) implies for a holds a is positive
proof
given x such that
A1: x is greatest;
let a;
a<=x by A1;
then a\x=0.X;
then
A2: (a\x)`=0.X by BCIALG_1:def 5;
0.X<=x by A1;
then x`=0.X;
then a`\0.X=0.X by A2,BCIALG_1:9;
then a`=0.X by BCIALG_1:2;
then 0.X<=a;
hence thesis;
end;
theorem Th28:
x\(x``) is positive Element of X
proof
(x\((x`)`))` = x`\(((x`)`)`) by BCIALG_1:9
.=x`\x` by BCIALG_1:8
.=0.X by BCIALG_1:def 5;
then 0.X<=x\((x`)`);
hence thesis by Def2;
end;
theorem
a is minimal iff a`` = a
proof
thus a is minimal implies a`` = a
proof
(a`)`\a=0.X by BCIALG_1:1;
then
A1: (a`)` <= a;
assume a is minimal;
hence thesis by A1;
end;
assume
A2: a`` = a;
now
let x;
assume x<=a;
then
A3: x\a=0.X;
a\x=x`\a` by A2,BCIALG_1:7;
then a\x=(0.X)` by A3,BCIALG_1:9;
then a\x=0.X by BCIALG_1:def 5;
hence x=a by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
theorem Th30:
a is minimal iff ex x st a=x`
proof
thus a is minimal implies ex x st a=x`
proof
assume
A1: a is minimal;
take x=a`;
x`\a=0.X by BCIALG_1:1;
then x` <= a;
hence thesis by A1;
end;
given x such that
A2: a=x`;
now
let y;
assume y<=a;
then
A3: y\a=0.X;
then a\y=y\x`\y\x by A2,BCIALG_1:7;
then a\y=y\y\x`\x by BCIALG_1:7;
then a\y=(x`)`\x by BCIALG_1:def 5;
then a\y=0.X by BCIALG_1:1;
hence a=y by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
:: p38
definition
let X,x;
attr x is nilpotent means
ex k being non zero Nat st (0.X ,x) to_power k = 0.X;
end;
definition
let X;
attr X is nilpotent means
for x being Element of X holds x is nilpotent;
end;
definition
let X,x;
assume
A1: x is nilpotent;
func ord x -> non zero Nat means
:Def8:
(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;
existence
proof
defpred P[Nat] means ex w be Nat st w=$1 & (0.X,x)to_power w =
0.X & w<>0;
ex k being non zero Nat st (0.X,x) to_power k = 0.X by A1;
then
A2: ex n being Nat st P[n];
consider k being Nat such that
A3: P[k] and
A4: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A2);
reconsider k as non zero Nat by A3;
take k;
thus thesis by A3,A4;
end;
uniqueness
proof
let n1,n2 be non zero Nat;
assume (0.X,x) to_power n1 = 0.X & ( for m being Nat st (0.X,x
) to_power m=0.X&m <> 0 holds n1 <=m)& ( 0.X,x) to_power n2 = 0.X & for m being
Nat st (0.X,x)to_power m=0.X&m <> 0 holds n2 <=m;
then n1 <= n2 & n2 <= n1;
hence thesis by XXREAL_0:1;
end;
correctness;
end;
registration
let X;
cluster 0.X -> nilpotent;
coherence
proof
(0.X,0.X) to_power 1 = 0.X by Th6;
hence thesis;
end;
end;
theorem :: P39
x is positive Element of X iff x is nilpotent & ord x=1
proof
thus x is positive Element of X implies x is nilpotent&ord x=1
proof
assume x is positive Element of X;
then 0.X<=x by Def2;
then
A1: x`=0.X;
thus
A2: x is nilpotent
proof
set k=1;
take k;
thus thesis by A1,Th2;
end;
thus ord x=1
proof
set k=1;
reconsider k as non zero Nat;
(0.X,x) to_power k=0.X & for m being Nat st (0.X,x)
to_power m=0.X &m <> 0 holds k<= m by A1,Th2,NAT_1:14;
hence thesis by A2,Def8;
end;
end;
assume x is nilpotent & ord x=1;
then (0.X,x) to_power 1 = 0.X by Def8;
then x`=0.X by Th2;
then 0.X<=x;
hence thesis by Def2;
end;
theorem
X is BCK-algebra iff for x holds ord x=1 & x is nilpotent
proof
thus X is BCK-algebra implies for x being Element of X holds ord x=1&x is
nilpotent
proof
set k=1;
assume
A1: X is BCK-algebra;
let x be Element of X;
A2: x`=0.X by A1,BCIALG_1:def 8;
then (0.X,x)to_power 1=0.X by Th2;
then
A3: x is nilpotent;
reconsider k as non zero Nat;
A4: for m being Nat st (0.X,x)to_power m=0.X&m <> 0 holds k<= m
by NAT_1:14;
(0.X,x) to_power k=0.X by A2,Th2;
hence thesis by A3,A4,Def8;
end;
assume
A5: for x holds ord x = 1&x is nilpotent;
now
let x;
ord x =1 & x is nilpotent by A5;
then (0.X,x) to_power 1 = 0.X by Def8;
hence x` =0.X by Th2;
end;
hence thesis by BCIALG_1:def 8;
end;
theorem
(0.X,x`) to_power n is minimal
proof
(0.X,x`) to_power n=((0.X,x) to_power n)` by Th9;
hence thesis by Th30;
end;
theorem
x is nilpotent implies ord x = ord (x`)
proof
assume
A1: x is nilpotent;
then consider k being non zero Nat such that
A2: (0.X,x) to_power k = 0.X;
A3: x` is nilpotent
proof
take k;
(0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
.=0.X by A2,BCIALG_1:def 5;
hence thesis;
end;
set k=ord x;
A4: now
let m be Nat;
assume that
A5: (0.X,x`)to_power m=0.X and
A6: m <> 0;
((0.X,x)to_power m)`=0.X by A5,Th9;
then (((0.X,x)to_power m)`)`=0.X by BCIALG_1:def 5;
then (0.X,x)to_power m=0.X by Th12;
hence k<=m by A1,A6,Def8;
end;
(0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
.=(0.X)` by A1,Def8
.=0.X by BCIALG_1:def 5;
hence thesis by A3,A4,Def8;
end;
begin :: Congruence and Quotient Algebras P58-65
definition
let X be BCI-algebra;
mode Congruence of X -> Equivalence_Relation of X means
:Def9:
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;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y,u,v be Element of X;
assume [x,y] in P & [u,v]in P;
then x=y & u=v by RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
:: Left Congruence
definition
let X be BCI-algebra;
mode L-congruence of X -> Equivalence_Relation of X means
:Def10:
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;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y be Element of X;
assume
A1: [x,y] in P;
let u be Element of X;
u\x=u\y by A1,RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
:: Right Congruence
definition
let X be BCI-algebra;
mode R-congruence of X -> Equivalence_Relation of X means
:Def11:
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;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y be Element of X;
assume
A1: [x,y] in P;
let u be Element of X;
x\u=y\u by A1,RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
::Ideal Congruence
definition
let X be BCI-algebra,A be Ideal of X;
mode I-congruence of X,A -> Relation of X means
:Def12:
for x,y being Element of X holds [x,y] in it iff x\y in A & y\x in A;
existence
proof
defpred PP[object,object] means
ex x,y being Element of X st x=$1&y=$2 &x\y in A
& y\x in A;
consider P being Relation of X such that
A1: for x2,y2 being object holds [x2,y2] in P iff x2 in the carrier of X&
y2 in the carrier of X&PP[x2,y2] from RELSET_1:sch 1;
take P;
let x2,y2 be Element of X;
[x2,y2] in P implies ex x1,y1 being Element of X st x1=x2&y1=y2&x1\y1
in A & y1\x1 in A by A1;
hence [x2,y2] in P implies x2\y2 in A & y2\x2 in A;
thus thesis by A1;
end;
end;
registration
let X be BCI-algebra, A be Ideal of X;
cluster -> total symmetric transitive for I-congruence of X,A;
coherence
proof
for RI being I-congruence of X,A holds RI is Equivalence_Relation of X
proof
let RI be I-congruence of X,A;
reconsider RI as Relation of X;
for x being object st x in the carrier of X holds [x,x] in RI
proof
let x be object;
assume x in the carrier of X;
then reconsider x as Element of X;
0.X in A by BCIALG_1:def 18;
then x\x in A by BCIALG_1:def 5;
hence thesis by Def12;
end;
then RI is_reflexive_in the carrier of X by RELAT_2:def 1;
then
A1: field RI = the carrier of X by ORDERS_1:13;
for x,y,z being object st [x,y] in RI&[y,z] in RI holds [x,z] in RI
proof
let x,y,z be object;
assume that
A2: [x,y] in RI and
A3: [y,z] in RI;
reconsider x,y,z as Element of X by A2,A3,ZFMISC_1:87;
(z\x\(y\x))\(z\y)=0.X by BCIALG_1:def 3;
then
A4: (z\x\(y\x))\(z\y) in A by BCIALG_1:def 18;
(x\z\(x\y))\(y\z)=0.X by BCIALG_1:1;
then
A5: (x\z\(x\y))\(y\z) in A by BCIALG_1:def 18;
y\z in A by A3,Def12;
then
A6: x\z\(x\y) in A by A5,BCIALG_1:def 18;
z\y in A by A3,Def12;
then
A7: z\x\(y\x) in A by A4,BCIALG_1:def 18;
y\x in A by A2,Def12;
then
A8: z\x in A by A7,BCIALG_1:def 18;
x\y in A by A2,Def12;
then x\z in A by A6,BCIALG_1:def 18;
hence thesis by A8,Def12;
end;
then
A9: RI is transitive by RELAT_2:31;
for x,y being object st x in the carrier of X & y in the carrier of X &
[x,y] in RI holds [y,x] in RI
proof
let x,y be object;
assume that
A10: x in the carrier of X & y in the carrier of X and
A11: [x,y] in RI;
reconsider x,y as Element of X by A10;
x\y in A & y\x in A by A11,Def12;
hence thesis by Def12;
end;
then RI is_symmetric_in the carrier of X by RELAT_2:def 3;
then RI is symmetric by A1,RELAT_2:def 11;
hence thesis by A1,A9,EQREL_1:9;
end;
hence thesis;
end;
end;
definition
let X be BCI-algebra;
func IConSet(X) -> set means
:Def13:
for A1 being set holds A1 in it iff ex I being
Ideal of X st A1 is I-congruence of X,I;
existence
proof
defpred P[object] means
ex I being Ideal of X st $1 is I-congruence of X,I;
consider Y being set such that
A1: for x being object holds x in Y iff x in bool [:the carrier of X,the
carrier of X:] & P[x] from XBOOLE_0:sch 1;
take Y;
let x be set;
thus x in Y implies ex I being Ideal of X st x is I-congruence of X,I by A1
;
given I being Ideal of X such that
A2: x is I-congruence of X,I;
thus thesis by A1,A2;
end;
uniqueness
proof
defpred P[object] means
ex I being Ideal of X st $1 is I-congruence of X,I;
let A1, A2 be set such that
A3: for x being set holds x in A1 iff ex I being Ideal of X st x is
I-congruence of X,I and
A4: for x being set holds x in A2 iff ex I being Ideal of X st x is
I-congruence of X,I;
A5: for x being object holds x in A2 iff P[x] by A4;
A6: for x being object holds x in A1 iff P[x] by A3;
A1 = A2 from XBOOLE_0:sch 2(A6,A5);
hence thesis;
end;
end;
definition
let X be BCI-algebra;
func ConSet(X) -> set equals
the set of all R where R is Congruence of X;
coherence;
func LConSet(X) -> set equals
the set of all R where R is L-congruence of X;
coherence;
func RConSet(X) -> set equals
the set of all R where R is R-congruence of X;
coherence;
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
for X,E holds Class(E,0.X) is closed Ideal of X
proof
let X,E;
A1: now
let x,y be Element of X;
assume that
A2: x\y in Class(E,0.X) and
A3: y in Class(E,0.X);
A4: [x,x] in E by EQREL_1:5;
[0.X,y] in E by A3,EQREL_1:18;
then [x\0.X,x\y] in E by A4,Def9;
then [x,x\y] in E by BCIALG_1:2;
then
A5: [x\y,x] in E by EQREL_1:6;
[0.X,x\y] in E by A2,EQREL_1:18;
then [0.X,x] in E by A5,EQREL_1:7;
hence x in Class(E,0.X)by EQREL_1:18;
end;
A6: [0.X,0.X] in E by EQREL_1:5;
then 0.X in Class(E,0.X) by EQREL_1:18;
then reconsider Rx=Class(E,0.X) as Ideal of X by A1,BCIALG_1:def 18;
now
let x be Element of Rx;
[0.X,x] in E by EQREL_1:18;
then [(0.X)`,x`] in E by A6,Def9;
then [0.X,x`] in E by BCIALG_1:def 5;
hence x` in Class(E,0.X) by EQREL_1:18;
end;
hence thesis by BCIALG_1:def 19;
end;
theorem Th36:
R is Congruence of X iff R is R-congruence of X&R is L-congruence of X
proof
A1: field R = the carrier of X by EQREL_1:9;
then
A2: R is_reflexive_in the carrier of X by RELAT_2:def 9;
thus R is Congruence of X implies R is R-congruence of X&R is L-congruence
of X
proof
assume
A3: R is Congruence of X;
thus R is R-congruence of X
proof
let x,y be Element of X;
assume
A4: [x,y] in R;
let u be Element of X;
[u,u] in R by A2,RELAT_2:def 1;
hence thesis by A3,A4,Def9;
end;
let x,y be Element of X;
assume
A5: [x,y] in R;
let u be Element of X;
[u,u] in R by A2,RELAT_2:def 1;
hence thesis by A3,A5,Def9;
end;
assume
A6: R is R-congruence of X & R is L-congruence of X;
A7: R is_transitive_in the carrier of X by A1,RELAT_2:def 16;
now
let x,y,u,v be Element of X;
assume [x,y] in R & [u,v]in R;
then [x\u,y\u] in R & [y\u,y\v] in R by A6,Def10,Def11;
hence [x\u,y\v] in R by A7,RELAT_2:def 8;
end;
hence thesis by Def9;
end;
theorem Th37:
RI is Congruence of X
proof
field RI = the carrier of X by EQREL_1:9;
then
A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;
now
let x,y,u,v be Element of X;
assume that
A2: [x,y] in RI and
A3: [u,v]in RI;
(y\u\(y\v))\(v\u)=0.X by BCIALG_1:1;
then
A4: (y\u\(y\v))\(v\u) in I by BCIALG_1:def 18;
v\u in I by A3,Def12;
then
A5: y\u\(y\v) in I by A4,BCIALG_1:def 18;
(y\v\(y\u))\(u\v)=0.X by BCIALG_1:1;
then
A6: (y\v\(y\u))\(u\v) in I by BCIALG_1:def 18;
u\v in I by A3,Def12;
then y\v\(y\u) in I by A6,BCIALG_1:def 18;
then
A7: [y\u,y\v] in RI by A5,Def12;
(x\u\(y\u))\(x\y)=0.X by BCIALG_1:def 3;
then
A8: (x\u\(y\u))\(x\y) in I by BCIALG_1:def 18;
(y\u\(x\u))\(y\x)=0.X by BCIALG_1:def 3;
then
A9: (y\u\(x\u))\(y\x) in I by BCIALG_1:def 18;
y\x in I by A2,Def12;
then
A10: y\u\(x\u) in I by A9,BCIALG_1:def 18;
x\y in I by A2,Def12;
then x\u\(y\u) in I by A8,BCIALG_1:def 18;
then [x\u,y\u] in RI by A10,Def12;
hence [x\u,y\v] in RI by A1,A7,RELAT_2:def 8;
end;
hence thesis by Def9;
end;
definition
let X be BCI-algebra, I be Ideal of X;
redefine mode I-congruence of X,I -> Congruence of X; :: redefines I-congruence (BCIALG_2, definition)
coherence by Th37;
end;
theorem Th38:
Class(RI,0.X) c= I
proof
let x be object;
assume
A1: x in Class(RI,0.X);
then consider y being object such that
A2: [y,x] in RI and
A3: y in {0.X} by RELAT_1:def 13;
reconsider x as Element of X by A1;
reconsider y as Element of X by A3,TARSKI:def 1;
y=0.X by A3,TARSKI:def 1;
then x\0.X in I by A2,Def12;
hence thesis by BCIALG_1:2;
end;
theorem
I is closed iff I = Class(RI,0.X)
proof
thus I is closed implies I = Class(RI,0.X)
proof
assume
A1: I is closed;
thus I c= Class(RI,0.X)
proof
let x be object;
assume
A2: x in I;
then reconsider x as Element of I;
A3: x\0.X in I by A2,BCIALG_1:2;
x` in I by A1;
then 0.X in {0.X} & [0.X,x] in RI by A3,Def12,TARSKI:def 1;
hence thesis by RELAT_1:def 13;
end;
thus thesis by Th38;
end;
assume
A4: I = Class(RI,0.X);
now
let x be Element of I;
ex y being object st [y,x] in RI & y in {0.X} by A4,RELAT_1:def 13;
then [0.X,x] in RI by TARSKI:def 1;
hence x` in I by Def12;
end;
hence thesis;
end;
theorem Th40:
[x,y] in E implies x\y in Class(E,0.X) & y\x in Class(E,0.X)
proof
assume
A1: [x,y] in E;
A2: field E = the carrier of X by EQREL_1:9;
then
A3: E is_reflexive_in the carrier of X by RELAT_2:def 9;
then
A4: [y,y] in E by RELAT_2:def 1;
E is_symmetric_in the carrier of X by A2,RELAT_2:def 11;
then [y,x] in E by A1,RELAT_2:def 3;
then [y\y,x\y] in E by A4,Def9;
then
A5: [0.X,x\y] in E by BCIALG_1:def 5;
[x,x] in E by A3,RELAT_2:def 1;
then [x\x,y\x] in E by A1,Def9;
then 0.X in {0.X} & [0.X,y\x] in E by BCIALG_1:def 5,TARSKI:def 1;
hence thesis by A5,RELAT_1:def 13;
end;
theorem
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
proof
let A,I be Ideal of X,IA be I-congruence of X,A,II be I-congruence of X,I;
assume
A1: Class(IA,0.X) = Class(II,0.X);
let xx,yy be object;
thus [xx,yy] in IA implies [xx,yy] in II
proof
assume
A2: [xx,yy] in IA;
then consider x,y being object such that
A3: [xx,yy]=[x,y] and
A4: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A4;
x\y in II.:{0.X} by A1,A2,A3,Th40;
then ex z being object st [z,x\y] in II & z in {0.X} by RELAT_1:def 13;
then [0.X,x\y] in II by TARSKI:def 1;
then x\y\0.X in I by Def12;
then
A5: x\y in I by BCIALG_1:2;
y\x in II.:{0.X} by A1,A2,A3,Th40;
then ex z being object st [z,y\x] in II & z in {0.X} by RELAT_1:def 13;
then [0.X,y\x] in II by TARSKI:def 1;
then y\x\0.X in I by Def12;
then y\x in I by BCIALG_1:2;
hence thesis by A3,A5,Def12;
end;
thus [xx,yy] in II implies [xx,yy] in IA
proof
assume
A6: [xx,yy] in II;
then consider x,y being object such that
A7: [xx,yy]=[x,y] and
A8: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A8;
x\y in IA.:{0.X} by A1,A6,A7,Th40;
then ex z being object st [z,x\y] in IA & z in {0.X} by RELAT_1:def 13;
then [0.X,x\y] in IA by TARSKI:def 1;
then x\y\0.X in A by Def12;
then
A9: x\y in A by BCIALG_1:2;
y\x in IA.:{0.X} by A1,A6,A7,Th40;
then ex z being object st [z,y\x] in IA & z in {0.X} by RELAT_1:def 13;
then [0.X,y\x] in IA by TARSKI:def 1;
then y\x\0.X in A by Def12;
then y\x in A by BCIALG_1:2;
hence thesis by A7,A9,Def12;
end;
end;
theorem Th42:
[x,y] in E & u in Class(E,0.X) implies [x,(y,u)to_power k] in E
proof
assume that
A1: [x,y] in E and
A2: u in Class(E,0.X);
defpred P[Nat] means [x,(y,u)to_power $1] in E;
ex z being object st [z,u] in E & z in {0.X} by A2,RELAT_1:def 13;
then
A3: [0.X,u] in E by TARSKI:def 1;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [x,(y,u) to_power k] in E;
then [x\0.X,(y,u)to_power k\u] in E by A3,Def9;
then [x,(y,u)to_power k\u] in E by BCIALG_1:2;
hence thesis by Th4;
end;
A5: P[0] by A1,Th1;
for n holds P[n] from NAT_1:sch 2(A5,A4);
hence thesis;
end;
theorem
(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
proof
assume
A1: 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;
let E,I;
assume
A2: I=Class(E,0.X);
now
let x,y be Element of X;
x\y in I & y\x in I implies[x,y] in E
proof
assume that
A3: x\y in I and
A4: y\x in I;
ex z being object st [z,y\x] in E & z in {0.X} by A2,A4,RELAT_1:def 13;
then
A5: [0.X,y\x] in E by TARSKI:def 1;
ex z being object st [z,x\y] in E & z in {0.X} by A2,A3,RELAT_1:def 13;
then
A6: [0.X,x\y] in E by TARSKI:def 1;
consider i,j,m,n being Nat such that
A7: ((x,x\y)to_power i,y\x)to_power j =((y,y\x)to_power m,x\y)
to_power n by A1;
A8: field E = the carrier of X by EQREL_1:9;
A9: E is_reflexive_in field E by RELAT_2:def 9;
then [x,x] in E by A8,RELAT_2:def 1;
then
A10: [x,(x,x\y) to_power i] in E by A2,A3,Th42;
A11: [x,((x,(x\y))to_power i,y\x)to_power j] in E
proof
defpred P[Nat] means [x,((x,(x\y))to_power i,y\x)to_power $1] in E;
A12: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [x,((x,(x\y))to_power i,y\x)to_power k] in E;
then [x\0.X,((x,(x\y))to_power i,y\x)to_power k\(y\x)] in E by A5
,Def9;
then [x,((x,(x\y))to_power i,y\x)to_power k\(y\x)] in E by BCIALG_1:2
;
hence thesis by Th4;
end;
A13: P[0] by A10,Th1;
for n holds P[n] from NAT_1:sch 2(A13,A12);
hence thesis;
end;
[y,y] in E by A8,A9,RELAT_2:def 1;
then
A14: [y,(y,y\x) to_power m] in E by A2,A4,Th42;
A15: [y,((y,(y\x))to_power m,x\y)to_power n] in E
proof
defpred P[Nat] means [y,((y,(y\x))to_power m,x\y)to_power $1] in E;
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [y,((y,(y\x))to_power m,x\y)to_power k] in E;
then [y\0.X,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by A6
,Def9;
then [y,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by BCIALG_1:2
;
hence thesis by Th4;
end;
A17: P[0] by A14,Th1;
for n holds P[n] from NAT_1:sch 2(A17,A16);
hence thesis;
end;
E is_symmetric_in field E by RELAT_2:def 11;
then
E is_transitive_in field E & [((x,(x\y))to_power i,y\x)to_power j,y
] in E by A7,A8,A15,RELAT_2:def 3,def 16;
hence thesis by A8,A11,RELAT_2:def 8;
end;
hence [x,y] in E iff x\y in I & y\x in I by A2,Th40;
end;
hence thesis by Def12;
end;
theorem
IConSet(X) c= ConSet(X)
proof
let x be object;
assume x in IConSet(X);
then ex I being Ideal of X st x is I-congruence of X,I by Def13;
hence thesis;
end;
theorem Th45:
ConSet(X) c= LConSet(X)
proof
let x be object;
assume x in ConSet(X);
then ex R being Congruence of X st x=R;
then x is L-congruence of X by Th36;
hence thesis;
end;
theorem Th46:
ConSet(X) c= RConSet(X)
proof
let x be object;
assume x in ConSet(X);
then ex R being Congruence of X st x=R;
then x is R-congruence of X by Th36;
hence thesis;
end;
theorem
ConSet(X) = LConSet(X)/\RConSet(X)
proof
ConSet(X) c= LConSet(X) & ConSet(X) c= RConSet(X) by Th45,Th46;
hence ConSet(X) c= LConSet(X)/\RConSet(X) by XBOOLE_1:19;
thus LConSet(X)/\RConSet(X) c= ConSet(X)
proof
let x be object;
assume
A1: x in LConSet(X)/\RConSet(X);
then x in RConSet(X) by XBOOLE_0:def 4;
then
A2: ex R being R-congruence of X st x=R;
x in LConSet(X) by A1,XBOOLE_0:def 4;
then ex L being L-congruence of X st x=L;
then x is Congruence of X by A2,Th36;
hence thesis;
end;
end;
theorem
(for LC holds LC is I-congruence of X,I) implies E = RI
proof
assume
A1: for LC holds LC is I-congruence of X,I;
let x1,y1 be object;
E is L-congruence of X by Th36;
then
A2: E is I-congruence of X,I by A1;
thus [x1,y1] in E implies [x1,y1] in RI
proof
assume
A3: [x1,y1] in E;
then consider x,y being object such that
A4: [x1,y1]=[x,y] and
A5: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A5;
y\x in Class(E,0.X) by A3,A4,Th40;
then ex z being object st [z,y\x] in E & z in {0.X} by RELAT_1:def 13;
then [0.X,y\x] in E by TARSKI:def 1;
then y\x\0.X in I by A2,Def12;
then
A6: y\x in I by BCIALG_1:2;
x\y in Class(E,0.X) by A3,A4,Th40;
then ex z being object st [z,x\y] in E & z in {0.X} by RELAT_1:def 13;
then [0.X,x\y] in E by TARSKI:def 1;
then x\y\0.X in I by A2,Def12;
then x\y in I by BCIALG_1:2;
hence thesis by A4,A6,Def12;
end;
thus [x1,y1] in RI implies [x1,y1] in E
proof
assume
A7: [x1,y1] in RI;
then consider x,y being object such that
A8: [x1,y1]=[x,y] and
A9: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A9;
x\y in I & y\x in I by A7,A8,Def12;
hence thesis by A2,A8,Def12;
end;
end;
theorem
(for RC holds RC is I-congruence of X,I) implies E = RI
proof
assume
A1: for RC holds RC is I-congruence of X,I;
let x1,y1 be object;
E is R-congruence of X by Th36;
then
A2: E is I-congruence of X,I by A1;
thus [x1,y1] in E implies [x1,y1] in RI
proof
assume
A3: [x1,y1] in E;
then consider x,y being object such that
A4: [x1,y1]=[x,y] and
A5: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A5;
y\x in Class(E,0.X) by A3,A4,Th40;
then ex z being object st [z,y\x] in E & z in {0.X} by RELAT_1:def 13;
then [0.X,y\x] in E by TARSKI:def 1;
then y\x\0.X in I by A2,Def12;
then
A6: y\x in I by BCIALG_1:2;
x\y in Class(E,0.X) by A3,A4,Th40;
then ex z being object st [z,x\y] in E & z in {0.X} by RELAT_1:def 13;
then [0.X,x\y] in E by TARSKI:def 1;
then x\y\0.X in I by A2,Def12;
then x\y in I by BCIALG_1:2;
hence thesis by A4,A6,Def12;
end;
thus [x1,y1] in RI implies [x1,y1] in E
proof
assume
A7: [x1,y1] in RI;
then consider x,y being object such that
A8: [x1,y1]=[x,y] and
A9: x in the carrier of X & y in the carrier of X by RELSET_1:2;
reconsider x,y as Element of X by A9;
x\y in I & y\x in I by A7,A8,Def12;
hence thesis by A2,A8,Def12;
end;
end;
theorem
Class(LC,0.X) is closed Ideal of X
proof
A1: now
let x,y be Element of X;
assume that
A2: x\y in Class(LC,0.X) and
A3: y in Class(LC,0.X);
[0.X,y] in LC by A3,EQREL_1:18;
then [x\0.X,x\y] in LC by Def10;
then [x,x\y] in LC by BCIALG_1:2;
then
A4: [x\y,x] in LC by EQREL_1:6;
[0.X,x\y] in LC by A2,EQREL_1:18;
then [0.X,x] in LC by A4,EQREL_1:7;
hence x in Class(LC,0.X)by EQREL_1:18;
end;
[0.X,0.X] in LC by EQREL_1:5;
then 0.X in Class(LC,0.X) by EQREL_1:18;
then reconsider Rx=Class(LC,0.X) as Ideal of X by A1,BCIALG_1:def 18;
now
let x be Element of Rx;
[0.X,x] in LC by EQREL_1:18;
then [(0.X)`,x`] in LC by Def10;
then [0.X,x`] in LC by BCIALG_1:def 5;
hence x` in Class(LC,0.X) by EQREL_1:18;
end;
hence thesis by BCIALG_1:def 19;
end;
:: 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;
coherence
proof
Class(E,0.X) in Class E by EQREL_1:def 3;
hence thesis;
end;
end;
definition
let X,E;
func EqClaOp E -> BinOp of Class E means
:Def17:
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)
;
existence
proof
defpred P[Element of Class E,Element of Class E,set] means for x,y st $1 =
Class(E,x) & $2 = Class(E,y) holds $3 = Class(E,x\y);
A1: for W1,W2 being Element of Class E ex V being Element of Class E st P[
W1,W2,V]
proof
let W1,W2 be Element of Class E;
consider x1 being object such that
A2: x1 in the carrier of X and
A3: W1 = Class(E,x1) by EQREL_1:def 3;
consider y1 being object such that
A4: y1 in the carrier of X and
A5: W2 = Class(E,y1) by EQREL_1:def 3;
reconsider x1,y1 as Element of X by A2,A4;
reconsider C = Class(E,x1\y1) as Element of Class E by EQREL_1:def 3;
take C;
now
let x,y;
assume that
A6: W1=Class(E,x) and
A7: W2=Class(E,y);
y in Class(E,y1) by A5,A7,EQREL_1:23;
then
A8: [y1,y] in E by EQREL_1:18;
x in Class(E,x1) by A3,A6,EQREL_1:23;
then [x1,x] in E by EQREL_1:18;
then [x1\y1,x\y] in E by A8,Def9;
then x\y in Class(E,x1\y1) by EQREL_1:18;
hence C = Class(E,x\y) by EQREL_1:23;
end;
hence thesis;
end;
thus ex B being BinOp of Class E st for W1,W2 being Element of Class E
holds P[W1,W2,B.(W1,W2)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof
let o1,o2 be BinOp of Class E;
assume
A9: for W1,W2 being Element of Class E for x,y st W1=Class(E,x)&W2=
Class(E,y)holds o1.(W1,W2)=Class(E,x\y);
assume
A10: for W1,W2 being Element of Class E for x,y st W1=Class(E,x)&W2=
Class(E,y)holds o2.(W1,W2)=Class(E,x\y);
now
let W1,W2 be Element of Class(E);
consider x being object such that
A11: x in the carrier of X and
A12: W1 = Class(E,x) by EQREL_1:def 3;
consider y being object such that
A13: y in the carrier of X and
A14: W2 = Class(E,y) by EQREL_1:def 3;
reconsider x,y as Element of X by A11,A13;
o1.(W1,W2)=Class(E,x\y) by A9,A12,A14;
hence o1.(W1,W2) = o2.(W1,W2) by A10,A12,A14;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let X,E;
func zeroEqC(E) -> Element of Class E equals
Class(E,0.X);
coherence by EQREL_1:def 3;
end;
::Quotient Algebras
definition
let X,E;
func X./.E -> BCIStr_0 equals
BCIStr_0(#Class E,EqClaOp E,zeroEqC(E)#);
coherence;
end;
registration
let X;
let E be Congruence of X;
cluster X./.E -> non empty;
coherence;
end;
reserve W1,W2 for Element of Class E;
definition
let X,E,W1,W2;
func W1\W2 -> Element of Class E equals
(EqClaOp E).(W1,W2);
coherence;
end;
theorem Th51:
X./.RI is BCI-algebra
proof
reconsider IT = X./.RI as non empty BCIStr_0;
A1: now
let w1,w2,w3 be Element of IT;
w1 in the carrier of IT;
then consider x1 being object such that
A2: x1 in the carrier of X and
A3: w1 = Class(RI,x1) by EQREL_1:def 3;
w3 in the carrier of IT;
then consider z1 being object such that
A4: z1 in the carrier of X and
A5: w3 = Class(RI,z1) by EQREL_1:def 3;
w2 in the carrier of IT;
then consider y1 being object such that
A6: y1 in the carrier of X and
A7: w2 = Class(RI,y1) by EQREL_1:def 3;
reconsider x1,y1,z1 as Element of X by A2,A6,A4;
A8: w3\w2=Class(RI,z1\y1) by A7,A5,Def17;
w1\w2=Class(RI,x1\y1) by A3,A7,Def17;
then
A9: (w1\w2)\(w3\w2)=Class(RI,(x1\y1)\(z1\y1)) by A8,Def17;
w1\w3=Class(RI,x1\z1) by A3,A5,Def17;
then (w1\w2)\(w3\w2)\(w1\w3)=Class(RI,(x1\y1)\(z1\y1)\(x1\z1)) by A9,Def17;
hence ((w1\w2)\(w3\w2))\(w1\w3)=0.IT by BCIALG_1:def 3;
end;
A10: now
let w1,w2,w3 be Element of IT;
w1 in the carrier of IT;
then consider x1 being object such that
A11: x1 in the carrier of X and
A12: w1 = Class(RI,x1) by EQREL_1:def 3;
w2 in the carrier of IT;
then consider y1 being object such that
A13: y1 in the carrier of X and
A14: w2 = Class(RI,y1) by EQREL_1:def 3;
w3 in the carrier of IT;
then consider z1 being object such that
A15: z1 in the carrier of X and
A16: w3 = Class(RI,z1) by EQREL_1:def 3;
reconsider x1,y1,z1 as Element of X by A11,A13,A15;
w1\w3=Class(RI,x1\z1) by A12,A16,Def17;
then
A17: (w1\w3)\w2=Class(RI,x1\z1\y1) by A14,Def17;
w1\w2=Class(RI,x1\y1) by A12,A14,Def17;
then (w1\w2)\w3=Class(RI,(x1\y1)\z1) by A16,Def17;
then ((w1\w2)\w3)\((w1\w3)\w2)=Class(RI,(x1\y1)\z1\(x1\z1\y1)) by A17,Def17
;
hence ((w1\w2)\w3)\((w1\w3)\w2)=0.IT by BCIALG_1:def 4;
end;
A18: now
let w1,w2 be Element of IT;
assume that
A19: w1\w2=0.IT and
A20: w2\w1=0.IT;
w1 in the carrier of IT;
then consider x1 being object such that
A21: x1 in the carrier of X and
A22: w1 = Class(RI,x1) by EQREL_1:def 3;
w2 in the carrier of IT;
then consider y1 being object such that
A23: y1 in the carrier of X and
A24: w2 = Class(RI,y1) by EQREL_1:def 3;
reconsider x1,y1 as Element of X by A21,A23;
w2\w1=Class(RI,y1\x1) by A22,A24,Def17;
then 0.X in Class(RI,y1\x1) by A20,EQREL_1:23;
then [y1\x1,0.X] in RI by EQREL_1:18;
then y1\x1\0.X in I by Def12;
then
A25: y1\x1 in I by BCIALG_1:2;
w1\w2=Class(RI,x1\y1) by A22,A24,Def17;
then 0.X in Class(RI,x1\y1) by A19,EQREL_1:23;
then [x1\y1,0.X] in RI by EQREL_1:18;
then x1\y1\0.X in I by Def12;
then x1\y1 in I by BCIALG_1:2;
then [x1,y1] in RI by A25,Def12;
hence w1=w2 by A22,A24,EQREL_1:35;
end;
now
let w1 be Element of IT;
w1 in the carrier of IT;
then consider x1 being object such that
A26: x1 in the carrier of X and
A27: w1 = Class(RI,x1) by EQREL_1:def 3;
reconsider x1 as Element of X by A26;
w1\w1=Class(RI,x1\x1) by A27,Def17;
hence w1\w1 = 0.IT by BCIALG_1:def 5;
end;
hence thesis by A1,A10,A18,BCIALG_1:def 3,def 4,def 5,def 7;
end;
registration
let X,I,RI;
cluster X./.RI -> strict being_B being_C being_I being_BCI-4;
coherence by Th51;
end;
theorem
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
proof
let X,I;
assume
A1: I = BCK-part(X);
let RI be I-congruence of X,I;
set IT = X./.RI;
for w1 being Element of IT holds (w1`)` = w1
proof
let w1 be Element of IT;
w1 in the carrier of IT;
then consider x1 being object such that
A2: x1 in the carrier of X and
A3: w1 = Class(RI,x1) by EQREL_1:def 3;
reconsider x1 as Element of X by A2;
w1`= Class(RI,x1`) by A3,Def17;
then
A4: w1``=Class(RI,x1``) by Def17;
x1\((x1`)`) is positive Element of X by Th28;
then 0.X <= x1\(x1``) by Def2;
then
A5: x1\(x1``) in I by A1;
0.X in I by BCIALG_1:def 18;
then (x1`)`\x1 in I by BCIALG_1:1;
then [x1``,x1] in RI by A5,Def12;
hence thesis by A3,A4,EQREL_1:35;
end;
hence thesis by BCIALG_1:54;
end;