:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies BCIALG_1, BOOLE, RLVECT_1, FUNCT_1, RELAT_1, SUBSET_1, BCIALG_2,
BCIALG_6, BINOP_1, FUNCOP_1, UNIALG_2, REALSET1, TARSKI, CHORD, EQREL_1,
FILTER_2, PRE_TOPC, COHSP_1, WELLORD1, ALG_1, GROUP_6, PROB_1, SGRAPH1,
MOD_4, ARYTM, WAYBEL15, ABSVALUE, GROUP_1, ARYTM_1, ARYTM_3, INT_2,
NAT_1, INT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, BCIALG_1, FUNCOP_1,
NAT_1, NUMBERS, XCMPLX_0, INT_2, XXREAL_0, BINOP_2, BCIALG_3, SUPINF_1,
SEQ_1, NAT_D, INT_1, BCIALG_2, EQREL_1;
constructors BINOP_1, FINSOP_1, REALSET1, BCIALG_1, BCIALG_2, FUNCOP_1, NAT_1,
XXREAL_0, REAL_1, INT_2, BINOP_2, FINSEQOP, BCIALG_3, SUPINF_1, INT_1,
SEQ_1, NAT_D;
registrations XBOOLE_0, RELSET_1, REALSET1, STRUCT_0, BCIALG_1, BCIALG_2,
FUNCT_2, PARTFUN1, RELAT_1, NAT_1, XREAL_0, ORDINAL1, XXREAL_0, BCIALG_3,
SUPINF_1, INT_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, REALSET1, BINOP_1, STRUCT_0, BCIALG_1, FUNCT_1, BCIALG_2,
XBOOLE_0, NAT_1, INT_1, BCIALG_3;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, BINOP_1, ZFMISC_1, RELAT_1,
XBOOLE_0, XBOOLE_1, BCIALG_1, GROUP_6, BCIALG_2, EQREL_1, RELSET_1,
ABSVALUE, ORDINAL1, NAT_D, XREAL_1, INT_1, XCMPLX_1, INT_2, NAT_1,
NEWTON, XXREAL_0;
schemes BINOP_1, FUNCT_2, FUNCT_1, NAT_1, INT_1;
begin :: The power of an Element of BCI-algebra
reserve X,Y for BCI-algebra;
reserve n for Element of NAT;
reserve i,j for Integer;
definition
let D be set, f be Function of NAT,D;
let n be Nat;
redefine func f.n -> Element of D;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 13;
f.n is Element of D;
hence thesis;
end;
end;
definition let G be non empty BCIStr_0;
func BCI-power G -> Function of [:the carrier of G,NAT:],the carrier of G
means
:Def1: for x being Element of G
holds it.(x,0)=0.G & for n holds it.(x,n + 1) = x\(it.(x,n))`;
existence
proof
defpred P[set,set] means
ex f being Function of NAT, the carrier of G,
x being Element of G st $1 = x & f = $2 &
f.0 = 0.G & for n holds f.(n + 1) = x\(f.n)`;
A1: for x1,y1,y2 be set st x1 in the carrier of G & P[x1,y1] & P[x1,y2]
holds y1 = y2
proof let x1,y1,y2 be set;
assume x1 in the carrier of G;
given g1 being Function of NAT, the carrier of G,
h being Element of G such that
A2: x1 = h & g1 = y1 & g1.0 = 0.G &for n holds g1.(n + 1) = h\(g1.n)`;
given g2 being Function of NAT, the carrier of G,
m being Element of G such that
A6: x1 = m & g2 = y2 & g2.0 = 0.G &
for n holds g2.(n + 1) = m\(g2.n)`;
defpred P[Element of NAT] means g1.$1 = g2.$1;
A10: P[0] by A2,A6;
A11: now let n;
assume P[n];
then g1.(n + 1) = m\(g2.n)` by A2,A6
.= g2.(n + 1) by A6;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 1(A10,A11);
hence thesis by A2,A6,FUNCT_2:113;
end;
A12: for x be set st x in the carrier of G ex y be set st P[x,y]
proof let x be set;
assume x in the carrier of G;
then reconsider b = x as Element of G;
deffunc Ff(Nat,Element of G) = b\($2)`;
consider g0 being Function of NAT,the carrier of G such that
A13: g0.0 = 0.G &
for n being Nat holds g0.(n+1) = Ff(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.G by A13;
let n;
thus g0.(n + 1) = b\(g0.n)` by A13;
end;
consider f being Function such that
A15:dom f = the carrier of G &
for x be set st x in the carrier of G holds P[x,f.x]
from FUNCT_1:sch 2(A1,A12);
defpred P[Element of G,Element of NAT,set] means
ex g0 being Function of NAT, the carrier of G st g0 = f.$1 & $3 = g0.$2;
A16: for a being Element of G, n being Element of NAT
ex b being Element of G st P[a,n,b]
proof
let a be Element of G, n be Element of NAT;
consider g0 being Function of NAT, the carrier of G,
h being Element of G such that a = h and
A17: g0 = f.a and g0.0 = 0.G &
for n holds g0.(n + 1) = h\(g0.n)` by A15;
take g0.n, g0;
thus thesis by A17;
end;
consider F being Function of [:the carrier of G,NAT:], the carrier of G
such that
A18: for a being Element of G,
n being Element of NAT holds P[a,n,F.(a,n)] from BINOP_1:sch 3(A16);
take F;
let h be Element of G;
A19: ex g1 being Function of NAT, the carrier of G
st g1 = f.h & F.(h,0) = g1.0 by A18;
ex g2 being Function of NAT, the carrier of G,b being Element of G
st h = b & g2 = f.h & g2.0 = 0.G &for n holds g2.(n + 1) = b\(g2.n)` by A15;
hence F.(h,0) = 0.G by A19;
let n;
A20: ex g0 being Function of NAT, the carrier of G
st g0 = f.h & F.(h,n) = g0.n by A18;
A21: ex g1 being Function of NAT, the carrier of G
st g1 = f.h & F.(h,n + 1) = g1.(n + 1) by A18;
consider g2 being Function of NAT, the carrier of G,
b being Element of G such that
A22: h = b & g2 = f.h & g2.0 = 0.G and
A23: for n holds g2.(n + 1) = b\(g2.n)` by A15;
thus F.(h,n + 1) = h\(F.(h,n))` by A20,A21,A22,A23;
end;
uniqueness
proof let f,g be Function of [:the carrier of G,NAT:], the carrier of G;
assume that
A24: for h being Element of G holds f.(h,0) = 0.G &
for n holds f.(h,n + 1) = h\(f.(h,n))` and
A25: for h being Element of G holds g.(h,0) = 0.G &
for n holds g.(h,n + 1) = h\(g.(h,n))`;
now let h be Element of G, n be Element of NAT;
defpred P[Element of NAT] means f.[h,$1] = g.[h,$1];
f.[h,0] = f.(h,0)
.= 0.G by A24
.= g.(h,0) by A25
.= g.[h,0];
then A26: P[0];
A27: now let n;
assume A28: P[n];
A29: f.[h,n] = f.(h,n) & g.[h,n] = g.(h,n);
f.[h,n + 1] = f.(h,n + 1)
.= h\(f.(h,n))` by A24
.= g.(h,n + 1) by A25,A28,A29
.= g.[h,n + 1];
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 1(A26,A27);
hence f.(h,n) = g.(h,n);
end;
hence thesis by BINOP_1:2;
end;
end;
reserve x,y for Element of X;
reserve a,b for Element of AtomSet(X);
reserve m,n for Nat;
reserve i,j for Integer;
definition let X,i,x;
func x |^ i -> Element of X equals
:Def2: BCI-power(X).(x,abs(i)) if 0 <= i otherwise
(BCI-power(X).(x`,abs(i)));
correctness;
end;
definition let X,n,x;
redefine func x |^ n equals
BCI-power(X).(x,n);
compatibility
proof let g be Element of X;
abs n = n by ABSVALUE:def 1;
hence thesis by Def2;
end;
end;
theorem Th0:
a\(x\b) = b\(x\a)
proof
A1: b in AtomSet(X);
consider y1 being Element of X such that
A3: b=y1&y1 is atom by A1;
a\(x\b)<=(b\(x\a)) by BCIALG_1:26;
then A5:a\(x\b)\(b\(x\a)) = 0.X by BCIALG_1:def 11;
(x\(x\b))\b=0.X by BCIALG_1:1;
then (b\(x\a))\(a\(x\b))= ((x\(x\b))\(x\a))\(a\(x\b)) by A3,BCIALG_1:def 14;
then (b\(x\a))\(a\(x\b))= ((x\(x\a))\(x\b))\(a\(x\b))by BCIALG_1:7;
then (b\(x\a))\(a\(x\b))= ((x\(x\a))\(x\b))\(a\(x\b))\0.X by BCIALG_1:2;
then (b\(x\a))\(a\(x\b))
=((x\(x\a))\(x\b))\(a\(x\b))\((x\(x\a))\a) by BCIALG_1:1;
then b\(x\a)\(a\(x\b))=0.X by BCIALG_1:def 3;
hence thesis by A5,BCIALG_1:def 7;
end;
theorem Th1:
x |^ (n+1) = x\(x |^ n )`
proof
reconsider n as Element of NAT by ORDINAL1:def 13;
x |^ (n + 1) = x\(x |^ n )` by Def1;
hence thesis;
end;
theorem Th2:
x |^ 0 = 0.X by Def1;
theorem Th3:
x |^ 1 = x
proof
x |^ 1 = x|^(0+1) .= x\(x|^0)` by Def1
.=x\(0.X)` by Def1
.=x\0.X by BCIALG_1:def 5;
hence thesis by BCIALG_1:2;
end;
theorem Th4:
x |^ -1 = x`
proof
x |^ (-1)= BCI-power(X).(x`,abs(-1)) by Def2;
then x |^ (-1)= BCI-power(X).(x`,-(-1)) by ABSVALUE:def 1;
then x |^ (-1)= x`|^ 1;
hence thesis by Th3;
end;
theorem
x |^ 2 = x\x`
proof
x |^ 2 = x|^(1+1) .= x\(x|^1)` by Def1;
hence thesis by Th3;
end;
theorem Th6:
0.X |^ n = 0.X
proof
defpred P[Nat] means (0.X) |^ $1 = 0.X;
A1: P[0] by Def1;
A2: now
let n;
assume P[n];
then (0.X) |^ (n + 1) = ((0.X)`)` by Th1
.=(0.X)` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 5;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
::P18-theorem 1.4.2(1-4)
theorem
(a |^ (-1))|^ (-1) = a
proof
(a |^ -1)|^ -1 = (a`)|^ -1 by Th4
.= a`` by Th4;
hence thesis by BCIALG_1:29;
end;
theorem
x |^(-n) =(x``)|^(-n)
proof
defpred P[Nat] means x |^(-$1) =(x``)|^(-$1);
x |^(0) =0.X by Def1 .=(x``)|^(0) by Def1;
then A1: P[0];
A3: now
let n;
assume P[n];
set m=-(n+1);
-(-(n+1))>0;
then B3:m<0;
then x |^ m = BCI-power(X).(x`,abs(m)) by Def2
.= BCI-power(X).((x``)`,abs(m)) by BCIALG_1:8
.= (x``) |^(-(n+1)) by Def2,B3;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th9:
a` |^ n = a |^ -n
proof
per cases;
suppose A1:n=0;
hence a` |^ n = 0.X by Def1 .= a|^ -n by A1,Th2;
end;
suppose A3:n>0;
set m=-n;
-(-n)>0 by A3;
then A5:m<0;
then a|^m = BCI-power(X).(a`,abs(m)) by Def2
.=BCI-power(X).(a`,-(-n)) by A5,ABSVALUE:def 1;
hence thesis;
end;
end;
theorem
x in BCK-part(X) & n>=1 implies x|^n = x
proof
assume A1:x in BCK-part(X)& n>=1;
then consider y being Element of X such that
A3:y=x &0.X<=y;
defpred P[Nat] means x |^ $1 = x;
B1: P[1] by Th3;
B3: now
let n;
assume n>=1;
assume B7:P[n];
x |^ (n+1) =x\x` by B7,Th1
.=x\0.X by A3,BCIALG_1:def 11
.= x by BCIALG_1:2;
hence P[n+1];
end;
for n st n>=1 holds P[n] from NAT_1:sch 8(B1,B3);
hence thesis by A1;
end;
theorem
x in BCK-part(X) implies x|^ (-n) = 0.X
proof
assume x in BCK-part(X);
then consider y being Element of X such that
C3:y=x &0.X<=y;
defpred P[Nat] means x |^ (-$1) = 0.X;
A1: P[0] by Def1;
A3: now
let n;
assume B1:P[n];
-(-(n+1))>0;
then B3:-(n+1)<0;
per cases;
suppose -n=0;
then x |^(-(n+1)) =x` by Th4
.=0.X by C3,BCIALG_1:def 11;
hence P[n+1];
end;
suppose BB:-n<0;
then BCI-power(X).(x`,abs(-n)) = 0.X by Def2,B1;
then BCI-power(X).(x`,--n) = 0.X by BB,ABSVALUE:def 1;
then x`\(x` |^ n )` =(x\0.X)` by BCIALG_1:9
.=x` by BCIALG_1:2;
then x`\(x` |^ n )`= 0.X by C3,BCIALG_1:def 11;
then 0.X = x`|^ (n+1) by Th1
.=BCI-power(X).(x`,-(-(n+1)))
.=BCI-power(X).(x`,abs(-(n+1))) by B3,ABSVALUE:def 1
.=x |^ (-(n+1)) by Def2,B3;
hence P[n+1];
end;
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
::P19 theorem 1.4.3
theorem Th12:
a|^i in AtomSet(X)
proof
defpred P[Integer] means a |^ $1 in AtomSet(X);
0.X in AtomSet(X);
then A3: P[0] by Def1;
per cases;
suppose A4:i>=0;
A5:for i2 be Integer st i2>=0 holds P[i2] implies P[i2 + 1]
proof
let i2 be Integer;
assume B1:i2>=0;
assume B3:P[i2];
reconsider j=i2 as Element of NAT by B1,INT_1:16;
(a|^(j+1))``=(a\(a |^ j )`)`` by Def1;
then (a|^(j+1))``=(a`\(a |^ j )``)` by BCIALG_1:9;
then (a|^(j+1))``=a``\(a |^ j)``` by BCIALG_1:9;
then (a|^(j+1))``=a\(a |^ j)``` by BCIALG_1:29;
then (a|^(j+1))``=a\(a |^ j)` by B3,BCIALG_1:29;
then (a|^(j+1))``=a |^ (j+1) by Def1;
hence P[i2 + 1] by BCIALG_1:29;
end;
for i st i>=0 holds P[i] from INT_1:sch 2(A3,A5);
hence thesis by A4;
end;
suppose A6:i<=0;
A7:for i2 be Integer st i2<=0 holds P[i2] implies P[i2 - 1]
proof
let i2 be Integer;
assume B1:i2<=0;
assume B3:P[i2];
per cases by B1;
suppose D1:i2=0;
(a`)``=a` by BCIALG_1:8;
then a` in AtomSet(X) by BCIALG_1:29;
hence P[i2-1] by D1,Th4;
end;
suppose D1:i2<0;
set j=i2;
reconsider m=-j as Element of NAT by D1,INT_1:16;
a|^(j-1)=(BCI-power(X).(a`,abs(j-1))) by Def2,D1;
then a|^(j-1)=(BCI-power(X).(a`,-(j-1))) by D1,ABSVALUE:def 1;
then a|^(j-1)=a`|^(m+1);
then a|^(j-1)=a`\(a` |^ m )` by Def1;
then a|^(j-1)=a`\(a |^ --j )` by Th9;
then (a|^(j-1))``=(a``\(a |^ j )``)` by BCIALG_1:9;
then (a|^(j-1))``=(a\(a |^ j )``)` by BCIALG_1:29;
then (a|^(j-1))``=(a\(a |^ j ))` by B3,BCIALG_1:29;
then (a|^(j-1))``=a`\(a |^ -m )` by BCIALG_1:9;
then (a|^(j-1))``=a`\(a` |^ m )` by Th9;
then (a|^(j-1))``=a` |^ (m+1) by Def1;
then (a|^(j-1))``=(BCI-power(X).(a`,-(j-1)));
then (a|^(j-1))``=(BCI-power(X).(a`,abs(j-1))) by D1,ABSVALUE:def 1;
then (a|^(j-1))``=a|^(j-1) by Def2,D1;
hence P[i2-1] by BCIALG_1:29;
end;
end;
for i st i<=0 holds P[i] from INT_1:sch 3(A3,A7);
hence thesis by A6;
end;
end;
theorem Th13:
(a|^(n+1))` = (a|^n)`\a
proof
A1:a|^n in AtomSet(X) by Th12;
(a|^(n+1))` =( a\(a |^ n )`)` by Th1
.=a`\(a |^ n )`` by BCIALG_1:9
.=a`\(a |^ n ) by A1,BCIALG_1:29;
hence thesis by BCIALG_1:7;
end;
::P20 Th1.4.5(1)--(4)
Th14: a|^(n+m) = a|^m\(a|^n)`
proof
defpred P[Nat] means a|^(n+$1) = a|^$1\(a|^n)`;
reconsider p = a|^n as Element of AtomSet(X) by Th12;
a|^0\(a|^n)` = (a|^n)`` by Def1 .=p by BCIALG_1:29;
then A1: P[0];
A3: now
let m;
assume B1:P[m];
reconsider q = a|^(m+1) as Element of AtomSet(X) by Th12;
a|^(n+(m+1))=a|^(n+m+1)
.=a\(a|^m\(a|^n)`)` by B1,Th1
.=a\((a|^m)`\((a|^n)``)) by BCIALG_1:9
.=a\((a|^m)`\p) by BCIALG_1:29
.=p\((a|^m)`\a) by Th0
.=a|^n\(a|^(m+1))` by Th13
.=q\(p)` by Th0
.= a|^(m+1)\(a|^n)`;
hence P[m+1];
end;
for m holds P[m] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
Th15:
(a|^m)|^n = a|^(m*n)
proof
defpred P[Nat] means (a|^m)|^$1 = a|^(m*$1);
(a|^m)|^0 =0.X by Def1;
then A1: P[0] by Def1;
A3: now
let n;
assume B1:P[n];
(a|^m)|^(n+1) =(a|^m)\((a|^(m*n)))` by B1,Th1
.=(a|^(m+m*n)) by Th14
.= a|^(m*(n+1));
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th16:
(a\b)|^n = a|^n\(b|^n)
proof
defpred P[Nat] means (a\b)|^$1 = a|^$1\(b|^$1);
(a\b)|^0=0.X by Def1 .=(0.X)` by BCIALG_1:def 5
.=a|^0\0.X by Def1;
then A1: P[0] by Def1;
A3: now
let n;
assume B1:P[n];
B2:(b|^n)` in AtomSet(X)&a|^(n+1) in AtomSet(X) by Th12,BCIALG_1:34;
(a\b)|^(n+1) = (a\b)\(a|^n\(b|^n))` by B1,Th1
.= (a\(a|^n\(b|^n))`)\b by BCIALG_1:7
.= (a\((a|^n)`\(b|^n)`))\b by BCIALG_1:9
.= ((b|^n)`\((a|^n)`\a))\b by B2,Th0
.= ((b|^n)`\b)\((a|^n)`\a) by BCIALG_1:7
.= (b|^(n+1))`\((a|^n)`\a) by Th13
.= (b|^(n+1))`\(a|^(n+1))` by Th13
.= ((b|^(n+1))\(a|^(n+1)))` by BCIALG_1:9
.= a|^(n+1)\(b|^(n+1)) by B2,BCIALG_1:30;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem
(a\b)|^(-n) = a|^(-n)\(b|^(-n))
proof
B3:(a\b)|^(-n)=((a\b)`)|^n by Th9
.=(a`\b`)|^n by BCIALG_1:9;
set c = a`, d = b`;
reconsider c,d as Element of AtomSet(X) by BCIALG_1:34;
c|^n = a|^(-n) & d|^n = b |^ (-n) by Th9;
hence (a\b)|^(-n) = a|^(-n)\(b|^(-n)) by Th16,B3;
end;
theorem Th17:
a`|^n = (a|^n)`
proof
defpred P[Nat] means a`|^$1 = (a|^$1)`;
a`|^0 =0.X by Def1 .=(0.X)` by BCIALG_1:def 5;
then A1: P[0] by Def1;
A3: now
let n;
assume P[n];
0.X in AtomSet(X);then
a`|^(n+1) =(0.X)|^(n+1)\(a|^(n+1)) by Th16
.= (a|^(n+1))` by Th6;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th17b:
x`|^n = (x|^n)`
proof
defpred P[Nat] means x`|^$1 = (x|^$1)`;
x`|^0 = 0.X by Def1 .=(0.X)` by BCIALG_1:def 5;
then A1: P[0] by Def1;
A3: now let n;
assume B1:P[n];
x`|^(n+1) =x`\((x|^ n)`)` by B1,Th1
.=(x\(x|^ n )`)` by BCIALG_1:9
.= (x|^(n+1))` by Th1;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem
a`|^(-n) = (a|^(-n))`
proof
reconsider c =a` as Element of AtomSet(X) by BCIALG_1:34;
c|^(-n) = c`|^n by Th9 .= (c|^n)` by Th17 .= (a|^(-n))` by Th9;
hence (a`)|^(-n) = (a|^(-n))`;
end;
theorem Th18:
a=(x``)|^n implies x|^n in BranchV(a)
proof
defpred P[Nat] means for a st a=(x``)|^$1 holds x|^$1 in BranchV(a);
x|^0 = 0.X by Def1;
then 0.X \ x|^0 = 0.X by BCIALG_1:2;
then 0.X <= x|^0 by BCIALG_1:def 11;
then (x``)|^0 <= x|^0 by Def1;
then A1: P[0];
A3: now
let n;
assume B1:P[n];
now let a;
assume a=(x``)|^(n+1);
set b=(x``)|^n;
b in AtomSet(X)
proof
x`` in AtomSet(X) by BCIALG_1:34;
hence thesis by Th12;
end;
then reconsider b as Element of AtomSet(X);
B5:0.X in AtomSet(X);
x|^n in BranchV(b) by B1;
then (x|^n)` =((x``)|^n)` by B5,BCIALG_1:37;
then B5:x|^(n+1) =x\((x``)|^n)` by Th1;
((x``\(((x``)|^n)`))\((x)\(((x``)|^n)` )))\(x``\x)=0.X by BCIALG_1:def 3;
then (x``|^(n+1))\x|^(n+1)\(x``\x)=0.X by B5,Th1;
then (x``|^(n+1))\x|^(n+1)\0.X=0.X by BCIALG_1:1;
then (x``|^(n+1))\x|^(n+1)=0.X by BCIALG_1:2;
then x``|^(n+1) <= x|^(n+1) by BCIALG_1:def 11;
hence a=(x``)|^(n+1) implies x|^(n+1) in BranchV(a);
end;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th19:
(x|^n)` = ((x``)|^n)`
proof
set b=(x``)|^n;
x`` in AtomSet(X) by BCIALG_1:34;
then reconsider b as Element of AtomSet(X) by Th12;
B5:0.X in AtomSet(X);
x|^n in BranchV(b) by Th18;
hence (x|^n)` = ((x``)|^n)` by B5,BCIALG_1:37;
end;
Lm20:
i>0&j>0 implies a|^i \ a|^j = a|^(i-j)
proof
assume A1:i>0&j>0;
per cases by XXREAL_0:1;
suppose A1:i=j;
then a|^i \ a|^j = 0.X by BCIALG_1:def 5;
then a|^i \ a|^j = a|^0 by Def1;
hence thesis by A1;
end;
suppose B0:i>j;
set m=i-j;
m>0 by B0,XREAL_1:52;
then reconsider j,m as Element of NAT by A1,INT_1:16;
a|^m in AtomSet(X) by Th12;
then B5:(a|^m)``=a|^m by BCIALG_1:29;
a|^i = a|^((i-j)+j) .=a|^j\(a|^m)` by Th14;
then a|^i\a|^j=a|^j\a|^j\(a|^m)` by BCIALG_1:7;
hence thesis by B5,BCIALG_1:def 5;
end;
suppose C1:i0 by C1,XREAL_1:52;
then reconsider i,m as Element of NAT by A1,INT_1:16;
C7:0.X in AtomSet(X);
a|^j = a|^(i+(j-i)) .=a|^i\(a|^m)` by Th14;
then a|^i\a|^j = (a|^m)` by C7,BCIALG_1:32;
then a|^i\a|^j = a`|^m by Th17;
then a|^i\a|^j = a|^(-m) by Th9;
hence thesis;
end;
end;
theorem Th20:
a|^i \ a|^j = a|^(i-j)
proof
per cases;
suppose A5:i>0;
per cases;
suppose j>0;
hence thesis by Lm20,A5;
end;
suppose C1:j=0;
a|^(i-0) = a|^i\0.X by BCIALG_1:2
.=a|^i \ a|^0 by Def1;
hence thesis by C1;
end;
suppose C3:j<0;
set m=-j;
reconsider i,m as Element of NAT by A5,C3,INT_1:16;
a|^j = BCI-power(X).(a`,abs(j)) by Def2,C3
.= a`|^m by C3,ABSVALUE:def 1
.= (a|^m)` by Th17;
then a|^i \ a|^j = a|^(i+m) by Th14;
hence thesis;
end;
end;
suppose A9:i=0;
per cases;
suppose j>=0;
then reconsider j as Element of NAT by INT_1:16;
a|^0 \ a|^j = (a|^j)` by Def1
.= a`|^j by Th17 .=a|^ -j by Th9;
hence thesis by A9;
end;
suppose C3:j<0;
set m=-j;
reconsider m as Element of NAT by C3,INT_1:16;
a|^j = BCI-power(X).(a`,abs(j)) by Def2,C3
.= a`|^m by C3,ABSVALUE:def 1
.= (a|^m)` by Th17;
then a|^0 \ a|^j = a|^(0+m) by Th14;
hence thesis by A9;
end;
end;
suppose E1:i<0;
then E2:-i>0 by XREAL_1:60;
reconsider m=-i as Element of NAT by E1,INT_1:16;
per cases;
suppose E3:j>=0;
set n=-(i-j);
reconsider n,j as Element of NAT by E1,E3,INT_1:16;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
E9:a|^(i-j) = BCI-power(X).(a`,abs(i-j)) by Def2,E1
.= a`|^n by E1,ABSVALUE:def 1
.= b|^(j+m)
.= a`|^m\(a`|^j)` by Th14;
E11:a|^i = BCI-power(X).(a`,abs(i)) by Def2,E1
.= a`|^m by E1,ABSVALUE:def 1;
(a`|^j)` = b`|^j by Th17 .=a|^j by BCIALG_1:29;
hence thesis by E9,E11;
end;
suppose E13:j<0;
then E15:-j>0 by XREAL_1:60;
reconsider n=-j as Element of NAT by E13,INT_1:16;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
E17:a|^i = BCI-power(X).(a`,abs(i)) by Def2,E1
.= a`|^m by E1,ABSVALUE:def 1;
a|^j = BCI-power(X).(a`,abs(j)) by Def2,E13
.= a`|^n by E13,ABSVALUE:def 1;
then E19:a|^i\a|^j = b|^(m-n) by Lm20,E15,E2,E17;
per cases;
suppose m>=n;
then reconsider q=m-n as Element of NAT by INT_1:16,XREAL_1:50;
a|^i\a|^j = a|^(-q) by Th9,E19;
hence thesis;
end;
suppose F0:m0 by XREAL_1:52;
then reconsider p=n-m as Element of NAT by INT_1:16;
reconsider c = b` as Element of AtomSet(X) by BCIALG_1:34;
F3:m-n<0 by F0,XREAL_1:51;
then a|^i\a|^j=BCI-power(X).(b`,abs(m-n)) by Def2,E19
.=BCI-power(X).(b`,-(m-n)) by F3,ABSVALUE:def 1
.=a|^p by BCIALG_1:29;
hence thesis;
end;
end;
end;
end;
::1.4.11
theorem Th21:
(a|^i)|^j = a|^(i*j)
proof
per cases;
suppose A1:i>=0;
per cases;
suppose B1:j>=0;
reconsider i,j as Element of NAT by A1,B1,INT_1:16;
(a|^i)|^j = a|^(i*j) by Th15;
hence thesis;
end;
suppose B3:j<0;
then reconsider m=-j as Element of NAT by INT_1:16;
reconsider i as Element of NAT by A1,INT_1:16;
per cases by B3;
suppose D1:i*j<0;
then reconsider p=-i*j as Element of NAT by INT_1:16;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
reconsider d = a|^i as Element of AtomSet(X) by Th12;
a|^(i*j)=BCI-power(X).(a`,abs(i*j)) by Def2,D1
.=a`|^p by D1,ABSVALUE:def 1
.=a`|^(i*(-j))
.=(b|^i)|^m by Th15
.=(a|^i)`|^m by Th17
.=d|^(-m) by Th9
.=a|^i |^(-(-j));
hence thesis;
end;
suppose D3:i*j=0;
reconsider d = 0.X as Element of AtomSet(X) by BCIALG_1:23;
(a|^0)|^j = 0.X|^j by Def1
.=BCI-power(X).((0.X)`,abs(j)) by Def2,B3
.=(0.X)`|^m by B3,ABSVALUE:def 1
.=(d|^m)` by Th17
.=(0.X)` by Th6
.=0.X by BCIALG_1:2
.=a|^(i*j) by D3,Th2;
hence thesis by B3,D3,XCMPLX_1:6;
end;
end;
end;
suppose A3:i<0;
then reconsider m=-i as Element of NAT by INT_1:16;
per cases;
suppose C1:j>0;
then reconsider j as Element of NAT by INT_1:16;
reconsider p=-i*j as Element of NAT by A3,INT_1:16;
reconsider b = a` as Element of AtomSet(X) by BCIALG_1:34;
D1:i*j<0*j by A3,C1,XREAL_1:70;
then a|^(i*j)=BCI-power(X).(a`,abs(i*j)) by Def2
.=a`|^p by D1,ABSVALUE:def 1
.=a`|^((-i)*j)
.=(b|^m)|^j by Th15
.=(a|^(-m))|^j by Th9;
hence thesis;
end;
suppose C3:j=0;
reconsider b = a|^i as Element of AtomSet(X) by Th12;
(a|^i)|^j = b|^0 by C3 .= 0.X by Def1 .=a|^(i*0) by Th2;
hence thesis by C3;
end;
suppose C5:j<0;
then reconsider n=-j as Element of NAT by INT_1:16;
reconsider p=i*j as Element of NAT by A3,C5,INT_1:16;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
reconsider d = a|^m as Element of AtomSet(X) by Th12;
reconsider e =d` as Element of AtomSet(X) by BCIALG_1:34;
a|^i = BCI-power(X).(a`,abs(i)) by Def2,A3
.= a`|^m by A3,ABSVALUE:def 1;
then (a|^i)|^j =e|^(-n) by Th17
.=e`|^n by Th9
.=d|^n by BCIALG_1:29
.=a|^((-i)*(-j)) by Th15;
hence thesis;
end;
end;
end;
theorem Th22:
a|^(i+j) = a|^i\(a|^j)`
proof
per cases;
suppose j>0;
then reconsider j as Element of NAT by INT_1:16;
a|^i\(a|^j)`=a|^i\(a`|^j) by Th17 .=a|^i\(a|^(-j)) by Th9
.=a|^(i-(-j)) by Th20;
hence thesis;
end;
suppose A3:j=0;
then a|^(i+j) = a|^i\0.X by BCIALG_1:2
.=a|^i\(0.X)` by BCIALG_1:2
.=a|^i\(a|^j)` by A3,Th2;
hence thesis;
end;
suppose j<0;
then reconsider n=-j as Element of NAT by INT_1:16;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
a|^i\(a|^j)`=a|^i\(a|^(--j))`
.=a|^i\(a`|^n)` by Th9
.=a|^i\(b`|^n) by Th17
.=a|^i\(a|^n) by BCIALG_1:29
.=a|^(i-n) by Th20;
hence thesis;
end;
end;
definition let X,x;
attr x is finite-period means :Defx1:
ex n being Element of NAT st n<>0 & x|^n in BCK-part(X);
end;
theorem Thx22:
x is finite-period implies x`` is finite-period
proof
assume A1:x is finite-period;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
consider p being Element of NAT such that
C71:p<>0 & x|^p in BCK-part(X) by A1,Defx1;
consider y being Element of X such that
C72:y = x|^p & 0.X <= y by C71;
(x|^p)` = 0.X by C72,BCIALG_1:def 11;
then (b|^p)` = 0.X by Th19;
then 0.X <= b|^p by BCIALG_1:def 11;
then b|^p in BCK-part(X);
hence x`` is finite-period by Defx1,C71;
end;
definition
let X,x such that A1:x is finite-period;
func ord x -> Element of NAT means :Def8a:
x|^it in BCK-part(X)& it<>0 &
for m being Element of NAT st x|^m in BCK-part(X) & m <> 0 holds it <= m;
existence
proof
defpred P[Nat] means x|^$1 in BCK-part(X)& $1<>0;
consider n being Element of NAT such that
A3: n<>0 & x|^n in BCK-part(X) by Defx1,A1;
A5: ex n being Nat st P[n] by A3;
consider k being Nat such that
A7: P[k] and
A9: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A5);
reconsider k as Element of NAT by ORDINAL1:def 13;
take k;
thus x|^k in BCK-part(X)&k <> 0 by A7;
let m be Element of NAT;
assume x |^ m in BCK-part(X) & m <> 0;
hence k <= m by A9;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
assume that
A6: x|^ n1 in BCK-part(X)& n1<>0 &
for m being Element of NAT st x|^ m in BCK-part(X)&m <> 0 holds n1<=m and
A7: x|^ n2 in BCK-part(X) &n2<>0 &
for m being Element of NAT st x|^ m in BCK-part(X)&m <> 0 holds n2<=m;
n1 <= n2 & n2 <= n1 by A6,A7;
hence thesis by XXREAL_0:1;
end;
end;
theorem Th23:
a is finite-period & ord a = n implies a|^n = 0.X
proof
assume a is finite-period & ord a = n;
then a|^n in BCK-part(X) by Def8a;
then consider x being Element of X such that
A3:x = a|^n &0.X<=x;
a|^n in AtomSet(X) by Th12;
then consider y being Element of X such that
A5:y = a|^n & y is atom;
0.X\a|^n = 0.X by A3,BCIALG_1:def 11;
hence thesis by A5,BCIALG_1:def 14;
end;
theorem
X is BCK-algebra iff (for x holds x is finite-period & ord x = 1)
proof
thus X is BCK-algebra implies (for x holds x is finite-period & ord x = 1)
proof
assume A1:X is BCK-algebra;
let x;
x`=0.X by A1,BCIALG_1:def 8;
then 0.X<=x by BCIALG_1:def 11;
then x in BCK-part(X);
then A5:x|^1 in BCK-part(X)&1<>0 by Th3;
then A3:x is finite-period by Defx1;
for m being Element of NAT st x|^m in BCK-part(X) & m <> 0 holds 1<=m
proof
let m be Element of NAT;
assume x|^m in BCK-part(X) & m <> 0;
then 0+1<=m by INT_1:20;
hence thesis;
end;
hence thesis by A3,A5,Def8a;
end;
assume B1:for x holds x is finite-period & ord x = 1;
for y,z being Element of X holds (y\z)\y=0.X
proof
let y,z be Element of X;
(y\z)\y = (y\y)\z by BCIALG_1:7;
then C1:(y\z)\y = z` by BCIALG_1:def 5;
z is finite-period & ord z = 1 by B1;
then z|^1 in BCK-part(X) by Def8a;
then z in BCK-part(X) by Th3;
then consider z1 being Element of X such that
D1:z=z1 & 0.X<=z1;
thus thesis by D1,C1,BCIALG_1:def 11;
end;
then X is_K by BCIALG_1:def 6;
hence thesis by BCIALG_1:18;
end;
theorem Th25:
x is finite-period & a is finite-period & x in BranchV(a) implies
ord x = ord a
proof
assume A1:x is finite-period & a is finite-period & x in BranchV(a);
then consider xx being Element of X such that
A3:x = xx & a<=xx;
set nx = ord x, na = ord a;
a|^na in BCK-part(X) & na<>0 by Def8a,A1;
then A5:na>=1 by NAT_1:14;
per cases by A5,XXREAL_0:1;
suppose B0:na=1;
then a|^1 in BCK-part(X) by Def8a,A1;
then a in BCK-part(X) by Th3;
then consider aa being Element of X such that
B1:a = aa & 0.X <= aa;
a in AtomSet(X);
then consider ab being Element of X such that
B3:a = ab & ab is atom;
a` = 0.X by B1,BCIALG_1:def 11;
then a = 0.X by B3,BCIALG_1:def 14;
then x in BCK-part(X) by A3;
then B7:x|^1 in BCK-part(X)&1<>0 by Th3;
for m being Element of NAT st x|^m in BCK-part(X) & m <> 0
holds 1 <= m by NAT_1:14;
hence thesis by B0,Def8a,A1,B7;
end;
suppose C1:na>1;
a|^na in BCK-part(X) by Def8a,A1;
then consider aa being Element of X such that
B1:a|^na = aa & 0.X <= aa;
0.X in AtomSet(X);
then B2:x` = a` by A1,BCIALG_1:37;
(a|^na)` = 0.X by B1,BCIALG_1:def 11;
then x`|^na = 0.X by B2,Th17;
then (x|^na)` = 0.X by Th17b;
then 0.X <= x|^na by BCIALG_1:def 11;
then B7:x|^na in BCK-part(X)&na<>0 by C1;
for m being Element of NAT st x|^m in BCK-part(X) & m <> 0 holds na <= m
proof
let m be Element of NAT;
assume C1:x|^m in BCK-part(X) & m <> 0;
then consider xx being Element of X such that
C3:x|^m = xx & 0.X <= xx;
(x|^m)` = 0.X by C3,BCIALG_1:def 11;
then a`|^m = 0.X by B2,Th17b;
then (a|^m)` = 0.X by Th17;
then 0.X <= a|^m by BCIALG_1:def 11;
then a|^m in BCK-part(X);
hence thesis by Def8a,A1,C1;
end;
hence thesis by Def8a,A1,B7;
end;
end;
theorem Th26: ::1.5.3
x is finite-period & ord x = n implies(x|^m in BCK-part(X) iff n divides m)
proof
assume A1: x is finite-period & ord x = n;
thus x|^m in BCK-part(X) implies n divides m
proof
defpred P[Nat] means x|^$1 in BCK-part(X) implies n divides $1;
C1: for m being Nat st for k being Nat st k < m holds P[k] holds P[m]
proof
let m be Nat;
assume C2: for k being Nat st k < m holds P[k];
assume C3: x|^m in BCK-part(X);
per cases;
suppose m = 0;
hence thesis by INT_2:16;
end;
suppose C4:m <> 0;
reconsider mm=m as Element of NAT by ORDINAL1:def 13;
m<>0 & x|^mm in BCK-part(X) by C3,C4;
then n <= m by Def8a,A1;
then consider k being Nat such that
C6: m = n + k by NAT_1:10;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
C8:b is finite-period by Thx22,A1;
b\x = 0.X by BCIALG_1:1;
then b<=x by BCIALG_1:def 11;
then x in BranchV(b);
then n = ord b by Th25,C8,A1;
then b|^n in BCK-part(X) by Def8a,C8;
then consider z being Element of X such that
C13:z = b|^n & 0.X <= z;
C15:(b|^n)` = 0.X by C13,BCIALG_1:def 11;
reconsider a = b|^m as Element of AtomSet(X) by Th12;
consider zz being Element of X such that
C17:zz = x|^m & 0.X <= zz by C3;
(x|^m)` = 0.X by C17,BCIALG_1:def 11;
then (b|^(n+k))`= 0.X by C6,Th19;
then (b|^n\(b|^k)`)`= 0.X by Th22;
then ((b|^k)`)`` = 0.X by C15,BCIALG_1:9;
then (b|^k)` = 0.X by BCIALG_1:8;
then (x|^k)` = 0.X by Th19;
then 0.X <= x|^k by BCIALG_1:def 11;
then DD:x|^k in BCK-part(X);
n<>0 by Def8a,A1;
then n divides k by C2,DD,C6,NAT_1:16;
then consider i being Nat such that
C8: k = n * i by NAT_D:def 3;
m =n * (1 + i) by C6,C8;
hence thesis by NAT_D:def 3;
end;
end;
for m being Nat holds P[m] from NAT_1:sch 4(C1);
hence thesis;
end;
assume n divides m;
then consider i being Nat such that
D3:m = n * i by NAT_D:def 3;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
D5:b is finite-period by Thx22,A1;
b\x = 0.X by BCIALG_1:1;
then b<=x by BCIALG_1:def 11;
then x in BranchV(b);
then n = ord b by Th25,D5,A1;
then b|^n in BCK-part(X) by Def8a,D5;
then consider z being Element of X such that
D13:z = b|^n & 0.X <= z;
D15:(b|^n)` = 0.X by D13,BCIALG_1:def 11;
reconsider bn = b|^n as Element of AtomSet(X) by Th12;
(b|^m)` =((bn)|^i)` by Th21,D3;
then (b|^m)` =(0.X)|^i by D15,Th17;
then (b|^m)` =0.X by Th6;
then (x|^m)` =0.X by Th19;
then 0.X <= x|^m by BCIALG_1:def 11;
hence thesis;
end;
theorem ::1.5.4
x is finite-period & x|^m is finite-period & ord x = n & m>0
implies ord(x|^m)=n div (m gcd n)
proof
assume A1: x is finite-period & x|^m is finite-period & ord x = n & m>0;
then A2:n<>0 by Def8a;
Aa:(m gcd n) divides n by INT_2:32;
abs(n) > 0 by A2,ABSVALUE:def 1; then
A3: abs(n) hcf abs(m) > 0 by NEWTON:71;
A4: n gcd m > 0 by A1,NEWTON:71;
reconsider mgn=(m gcd n) as Element of NAT by A3,INT_2:51;
consider vn being Nat such that
A5: n = mgn * vn by Aa,NAT_D:def 3;
reconsider vn as Element of NAT by ORDINAL1:def 13;
m gcd n divides m by INT_2:31;
then consider i being Nat such that
A6: m = mgn * i by NAT_D:def 3;
reconsider i as Element of NAT by ORDINAL1:def 13;
n = mgn * vn + 0 by A5;
then A9: n div mgn = vn by A4,NAT_D:def 1;
A13: vn,i are_relative_prime
proof
(i gcd vn) divides vn by NAT_D:def 5;
then consider b1 being Nat such that
B1: vn = (i gcd vn)*b1 by NAT_D:def 3;
(i gcd vn) divides i by NAT_D:def 5;
then consider b2 being Nat such that
B3: i = (i gcd vn)*b2 by NAT_D:def 3;
B5: n = (m gcd n) * (i gcd vn)*b1 by A5,B1;
m = (m gcd n) * (i gcd vn)*b2 by A6,B3;
then (m gcd n) * (i gcd vn) divides n
& (m gcd n) * (i gcd vn) divides m by B5,NAT_D:def 3;
then (m gcd n) * (i gcd vn) divides (m gcd n) by NAT_D:def 5;
then consider c being Nat such that
B7: m gcd n = (m gcd n) * (i gcd vn)*c by NAT_D:def 3;
B9: (m gcd n)*1 = (m gcd n) * ((i gcd vn)*c) by B7;
m gcd n <>0 by A1,INT_2:35;
then 1 = i gcd vn by B9,NAT_1:15,XCMPLX_1:5;
hence thesis by INT_2:def 4;
end;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
C8:b is finite-period by Thx22,A1;
b\x = 0.X by BCIALG_1:1;
then b<=x by BCIALG_1:def 11;
then x in BranchV(b);
then C12:n = ord b by Th25,C8,A1;
then b|^n in BCK-part(X) by Def8a,C8;
then consider z being Element of X such that
C13:z = b|^n & 0.X <= z;
A12: (x|^m)|^ vn in BCK-part(X)
proof
((x|^m)|^ vn)` = (x|^m)`|^ vn by Th17b
.=(b|^m)`|^ vn by Th19
.=(b|^m|^ vn)` by Th17b
.=(b|^(mgn*i*vn))` by A6,Th21
.=(b|^(n*i))` by A5
.=((b|^n)|^i)` by Th21
.=(b|^n)`|^i by Th17b
.=(0.X)|^i by C13,BCIALG_1:def 11
.= 0.X by Th6;
then 0.X <= (x|^m)|^ vn by BCIALG_1:def 11;
hence thesis;
end;
A11:for mm being Element of NAT st (x|^m)|^mm in BCK-part(X)&mm<>0
holds vn <= mm
proof
let mm be Element of NAT;
assume D1:(x|^m)|^mm in BCK-part(X)&mm<>0;
then consider z being Element of X such that
D3:z = (x|^m)|^mm & 0.X <= z;
((x|^m)|^mm)` = 0.X by D3,BCIALG_1:def 11;
then (x|^m)`|^mm = 0.X by Th17b;
then (b|^m)`|^mm = 0.X by Th19;
then (b|^m|^mm)` = 0.X by Th17b;
then (b|^(m*mm))` = 0.X by Th21;
then 0.X <= b|^(m*mm) by BCIALG_1:def 11;
then b|^(m*mm) in BCK-part(X);
then mgn*vn divides mgn*i*mm by A5,A6,C12,Th26,C8;
then consider c being Nat such that
D5: mgn*i*mm = mgn*vn*c by NAT_D:def 3;
D6: mgn*(i*mm) = mgn*(vn*c) by D5;
mgn <>0 by A1,INT_2:35;
then i*mm = vn*c by D6,XCMPLX_1:5;
then vn divides i*mm by NAT_D:def 3;
then vn divides mm by A13,INT_2:40;
then consider cc being Nat such that
D7: mm = vn*cc by NAT_D:def 3;
cc<>0 by D1,D7;
hence thesis by D7,NAT_1:24;
end;
vn <> 0 by A5,A1,Def8a;
hence thesis by A9,A12,Def8a,A1,A11;
end;
theorem
x is finite-period & x` is finite-period implies ord x = ord(x`)
proof
assume A1:x is finite-period & x` is finite-period;
set n = ord x;
set m = ord(x`);
x|^n in BCK-part(X) by Def8a,A1;
then consider zz being Element of X such that
A3:zz = x|^n & 0.X <= zz;
(x|^n)` = 0.X by A3,BCIALG_1:def 11;
then (x`)|^n = 0.X by Th17b;
then ((x`)|^n)` = 0.X by BCIALG_1:def 5;
then 0.X <= (x`)|^n by BCIALG_1:def 11;
then (x`)|^n in BCK-part(X) & n<>0 by Def8a,A1;
then C1:m<=n by Def8a,A1;
(x`)|^m in BCK-part(X) by Def8a,A1;
then consider zz being Element of X such that
A3:zz = (x`)|^m & 0.X <= zz;
((x`)|^m)` = 0.X by A3,BCIALG_1:def 11;
then (x``)|^m = 0.X by Th17b;
then ((x``)|^m)` = 0.X by BCIALG_1:def 5;
then (x|^m)` = 0.X by Th19;
then 0.X <= x|^m by BCIALG_1:def 11;
then x|^m in BCK-part(X) & m<>0 by Def8a,A1;
then n<=m by Def8a,A1;
hence thesis by C1,XXREAL_0:1;
end;
theorem
x\y is finite-period & x in BranchV(a) & y in BranchV(a) implies ord(x\y)=1
proof
assume A1:x\y is finite-period & x in BranchV(a) & y in BranchV(a);
then x\y in BCK-part(X) by BCIALG_1:40;
then A3:(x\y)|^1 in BCK-part(X) by Th3;
for m being Element of NAT st (x\y)|^m in BCK-part(X) & m <> 0
holds 1 <= m by NAT_1:14;
hence thesis by Def8a,A3,A1;
end;
theorem
x\y is finite-period & a\b is finite-period & x is finite-period
& y is finite-period & a is finite-period & b is finite-period & a<>b &
x in BranchV(a) & y in BranchV(b) implies ord(a\b) divides (ord x lcm ord y)
proof
assume A1:x\y is finite-period & a\b is finite-period & x is finite-period
& y is finite-period & a is finite-period & b is finite-period & a<>b &
x in BranchV(a) & y in BranchV(b);
A6:ord x divides (ord x lcm ord y)
&ord y divides (ord x lcm ord y)by NAT_D:def 4;
then consider xy being Nat such that
A7:ord x lcm ord y =(ord x)* xy by NAT_D:def 3;
consider yx being Nat such that
A8:ord x lcm ord y =(ord y)* yx by A6,NAT_D:def 3;
reconsider xly = ord x lcm ord y as Element of NAT;
reconsider na = ord a, nb = ord b as Element of NAT;
reconsider nab = ord(a\b) as Element of NAT;
(a\b)|^xly = a|^((ord x)* xy)\b|^((ord y)* yx) by A8,A7,Th16
.=(a|^(ord x))|^xy\b|^((ord y)* yx) by Th21
.=(a|^(ord x))|^xy\b|^(ord y)|^ yx by Th21
.=(a|^na)|^xy\b|^(ord y)|^ yx by A1,Th25
.=(0.X)|^xy\b|^(ord y)|^ yx by Th23,A1
.=(0.X)|^xy\b|^(ord b)|^ yx by A1,Th25
.=(0.X)|^xy\(0.X)|^ yx by Th23,A1
.=((0.X)|^ yx)` by Th6
.=(0.X)` by Th6
.=0.X by BCIALG_1:def 5;
then ((a\b)|^xly)` = 0.X by BCIALG_1:def 5;
then 0.X <=(a\b)|^xly by BCIALG_1:def 11;
then (a\b)|^xly in BCK-part(X);
hence ord(a\b) divides (ord x lcm ord y) by Th26,A1;
end;
begin :: Definition of {BCI}-Homomorphisms
reserve X,X',Y,Z,W for BCI-algebra,
H,H' for SubAlgebra of X',
G for SubAlgebra of X,
A for non empty Subset of X,
A' for non empty Subset of X',
I for Ideal of X,
CI,K for closed Ideal of X,
x,y,a,b for Element of X,
RI for I-congruence of X,I,
RK for I-congruence of X,K;
theorem Lmth14:
for X being BCI-algebra
for Y being SubAlgebra of X holds
for x,y being Element of X,x',y' being Element of Y st x = x' & y = y'
holds x\y = x'\y'
proof
let X be BCI-algebra;
let Y be SubAlgebra of X;
let x,y be Element of X,x',y' be Element of Y such that
A1: x = x' & y = y';
A2: [x',y'] in [:the carrier of Y,the carrier of Y:] by ZFMISC_1:106;
x'\y' = ((the InternalDiff of X)||the carrier of Y).(x',y')
by BCIALG_1:def 10
.= x\y by A1,A2,FUNCT_1:72;
hence thesis;
end;
definition let X,X' be non empty BCIStr_0; let f be Function of X,X';
attr f is multiplicative means :Def0:
for a, b being Element of X holds f.(a\b) = f.a\f.b;
end;
registration let X,X' be BCI-algebra;
cluster multiplicative Function of X,X';
existence
proof
reconsider f = (the carrier of X) --> 0.X' as Function of X, X';
take f;
for x,y being Element of X holds f.(x \ y) = f.x \ f.y
proof
let x,y be Element of X;
f.(x \ y) = 0.X' by FUNCOP_1:13
.= (0.X')` by BCIALG_1:2
.= f.x \ 0.X' by FUNCOP_1:13;
hence thesis by FUNCOP_1:13;
end;
hence thesis by Def0;
end;
end;
definition let X,X' be BCI-algebra;
mode BCI-homomorphism of X,X' is multiplicative Function of X,X';
end;
reserve f for BCI-homomorphism of X,X';
reserve g for BCI-homomorphism of X',X;
reserve h for BCI-homomorphism of X',Y;
definition let X,X',f;
attr f is isotonic means
for x,y st x <= y holds f.x <= f.y;
end;
definition let X;
mode Endomorphism of X is BCI-homomorphism of X,X;
end;
definition let X,X',f;
func Ker f equals {x where x is Element of X:f.x=0.X'};
coherence;
end;
theorem PR1621:
f.(0.X) = 0.X'
proof
f.(0.X) = f.((0.X)`) by BCIALG_1:2
.=f.(0.X)\f.(0.X) by Def0;
hence thesis by BCIALG_1:def 5;
end;
registration let X,X',f;
cluster Ker f -> non empty;
coherence
proof
f.(0.X) = 0.X' by PR1621;
then 0.X in Ker f;
hence thesis;
end;
end;
theorem
x <= y implies f.x <= f.y
proof
assume A1:x<=y;
f.x\f.y = f.(x\y) by Def0
.=f.(0.X) by A1,BCIALG_1:def 11
.= 0.X' by PR1621;
hence thesis by BCIALG_1:def 11;
end;
theorem
f is one-to-one iff Ker(f) = {0.X}
proof
thus f is one-to-one implies Ker(f) = {0.X}
proof
assume
A1: f is one-to-one;
thus Ker(f) c= {0.X}
proof
let a be set;
assume a in Ker f;
then consider x being Element of X such that
B1:a=x & f.x = 0.X';
reconsider a as Element of X by B1;
f.a = f.(0.X) by B1,PR1621;
then a = 0.X by A1,FUNCT_2:25;
hence thesis by TARSKI:def 1;
end;
let a be set;
assume A1:a in {0.X};
then reconsider a as Element of X by TARSKI:def 1;
a = 0.X by A1,TARSKI:def 1;
then f.a = 0.X' by PR1621;
hence thesis;
end;
assume AA:Ker(f) = {0.X};
now let a,b;
assume that
A1: a <> b and
A3: f.a = f.b;
f.a \ f.b = 0.X'&f.b \ f.a = 0.X' by A3,BCIALG_1:def 5;
then f.(a \ b) = 0.X'& f.(b\a) = 0.X' by Def0;
then a\b in Ker f & b\a in Ker f;
then a\b =0.X & b\a = 0.X by AA,TARSKI:def 1;
hence contradiction by A1,BCIALG_1:def 7;
end;
then for a,b st f.a = f.b holds a = b;
hence thesis by GROUP_6:1;
end;
theorem
f is bijective & g=f" implies g is bijective
proof
assume A1:f is bijective & g=f";
then A4:g is one-to-one by FUNCT_1:62;
dom f = the carrier of X by FUNCT_2:def 1; then
rng g = the carrier of X by A1,FUNCT_1:55;
then g is onto by FUNCT_2:def 3;
hence thesis by A4;
end;
theorem
h*f is BCI-homomorphism of X,Y
proof
reconsider g = h*f as Function of X,Y;
now let a,b;
thus g.(a \ b) = h.(f.(a \ b)) by FUNCT_2:21
.= h.(f.a \ f.b) by Def0
.= (h.(f.a)) \ (h.(f.b)) by Def0
.= (g.a)\(h.(f.b)) by FUNCT_2:21
.= g.a \ g.b by FUNCT_2:21;
end;
hence thesis by Def0;
end;
theorem
for f being BCI-homomorphism of X,Y,g being BCI-homomorphism of Y,Z,
h being BCI-homomorphism of Z,W holds h*(g*f) = (h*g)*f
proof
let f be BCI-homomorphism of X,Y,g be BCI-homomorphism of Y,Z,
h be BCI-homomorphism of Z,W;
reconsider g1 = h*(g*f) as Function of X,W;
reconsider g2 = (h*g)*f as Function of X,W;
for x being set st x in the carrier of X holds g1.x = g2.x
proof let x be set;
assume D1:x in the carrier of X; then
D2:g1.x = h.((g*f).x) by FUNCT_2:21
.=h.(g.(f.x)) by D1,FUNCT_2:21;
g2.x = (h*g).(f.x) by D1,FUNCT_2:21
.=h.(g.(f.x))by D1,FUNCT_2:7,21;
hence g1.x =g2.x by D2;
end;
hence thesis by FUNCT_2:18;
end;
theorem
for Z being SubAlgebra of X' st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
proof
let Z be SubAlgebra of X';
assume A1: the carrier of Z = rng f;
f is Function of X, Z
proof
dom f = the carrier of X by FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider f' = f as Function of X,Z;
now
let a,b;
thus f'.a \f'.b = f.a \ f.b by Lmth14
.= f'.(a \ b) by Def0;
end;
hence thesis by Def0;
end;
theorem PR1641:
Ker f is closed Ideal of X
proof
now
let x be set;
assume x in Ker f;
then consider x' being Element of X such that
B1:x=x' & f.x' = 0.X';
thus x in the carrier of X by B1;
end; then
A1:Ker f is non empty Subset of X by TARSKI:def 3;
Ker f is Ideal of X
proof
f.(0.X) = 0.X' by PR1621;
then B1:0.X in Ker f;
now let x,y;
assume B3:x\y in Ker f& y in Ker f;
then consider y' being Element of X such that
B5:y=y' & f.y' = 0.X';
consider x' being Element of X such that
B7:x\y=x' & f.x' = 0.X' by B3;
f.x \ 0.X' = 0.X' by B5,B7,Def0;
then f.x = 0.X' by BCIALG_1:2;
hence x in Ker f;
end;
hence thesis by A1,B1,BCIALG_1:def 18;
end;
then reconsider Kf=Ker f as Ideal of X;
Kf is closed
proof
let x be Element of Kf;
x in Kf;
then consider x' being Element of X such that
B1:x=x' & f.x'=0.X';
f.(x`)=f.(0.X)\f.x by Def0;
then f.(x`)=(0.X')` by PR1621,B1;
then f.(x`)=0.X' by BCIALG_1:def 5;
hence x` in Kf;
end;
hence thesis;
end;
registration let X,X',f;
cluster Ker f -> closed Ideal of X;
coherence by PR1641;
end;
theorem Lm1653:
f is onto implies for c being Element of X' ex x st c = f.x
proof
assume f is onto; then
A3: rng f = the carrier of X' by FUNCT_2:def 3;
for c being set holds c in rng f iff ex x st c = f.x
proof
let c be set;
thus c in rng f implies ex x st c = f.x
proof assume c in rng f;
then consider y being set such that
A1:y in dom f& f.y = c by FUNCT_1:def 5;
reconsider y as Element of X by A1;
take y;
thus thesis by A1;
end;
given x such that A3: c = f.x;
x in the carrier of X & the carrier of X = dom f by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 5;
end;
hence thesis by A3;
end;
::P75
theorem
for a being Element of X st a is minimal holds f.a is minimal
proof
let a be Element of X;
assume a is minimal;
then f.a=f.(a``)by BCIALG_2:29;
then f.a=f.0.X\(f.(0.X\a)) by Def0;
then f.a=f.0.X\(f.0.X\f.a) by Def0;
then f.a=(f.0.X\f.a)` by PR1621;
then f.a=(f.a)`` by PR1621;
hence thesis by BCIALG_2:29;
end;
theorem
for a being Element of AtomSet(X),b being Element of AtomSet(X')st b=f.a
holds f.:BranchV(a) c= BranchV(b)
proof
let a be Element of AtomSet(X),b be Element of AtomSet(X') such that
A1:b=f.a;
let y be set;
assume y in f.:BranchV(a);
then consider x being set such that
B1:x in dom f & x in BranchV(a) & y = f.x by FUNCT_1:def 12;
consider x1 being Element of X such that
B3:x=x1 & a<=x1 by B1;
reconsider x as Element of X by B3;
f.a\f.x=f.(a\x) by Def0;
then f.a\f.x=f.(0.X) by B3,BCIALG_1:def 11;
then f.a\f.x=0.X' by PR1621;
then b <= f.x by A1,BCIALG_1:def 11;
hence y in BranchV(b) by B1;
end;
::P76
theorem Thp167:
A' is Ideal of X' implies f"A' is Ideal of X
proof
assume A1:A' is Ideal of X';
0.X' in A' by A1,BCIALG_1:def 18;
then f.0.X in A' by PR1621; then
C3: 0.X in f"A' by FUNCT_2:46;
now let x,y be Element of X;
assume B1:x\y in f"A' & y in f"A'; then
E1: f.(x\y) in A' by FUNCT_2:46;
E3: f.y in A' by B1,FUNCT_2:46;
f.x\f.y in A' by Def0,E1;
then f.x in A' by A1,E3,BCIALG_1:def 18;
hence x in f"A' by FUNCT_2:46;
end;
hence thesis by C3,BCIALG_1:def 18;
end;
theorem
A' is closed Ideal of X' implies f"A' is closed Ideal of X
proof
assume A1: A' is closed Ideal of X';
then reconsider XY=f"A' as Ideal of X by Thp167;
for y being Element of XY holds y` in XY
proof
let y be Element of XY;
B1: f.y in A' by FUNCT_2:46;
reconsider y as Element of X;
(f.y)` in A' by A1,B1,BCIALG_1:def 19;
then f.0.X\f.y in A' by PR1621;
then f.(y`) in A' by Def0;
hence thesis by FUNCT_2:46;
end;
hence thesis by BCIALG_1:def 19;
end;
theorem PR1651:
f is onto implies f.:I is Ideal of X'
proof
assume AA:f is onto;
f.:I is non empty Subset of X'
proof
AB: 0.X in I by BCIALG_1:def 18;
0.X in the carrier of X;
then 0.X in dom f&f.(0.X)=0.X' by PR1621,FUNCT_2:def 1;
hence thesis by AB,FUNCT_1:def 12;
end;
then reconsider imaf = f.:I as non empty Subset of X';
BC: 0.X' in imaf
proof
AB: 0.X in I by BCIALG_1:def 18;
BB:f.(0.X)=0.X' by PR1621;
0.X in the carrier of X;
then 0.X in dom f by FUNCT_2:def 1;
hence 0.X' in imaf by AB,BB,FUNCT_1:def 12;
end;
for x,y being Element of X' st x\y in imaf & y in imaf holds x in imaf
proof
let x,y be Element of X';
assume B3:x\y in imaf& y in imaf;
then consider y' being set such that
B5:y' in dom f & y' in I & y = f.y' by FUNCT_1:def 12;
consider z being set such that
B7:z in dom f & z in I & x\y = f.z by B3,FUNCT_1:def 12;
reconsider y',z as Element of X by B5,B7;
consider yy being Element of X such that
B10:f.yy=x by Lm1653,AA;
set u=yy\((yy\y')\z);
(yy\y'\((yy\y')\z))\z =0.X by BCIALG_1:1;
then (u\y')\z = 0.X by BCIALG_1:7;
then (u\y')\z in I by BCIALG_1:def 18;
then u\y' in I by B7,BCIALG_1:def 18;
then B13:u in I &u in the carrier of X by B5,BCIALG_1:def 18;
then u in dom f by FUNCT_2:def 1;
then [u,f.u] in f by FUNCT_1:8;
then f.(yy\((yy\y')\z))in f.:I by B13,RELAT_1:def 13;
then f.yy\f.((yy\y')\z) in f.:I by Def0;
then f.yy\(f.(yy\y')\f.z) in f.:I by Def0;
then f.yy\(x\y\(x\y))in f.:I by B5,B7,B10,Def0;
then f.yy\0.X' in f.:I by BCIALG_1:def 5;
hence thesis by B10,BCIALG_1:2;
end;
hence thesis by BC,BCIALG_1:def 18;
end;
theorem
f is onto implies f.:CI is closed Ideal of X'
proof
assume f is onto;
then reconsider Kf = f.:CI as Ideal of X' by PR1651;
now let x' be Element of Kf;
consider x being set such that
B5:x in dom f & x in CI & x' = f.x by FUNCT_1:def 12;
reconsider x as Element of CI by B5;
B7: x` in CI by BCIALG_1:def 19;
x` in the carrier of X;
then x` in dom f by FUNCT_2:def 1;
then [x`,f.(x`)] in f by FUNCT_1:8;
then f.(x`)in f.:CI by B7,RELAT_1:def 13;
then f.(0.X)\f.x in f.:CI by Def0;
hence x'` in Kf by B5,PR1621;
end;
hence thesis by BCIALG_1:def 19;
end;
definition let X,X' be BCI-algebra;
pred X,X' are_isomorphic means
:Def4: ex f being BCI-homomorphism of X,X' st f is bijective;
end;
registration let X;let I be Ideal of X,RI be I-congruence of X,I;
cluster X./.RI -> strict being_B being_C being_I being_BCI-4;
coherence;
end;
definition let X; let I be Ideal of X,RI be I-congruence of X,I;
func nat_hom RI -> BCI-homomorphism of X, X./.RI means
:Def5: for x holds it.x = Class(RI,x);
existence
proof
defpred P[Element of X,set] means $2 = Class(RI,$1);
A1: for x being Element of X
ex y being Element of X./.RI st P[x,y]
proof
let x be Element of X;
reconsider y = Class(RI,x) as Element of X./.RI by EQREL_1:def 5;
take y;
thus thesis;
end;
consider f being Function of X,X./.RI such that
A3: for x being Element of X holds P[x,f.x] from FUNCT_2:sch 3(A1);
now let a,b be Element of X;
A5:f.a = Class(RI,a) & f.b = Class(RI,b)by A3;
reconsider E=RI as Congruence of X;
reconsider w1=Class(E,a),w2=Class(E,b)as Element of X./.RI
by EQREL_1:def 5;
f.a \ f.b=Class(RI,a\b) by A5,BCIALG_2:def 17;
hence f.a\f.b=f.(a\b) by A3;
end;
then reconsider f as BCI-homomorphism of X,X./.RI by Def0;
take f;
thus thesis by A3;
end;
uniqueness
proof
let f,g be BCI-homomorphism of X,X./.RI;
assume that
A5: for x be Element of X holds f.x = Class(RI,x) and
A7: for x be Element of X holds g.x = Class(RI,x);
now let x be Element of X;
f.x = Class(RI,x) & g.x = Class(RI,x) by A7,A5;
hence f.x = g.x;
end;
hence thesis by FUNCT_2:113;
end;
end;
begin ::Fundamental Theorem of Homomorphisms
::::::::::::::::::::::::::::::::::::::::
::Fundamental Theorem of Homomorphisms::
::::::::::::::::::::::::::::::::::::::::
:: f :::
:: X--------->X' :::
:: | / :::
:: g| / h :::
:: | / :::
:: | / :::
:: | / :::
:: V / :::
:: X/Ker(f) :::
::::::::::::::::::::::::::::::::::::::::
theorem
nat_hom RI is onto
proof
set f = nat_hom RI;
set Y = X./.RI;
reconsider Y as BCI-algebra;
reconsider f as BCI-homomorphism of X,Y;
for y being set st y in the carrier of Y
ex x being set st x in the carrier of X & y = f.x
proof
let y be set;
assume A1:y in the carrier of Y;
then reconsider y as Element of Y;
consider x being set such that
A3:x in the carrier of X & y = Class(RI,x)by A1,EQREL_1:def 5;
take x;
reconsider x as Element of X by A3;
thus thesis by A3,Def5;
end;
then rng f = the carrier of Y by FUNCT_2:16;
hence thesis by FUNCT_2:def 3;
end;
theorem Lm1662:
I=Ker f implies (ex h being BCI-homomorphism of X./.RI,X' st
(f = h*nat_hom(RI) & h is one-to-one))
proof
assume AA:I = Ker f;
set J = X./.RI;
defpred P[set,set] means for a being Element of X st $1=Class(RI,a)
holds $2 = f.a;
A1: for x being Element of J ex y being Element of X' st P[x,y]
proof
let x be Element of J;
x in Class(RI);
then consider y being set such that
B3:y in the carrier of X & x = Class(RI,y) by EQREL_1:def 5;
reconsider y as Element of X by B3;
reconsider t=f.y as Element of X';
take t;
let a be Element of X;
assume x = Class(RI,a);
then y in Class(RI,a) by B3,EQREL_1:31;
then [a,y] in RI by EQREL_1:26;
then B4:a\y in Ker f & y\a in Ker f by AA,BCIALG_2:def 12;
then consider x1 being Element of X such that
B5:a\y=x1&f.x1=0.X';
consider x2 being Element of X such that
B7:y\a=x2&f.x2=0.X' by B4;
f.a\f.y=0.X' & f.y\f.a=0.X' by Def0,B5,B7;
hence thesis by BCIALG_1:def 7;
end;
consider h being Function of J,X' such that
A9: for x being Element of J holds P[x,h.x] from FUNCT_2:sch 3(A1);
now let a,b be Element of J;
A11:a in Class(RI) & b in Class(RI);
then consider a1 being set such that
A13:a1 in the carrier of X & a = Class(RI,a1) by EQREL_1:def 5;
consider b1 being set such that
A15:b1 in the carrier of X & b = Class(RI,b1) by A11,EQREL_1:def 5;
reconsider a1,b1 as Element of X by A13,A15;
h.a = f.a1 & h.b = f.b1 by A9,A13,A15;
then A19:h.a\h.b =f.(a1\b1) by Def0;
a\b=Class(RI,a1\b1) by A13,A15,BCIALG_2:def 17;
hence h.a\h.b=h.(a\b) by A19,A9;
end;
then reconsider h as BCI-homomorphism of X./.RI,X' by Def0;
X1:h is one-to-one
proof
let y1,y2 be set;
assume DD:y1 in dom h & y2 in dom h & h.y1 = h.y2;
then reconsider S=y1,T=y2 as Element of J;
A21:S in Class(RI) & T in Class(RI);
consider a1 being set such that
A23:a1 in the carrier of X & S = Class(RI,a1) by A21,EQREL_1:def 5;
consider b1 being set such that
A25:b1 in the carrier of X & T = Class(RI,b1) by A21,EQREL_1:def 5;
reconsider a1,b1 as Element of X by A23,A25;
h.S = f.a1 & h.T = f.b1 by A9,A23,A25;
then f.a1\f.b1=0.X'&f.b1\f.a1=0.X' by DD,BCIALG_1:def 5;
then f.(a1\b1)=0.X'&f.(b1\a1)=0.X' by Def0;
then a1\b1 in Ker f & b1\a1 in Ker f;
then [a1,b1] in RI by AA,BCIALG_2:def 12;
then b1 in Class(RI,a1) by EQREL_1:26;
hence thesis by A23,A25,EQREL_1:31;
end;
take h;
f = h*nat_hom(RI)
proof
A31: dom(nat_hom(RI)) = the carrier of X
&dom f = the carrier of X by FUNCT_2:def 1;
A33: now let x be set;
thus x in dom f implies x in dom nat_hom RI & (nat_hom RI).x in dom h
proof
assume A35: x in dom f;
hence x in dom nat_hom RI by A31;
(nat_hom RI).x in rng nat_hom RI &dom h = the carrier of X./.RI
&dom f = the carrier of X by A31,A35,FUNCT_1:def 5,FUNCT_2:def 1;
hence (nat_hom RI).x in dom h;
end;
assume x in dom nat_hom RI & (nat_hom RI).x in dom h;
hence x in dom f by A31;
end;
now let x be set;
assume x in dom f;
then reconsider a = x as Element of X;
(nat_hom RI).a = Class(RI,a) by Def5;
hence f.x = h.((nat_hom RI).x) by A9;
end;
hence thesis by A33,FUNCT_1:20;
end;
hence thesis by X1;
end;
theorem
for X,X',I,RI,f st
I=Ker f holds (ex h being BCI-homomorphism of X./.RI,X' st
(f=h*nat_hom(RI) & h is one-to-one)) by Lm1662;
theorem
Ker(nat_hom RK) = K
proof
set h=nat_hom RK;
set Y = X./.RK;
thus Ker h c= K
proof
let y be set;
assume y in Ker h;
then consider x being Element of X such that
D1:y=x & h.x = 0.Y;
Class(RK,0.X)=Class(RK,x) by Def5,D1;
then x in Class(RK,0.X) by EQREL_1:31;
then [0.X,x] in RK by EQREL_1:26;
then x\0.X in K by BCIALG_2:def 12;
hence y in K by D1,BCIALG_1:2;
end;
let y be set;
assume D1:y in K;
then reconsider x=y as Element of X;
D3:x\0.X in K by D1,BCIALG_1:2;
x` in K by D1,BCIALG_1:def 19;
then [0.X,x] in RK by D3,BCIALG_2:def 12;
then x in Class(RK,0.X) by EQREL_1:26;
then Class(RK,0.X)=Class(RK,x) by EQREL_1:31;
then h.x =0.Y by Def5;
hence y in Ker h;
end;
Lmco1671:
the carrier of H' = rng f implies f is BCI-homomorphism of X,H'
proof
assume A1:the carrier of H' = rng f;
f is Function of X,H'
proof
the carrier of X=dom f by FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider h=f as Function of X,H';
now let a,b be Element of X;
h.a\h.b=f.a\f.b by Lmth14;
hence h.(a\b) = h.a\h.b by Def0;
end;
hence thesis by Def0;
end;
begin :: First Isomorphism Theorem
theorem
I = Ker f & the carrier of H' = rng f implies X./.RI,H' are_isomorphic
proof
assume AA:I = Ker f & the carrier of H' = rng f;
set J = X./.RI;
defpred P[set,set] means for a being Element of X st $1=Class(RI,a)
holds $2 = f.a;
A1: for x being Element of J ex y being Element of H' st P[x,y]
proof
let x be Element of J;
x in Class(RI);
then consider y being set such that
B3:y in the carrier of X & x = Class(RI,y) by EQREL_1:def 5;
reconsider y as Element of X by B3;
dom f = the carrier of X by FUNCT_2:def 1;
then reconsider t=f.y as Element of H' by AA,FUNCT_1:def 5;
take t;
let a be Element of X;
assume x = Class(RI,a);
then y in Class(RI,a) by B3,EQREL_1:31;
then [a,y] in RI by EQREL_1:26;
then B4:a\y in Ker f & y\a in Ker f by AA,BCIALG_2:def 12;
then consider x1 being Element of X such that
B5:a\y=x1&f.x1=0.X';
consider x2 being Element of X such that
B7:y\a=x2&f.x2=0.X' by B4;
f.a\f.y=0.X' & f.y\f.a=0.X' by Def0,B5,B7;
hence thesis by BCIALG_1:def 7;
end;
consider h being Function of J,H' such that
A9: for x being Element of J holds P[x,h.x] from FUNCT_2:sch 3(A1);
now let a,b be Element of J;
A11:a in Class(RI) & b in Class(RI);
then consider a1 being set such that
A13:a1 in the carrier of X & a = Class(RI,a1) by EQREL_1:def 5;
consider b1 being set such that
A15:b1 in the carrier of X & b = Class(RI,b1) by A11,EQREL_1:def 5;
reconsider a1,b1 as Element of X by A13,A15;
reconsider f as BCI-homomorphism of X,H' by AA,Lmco1671;
h.a = f.a1 & h.b = f.b1 by A9,A13,A15;
then A19: h.a \ h.b =f.(a1\b1) by Def0;
a\b=Class(RI,a1\b1) by A13,A15,BCIALG_2:def 17;
hence h.a\h.b=h.(a\b) by A19,A9;
end;
then reconsider h as BCI-homomorphism of X./.RI,H' by Def0;
X1: h is one-to-one
proof
let y1,y2 be set;
assume DD:y1 in dom h & y2 in dom h & h.y1 = h.y2;
then reconsider y1,y2 as Element of J;
A21:y1 in Class(RI) & y2 in Class(RI);
then consider a1 being set such that
A23:a1 in the carrier of X & y1 = Class(RI,a1) by EQREL_1:def 5;
consider b1 being set such that
A25:b1 in the carrier of X & y2 = Class(RI,b1) by A21,EQREL_1:def 5;
reconsider a1,b1 as Element of X by A23,A25;
h.y1 = f.a1 & h.y2 = f.b1 by A9,A23,A25;
then f.a1\f.b1=0.X'&f.b1\f.a1=0.X' by DD,BCIALG_1:def 5;
then f.(a1\b1)=0.X'&f.(b1\a1)=0.X' by Def0;
then a1\b1 in Ker f & b1\a1 in Ker f;
then [a1,b1] in RI by AA,BCIALG_2:def 12;
then b1 in Class(RI,a1) by EQREL_1:26;
hence thesis by A23,A25,EQREL_1:31;
end;
X3:the carrier of H' c= rng h
proof
let y be set;
assume y in the carrier of H';
then consider x being set such that
B3:x in dom f & y=f.x by AA,FUNCT_1:def 5;
reconsider S=Class(RI,x) as Element of J by B3,EQREL_1:def 5;
h.S = f.x & S in the carrier of J & the carrier of J = dom h
by A9,B3,FUNCT_2:def 1;
hence y in rng h by B3,FUNCT_1:def 5;
end;
rng h = the carrier of H' by X3,XBOOLE_0:def 10;
then h is onto by FUNCT_2:def 3;
hence thesis by Def4,X1;
end;
theorem CO1672:
I = Ker f & f is onto implies X./.RI,X' are_isomorphic
proof
assume A1:I = Ker f & f is onto;
then consider h being BCI-homomorphism of X./.RI,X' such that
A3:f=h*nat_hom(RI) & h is one-to-one by Lm1662;
for y being set st y in the carrier of X' holds ex z being set st
z in the carrier of X./.RI&h.z = y
proof let y be set;
assume y in the carrier of X';
then y in rng f by A1,FUNCT_2:def 3;
then consider x being set such that
B3:x in dom f & y=f.x by FUNCT_1:def 5;
take z = (nat_hom RI).x;
dom(nat_hom(RI)) = the carrier of X
& dom f=the carrier of X by FUNCT_2:def 1;
then dom(nat_hom(RI)) = the carrier of X
& dom f=the carrier of X
&(nat_hom RI).x in rng nat_hom RI &dom h = the carrier of X./.RI
& dom f = the carrier of X by B3,FUNCT_1:def 5,FUNCT_2:def 1;
hence thesis by B3,A3,FUNCT_1:23;
end;
then rng h = the carrier of X' by FUNCT_2:16;
then h is onto by FUNCT_2:def 3;
hence thesis by Def4,A3;
end;
begin :: Second Isomorphism Theorem
definition let X,G,K,RK;
func Union(G,RK) -> non empty Subset of X equals
union{Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
correctness
proof
set Z1 =union{Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
set Z2={Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
[0.X,0.X] in RK by EQREL_1:11;
then B5:0.X in Class(RK,0.X) by EQREL_1:26;
0.X = 0.G by BCIALG_1:def 10;
then a1: Class(RK,0.X) in Z2;
now
let x be set;
assume x in Z1;
then consider g being set such that
A1:x in g & g in Z2 by TARSKI:def 4;
consider a being Element of G such that
A3:g=Class(RK,a)&Class(RK,a) in the carrier of X./.RK by A1;
thus x in the carrier of X by A1,A3;
end;
hence thesis by a1,B5,TARSKI:def 3,def 4;
end;
end;
::P72
Lm168:for w being Element of Union(G,RK) holds ex a being
Element of G st w in Class(RK,a)
proof
defpred P[Element of Union(G,RK),Element of Union(G,RK),set] means
$3 = $1\$2;
set Z1 =union{Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
set Z2={Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
let w be Element of Union(G,RK);
consider g being set such that
B1:w in g & g in Z2 by TARSKI:def 4;
consider a being Element of G such that
B3:g=Class(RK,a)&Class(RK,a) in the carrier of X./.RK by B1;
take a;
thus thesis by B1,B3;
end;
definition let X,G,K,RK;
func HKOp(G,RK) -> BinOp of Union(G,RK) means
:Def6:for w1,w2 being Element of Union(G,RK)
for x,y being Element of X st w1=x&w2=y holds it.(w1,w2)=x\y;
existence
proof
defpred P[Element of Union(G,RK),Element of Union(G,RK),set] means
for x,y st $1 =x & $2 = y holds $3 = x\y;
A1: for w1,w2 being Element of Union(G,RK)
ex v being Element of Union(G,RK) st P[w1,w2,v]
proof
let w1,w2 be Element of Union(G,RK);
consider a being Element of G such that
B2:w1 in Class(RK,a) by Lm168;
B4:[a,w1] in RK by B2,EQREL_1:26;
consider b being Element of G such that
B6:w2 in Class(RK,b) by Lm168;
B9:[b,w2] in RK by B6,EQREL_1:26;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider a1=a,b1=b as Element of X by TARSKI:def 3;
reconsider w1,w2 as Element of X;
[a1\b1,w1\w2] in RK by B4,B9,BCIALG_2:def 9;
then w1\w2 in Class(RK,a1\b1) by EQREL_1:26;
then B11:w1\w2 in Class(RK,a\b) by Lmth14;
Class(RK,a1\b1) in the carrier of X./.RK by EQREL_1:def 5;
then Class(RK,a\b) in the carrier of X./.RK by Lmth14;
then Class(RK,a\b) in {Class(RK,c) where c is Element of G:
Class(RK,c) in the carrier of X./.RK};
then reconsider C = w1\w2 as Element of Union(G,RK) by B11,TARSKI:def 4;
take C;
thus thesis;
end;
thus ex B being BinOp of Union(G,RK) st for w1,w2 being Element of
Union(G,RK) holds P[w1,w2,B.(w1,w2)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof
let o1,o2 be BinOp of Union(G,RK);
assume A4:for w1,w2 being Element of Union(G,RK)
for x,y being Element of X st w1=x&w2=y holds o1.(w1,w2)=x\y;
assume A5:for w1,w2 being Element of Union(G,RK)
for x,y being Element of X st w1=x&w2=y holds o2.(w1,w2)=x\y;
now let w1,w2 be Element of Union(G,RK);
o1.(w1,w2)=w1\w2 by A4;
hence o1.(w1,w2)=o2.(w1,w2) by A5;
end;
hence thesis by BINOP_1:2;
end;
end;
definition let X,G,K,RK;
func zeroHK(G,RK) -> Element of Union(G,RK) equals
0.X;
coherence
proof
A1:0.G = 0.X by BCIALG_1:def 10;
then A3:0.G in Class(RK,0.G) by EQREL_1:28;
Class(RK,0.G) in {Class(RK,c) where c is Element of G:
Class(RK,c) in the carrier of X./.RK}by A1;
hence thesis by A1,A3,TARSKI:def 4;
end;
end;
definition let X,G,K,RK;
func HK(G,RK) -> BCIStr_0 equals
BCIStr_0(#Union(G,RK),HKOp(G,RK),zeroHK(G,RK) #);
coherence;
end;
registration let X,G,K,RK;
cluster HK(G,RK) -> non empty;
coherence;
end;
definition let X,G,K,RK; let w1,w2 be Element of Union(G,RK);
func w1\w2 -> Element of Union(G,RK) equals
HKOp(G,RK).(w1,w2);
coherence;
end;
theorem Thz1:
HK(G,RK) is BCI-algebra
proof
reconsider IT = HK(G,RK) as non empty BCIStr_0;
C1: IT is_B
proof
now let x,y,z be Element of IT;
reconsider x1=x,y1=y,z1=z as Element of Union(G,RK);
reconsider x2=x1,y2=y1,z2=z1 as Element of X;
AA:x2\y2 = x1\y1&z2\y2=z1\y1&x2\z2=x1\z1 by Def6;
then (x2\y2)\(z2\y2) = x1\y1\(z1\y1) by Def6;
then ((x2\y2)\(z2\y2))\(x2\z2)=((x1\y1)\(z1\y1))\(x1\z1)by AA,Def6;
hence ((x\y)\(z\y))\(x\z)=0.IT by BCIALG_1:def 3;
end;
hence thesis by BCIALG_1:def 3;
end;
C3:IT is_C
proof
let x,y,z be Element of IT;
reconsider x1=x,y1=y,z1=z as Element of Union(G,RK);
reconsider x2=x1,y2=y1,z2=z1 as Element of X;
x2\y2 = x1\y1&x2\z2=x1\z1 by Def6;
then (x2\y2)\z2 = (x1\y1)\z1&(x2\z2)\y2=(x1\z1)\y1 by Def6;
then ((x2\y2)\z2)\((x2\z2)\y2)=((x1\y1)\z1)\((x1\z1)\y1) by Def6;
hence ((x\y)\z)\((x\z)\y)=0.IT by BCIALG_1:def 4;
end;
C5:IT is_I
proof
let x be Element of IT;
reconsider x1=x as Element of Union(G,RK);
reconsider x2=x1 as Element of X;
x2\x2=x1\x1 by Def6;
hence x\x = 0.IT by BCIALG_1:def 5;
end;
IT is_BCI-4
proof
let x,y be Element of IT;
assume D1:x\y=0.IT&y\x=0.IT;
reconsider x1=x,y1=y as Element of Union(G,RK);
reconsider x2=x1,y2=y1 as Element of X;
x2\y2 = 0.X & y2\x2 = 0.X by D1,Def6;
hence x=y by BCIALG_1:def 7;
end;
hence thesis by C1,C3,C5;
end;
registration let X,G,K,RK;
cluster HK(G,RK) -> strict being_B being_C being_I being_BCI-4;
coherence by Thz1;
end;
theorem Thxm1:
HK(G,RK) is SubAlgebra of X
proof
set IT = HK(G,RK);
C1:0.IT = 0.X;
set V1=the carrier of IT;
reconsider D = V1 as non empty set;
set A = (the InternalDiff of X)||V1;
set B = the InternalDiff of IT;
set VV = the carrier of X;
dom(the InternalDiff of X) = [:VV,VV:] by FUNCT_2:def 1;
then dom A = [:VV,VV:] /\ [:V1,V1:] & [:V1,V1:] c= [:VV,VV:]
by RELAT_1:90,ZFMISC_1:119;
then A3:dom A = [:D,D:] by XBOOLE_1:28;
rng A = D
proof
for y being set holds y in D iff ex z being set st z in dom A & y = A.z
proof let y be set;
E1:y in D implies ex z being set st z in dom A & y = A.z
proof
assume F1:y in D;
then reconsider y1=y,y2=0.IT as Element of X;
F3:[y,0.IT] in [:D,D:] & [y,0.IT] in [:VV,VV:] by F1,ZFMISC_1:106;
then A.[y,0.IT] = y1\y2 by FUNCT_1:72
.= y by BCIALG_1:2;
hence thesis by A3,F3;
end;
now given z being set such that
F5:z in dom A & y = A.z;
consider x1,x2 being set such that
F7:x1 in D & x2 in D and
F9:z = [x1,x2] by A3,F5,ZFMISC_1:def 2;
reconsider x1,x2 as Element of Union(G,RK) by F7;
reconsider v1 = x1, v2 = x2 as Element of VV;
y = v1\v2 by F5,F9,FUNCT_1:70;
then y = x1\x2 by Def6;
hence y in D;
end;
hence thesis by E1;
end;
hence thesis by FUNCT_1:def 5;
end;
then reconsider A as BinOp of V1 by A3,FUNCT_2:def 1,RELSET_1:11;
now let x,y be Element of V1;
G1: x in V1 & y in V1;
then G3:[x,y] in [:V1,V1:]&[x,y] in [:VV,VV:] by ZFMISC_1:def 2;
reconsider xx=x,yy=y as Element of Union(G,RK);
reconsider vx=x,vy=y as Element of VV by G1;
A.(x,y)=vx\vy by G3,FUNCT_1:72;
hence A.(x,y)=B.(x,y) by Def6;
end;
then A=B by BINOP_1:2;
hence thesis by C1,BCIALG_1:def 10;
end;
theorem
(the carrier of G)/\K is closed Ideal of G
proof
set GK = (the carrier of G)/\K;
A1:0.G = 0.X by BCIALG_1:def 10; then
c1:0.G in K by BCIALG_1:def 18; then
C1:0.G in GK by XBOOLE_0:def 4;
for x being set st x in GK holds x in the carrier of G by XBOOLE_0:def 4;
then C2:GK is non empty Subset of G by c1,TARSKI:def 3,XBOOLE_0:def 4;
for x,y being Element of G st x\y in GK & y in GK holds x in GK
proof
let x,y be Element of G;
assume x\y in GK & y in GK;
then D3:x\y in K & y in K by XBOOLE_0:def 4;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider x1=x,y1=y as Element of X by TARSKI:def 3;
x1\y1 in K & y1 in K by Lmth14,D3;
then x in K by BCIALG_1:def 18;
hence x in GK by XBOOLE_0:def 4;
end;
then reconsider GK as Ideal of G by C1,C2,BCIALG_1:def 18;
for x being Element of GK holds x` in GK
proof
let x be Element of GK;
D1:x in the carrier of G & x in K by XBOOLE_0:def 4;
then reconsider y=x as Element of X;
y` in K by D1,BCIALG_1:def 19;
then x` in K by Lmth14,A1;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by BCIALG_1:def 19;
end;
theorem
for K1 being Ideal of HK(G,RK),RK1 being I-congruence of HK(G,RK),K1,
I being Ideal of G,RI being I-congruence of G,I st
K1=K & RK1=RK & I=(the carrier of G)/\K holds
G./.RI,HK(G,RK)./.RK1 are_isomorphic
proof
let K1 be Ideal of HK(G,RK),RK1 be I-congruence of HK(G,RK),K1,
I be Ideal of G,RI be I-congruence of G,I;
assume
A1:K1=K & RK1=RK & I=(the carrier of G)/\K;
A3:the carrier of G c= the carrier of HK(G,RK)
proof
let xx be set;
assume xx in the carrier of G;
then reconsider x=xx as Element of G;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then H2:x in the carrier of X by TARSKI:def 3;
then [x,x] in RK by EQREL_1:11;
then H3:x in Class(RK,x) by EQREL_1:26;
Class(RK,x) in the carrier of X./.RK by H2,EQREL_1:def 5;
then Class(RK,x) in {Class(RK,a)
where a is Element of G:Class(RK,a) in the carrier of X./.RK};
hence xx in the carrier of HK(G,RK)by H3,TARSKI:def 4;
end;
defpred P[Element of G,set] means $2 = Class(RK1,$1);
A5: for x being Element of G
ex y being Element of HK(G,RK)./.RK1 st P[x,y]
proof let x be Element of G;
set y=Class(RK1,x);
x in the carrier of G; then
reconsider y as Element of HK(G,RK)./.RK1 by A3,EQREL_1:def 5;
take y;
thus thesis;
end;
consider f being Function of G, HK(G,RK)./.RK1 such that
A7: for x being Element of G holds P[x,f.x]from FUNCT_2:sch 3(A5);
now let a,b be Element of G;
a in the carrier of G& b in the carrier of G;
then reconsider Wa=Class(RK1,a),Wb=Class(RK1,b)as Element of Class RK1
by A3,EQREL_1:def 5;
a in the carrier of G& b in the carrier of G;
then reconsider a1=a,b1=b as Element of HK(G,RK) by A3;
Wa=f.a&Wb=f.b by A7;
then B9:f.a\f.b=Class(RK1,a1\b1) by BCIALG_2:def 17;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider xa=a,xb=b as Element of X by TARSKI:def 3;
CC: HK(G,RK) is SubAlgebra of X by Thxm1;
xa\xb=a1\b1 by Lmth14,CC;
then f.a\f.b=Class(RK1,a\b) by B9,Lmth14;
hence f.(a\b)=f.a\f.b by A7;
end;
then reconsider f as BCI-homomorphism of G, HK(G,RK)./.RK1 by Def0;
CC1:f is onto
proof
now let y be set;
y in the carrier of HK(G,RK)./.RK1 implies y in rng f
proof
assume y in the carrier of HK(G,RK)./.RK1;
then consider x being set such that
D3:x in the carrier of HK(G,RK) & y=Class(RK1,x) by EQREL_1:def 5;
consider a being Element of G such that
D5:x in Class(RK,a) by Lm168,D3;
a in the carrier of G &
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then y = Class(RK1,a) by D3,A1,D5,EQREL_1:31;
then D9:y=f.a by A7;
a in the carrier of G &dom f = the carrier of G by FUNCT_2:def 1;
hence y in rng f by D9,FUNCT_1:def 5;
end;
hence y in rng f iff y in the carrier of HK(G,RK)./.RK1;
end;
then rng f = the carrier of HK(G,RK)./.RK1 by TARSKI:2;
hence thesis by FUNCT_2:def 3;
end;
Ker f = I
proof
set X' = HK(G,RK)./.RK1;
thus Ker f c= I
proof let h be set;
assume h in Ker f;
then consider x being Element of G such that
D1:h=x & f.x = 0.X';
x in the carrier of G &
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider x as Element of X;
Class(RK,x)= Class(RK,0.X)by A1,D1,A7;
then 0.X in Class(RK,x) by EQREL_1:31;
then [x,0.X] in RK by EQREL_1:26;
then x\0.X in K & 0.X in K by BCIALG_1:def 18,BCIALG_2:def 12;
then x in K by BCIALG_1:def 18;
hence h in I by D1,A1,XBOOLE_0:def 4;
end;
let h be set;
assume D0:h in I;
then reconsider x=h as Element of X by A1;
D1:h in the carrier of G & h in K by A1,D0,XBOOLE_0:def 4;
D3:x\0.X in K by D1,BCIALG_1:2;
x` in K by D1,BCIALG_1:def 19;
then [x,0.X] in RK by D3,BCIALG_2:def 12;
then 0.X in Class(RK,x) by EQREL_1:26;
then Class(RK1,h)= Class(RK1,0.X)by A1,EQREL_1:31;
then f.h = 0.X' by A7,D0;
hence h in Ker f by D0;
end;
hence thesis by CO1672,CC1;
end;