:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008-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 NUMBERS, BCIALG_1, SUBSET_1, INT_1, FUNCT_1, NAT_1, XBOOLE_0,
ZFMISC_1, STRUCT_0, CARD_1, SUPINF_2, ARYTM_3, RELAT_1, NEWTON, COMPLEX1,
XXREAL_0, WAYBEL15, ARYTM_1, GROUP_1, INT_2, UNIALG_2, CARD_FIL, RCOMP_1,
BCIALG_2, REALSET1, MSSUBFAM, FUNCOP_1, MOD_4, GROUP_6, TARSKI, FUNCT_2,
CHORD, WELLORD1, EQREL_1, CARD_3, BINOP_1, BCIALG_6, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, XCMPLX_0, STRUCT_0, BCIALG_1,
FUNCOP_1, ORDINAL1, NUMBERS, INT_2, XXREAL_0, NAT_D, INT_1, NAT_1,
BCIALG_2, EQREL_1;
constructors BINOP_1, REALSET1, BCIALG_2, REAL_1, BINOP_2, FINSEQOP, NAT_D,
RELSET_1, XXREAL_0, NAT_1;
registrations RELSET_1, REALSET1, STRUCT_0, BCIALG_1, BCIALG_2, FUNCT_2,
PARTFUN1, NAT_1, XREAL_0, ORDINAL1, XXREAL_0, INT_1, XCMPLX_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, BCIALG_1, FUNCT_1, XBOOLE_0;
equalities REALSET1, BINOP_1, STRUCT_0, BCIALG_1, BCIALG_2, XBOOLE_0;
expansions TARSKI, BINOP_1, BCIALG_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCOP_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, NAT_1, INT_1, CLASSES1;
begin :: The power of an Element of BCI-algebra
reserve X for BCI-algebra;
reserve n for Nat;
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[object,object] means
ex f being sequence of 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 x be object st x in the carrier of G ex y be object st P[x,y]
proof
let x be object;
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 sequence of the carrier of G such that
A2: 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,g0,b;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = the carrier of G & for x be object st x in the carrier of G
holds P[x,f.x] from CLASSES1:sch 1(A1);
defpred P[Element of G,Nat,set] means ex g0 being sequence of
the carrier of G st g0 = f.$1 & $3 = g0.$2;
A4: for a being Element of G, n being Nat ex b being Element of
G st P[a,n,b]
proof
let a be Element of G, n be Nat;
consider g0 being sequence of the carrier of G, h being Element of
G such that
a = h and
A5: g0 = f.a and
g0.0 = 0.G and
for n holds g0.(n + 1) = h\(g0.n)` by A3;
take g0.n, g0;
thus thesis by A5;
end;
consider F being Function of [:the carrier of G,NAT:], the carrier of G
such that
A6: for a being Element of G, n being Nat holds P[a,n,F.(a,n)]
from NAT_1:sch 19(A4);
take F;
let h be Element of G;
A7: ex g2 being sequence of 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 A3;
ex g1 being sequence of the carrier of G st g1 = f.h & F.(h,0) =
g1.0 by A6;
hence F.(h,0) = 0.G by A7;
let n;
A8: ex g2 being sequence of 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 A3;
( ex g0 being sequence of the carrier of G
st g0 = f.h & F.(h,n)= g0.n)&
ex g1 being sequence of the carrier of G st g1 = f.h & F.(h,n + 1
) = g1.(n + 1) by A6;
hence thesis by A8;
end;
uniqueness
proof
let f,g be Function of [:the carrier of G,NAT:], the carrier of G;
assume that
A9: for h being Element of G holds f.(h,0) = 0.G & for n holds f.(h,n
+ 1) = h\(f.(h,n))` and
A10: 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[Nat] means f.[h,$1] = g.[h,$1];
A11: now
let n;
assume
A12: P[n];
A13: g.[h,n] = g.(h,n);
f.[h,n + 1] = f.(h,n + 1) .= h\(f.(h,n))` by A9
.= g.(h,n + 1) by A10,A12,A13
.= g.[h,n + 1];
hence P[n+1];
end;
f.[h,0] = f.(h,0) .= 0.G by A9
.= g.(h,0) by A10
.= g.[h,0];
then
A14: P[0];
for n holds P[n] from NAT_1:sch 2(A14,A11);
hence f.(h,n) = g.(h,n);
end;
hence thesis;
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,x; let i be Integer;
func x |^ i -> Element of X equals
:Def2:
BCI-power(X).(x,|.i.|) if 0 <= i
otherwise (BCI-power(X).(x`,|.i.|));
correctness;
end;
definition
let X,x; let n be natural Number;
redefine func x |^ n equals :: redefines |^ (BCIALG_6, definition)
BCI-power(X).(x,n);
compatibility
proof
let g be Element of X;
|.n.| = n by ABSVALUE:def 1;
hence thesis by Def2;
end;
end;
theorem Th1:
a\(x\b) = b\(x\a)
proof
b in AtomSet(X);
then
A1: ex y1 being Element of X st b=y1 & y1 is atom;
(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 A1;
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
A2: b\(x\a)\(a\(x\b))=0.X by BCIALG_1:def 3;
a\(x\b)<=(b\(x\a)) by BCIALG_1:26;
then a\(x\b)\(b\(x\a)) = 0.X;
hence thesis by A2,BCIALG_1:def 7;
end;
theorem Th2:
x |^ (n+1) = x\(x |^ n )`
by Def1;
theorem Th3:
x |^ 0 = 0.X by Def1;
theorem Th4:
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 Th5:
x |^ -1 = x`
proof
x |^ (-1)= BCI-power(X).(x`,|.-1 .|) by Def2;
then x |^ (-1)= BCI-power(X).(x`,-(-1)) by ABSVALUE:def 1;
then x |^ (-1)= x`|^ 1;
hence thesis by Th4;
end;
theorem
x |^ 2 = x\x`
proof
x |^ 2 = x|^(1+1) .= x\(x|^1)` by Def1;
hence thesis by Th4;
end;
theorem Th7:
0.X |^ n = 0.X
proof
defpred P[Nat] means (0.X) |^ $1 = 0.X;
A1: now
let n;
assume P[n];
then (0.X) |^ (n + 1) = ((0.X)`)` by Th2
.=(0.X)` by BCIALG_1:def 5
.= 0.X by BCIALG_1:def 5;
hence P[n+1];
end;
A2: P[0] by Def1;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
::P18-theorem 1.4.2(1-4)
theorem
(a |^ (-1))|^ (-1) = a
proof
(a |^ -1)|^ -1 = (a`)|^ -1 by Th5
.= a`` by Th5;
hence thesis by BCIALG_1:29;
end;
theorem
x |^(-n) =(x``)|^(-n)
proof
defpred P[Nat] means x |^(-$1) =(x``)|^(-$1);
A1: now
let n;
assume P[n];
set m=-(n+1);
x |^ m = BCI-power(X).(x`,|.m.|) by Def2
.= BCI-power(X).((x``)`,|.m.|) by BCIALG_1:8
.= (x``) |^(-(n+1)) by Def2;
hence P[n+1];
end;
x |^(0) =0.X by Def1
.=(x``)|^(0) by Def1;
then
A2: P[0];
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th10:
a` |^ n = a |^ -n
proof
per cases;
suppose
A1: n=0;
hence a` |^ n = 0.X by Def1
.= a|^ -n by A1,Th3;
end;
suppose
A2: n>0;
set m=-n;
-(-n)>0 by A2;
then
A3: m<0;
then a|^m = BCI-power(X).(a`,|.m.|) by Def2
.=BCI-power(X).(a`,-(-n)) by A3,ABSVALUE:def 1;
hence thesis;
end;
end;
theorem
x in BCK-part(X) & n>=1 implies x|^n = x
proof
assume that
A1: x in BCK-part(X) and
A2: n>=1;
defpred P[Nat] means x |^ $1 = x;
A3: ex y being Element of X st y=x & 0.X<=y by A1;
A4: now
let n;
assume n>=1;
assume P[n];
then x |^ (n+1) =x\x` by Th2
.=x\0.X by A3
.= x by BCIALG_1:2;
hence P[n+1];
end;
A5: P[1] by Th4;
for n st n>=1 holds P[n] from NAT_1:sch 8(A5,A4);
hence thesis by A2;
end;
theorem
x in BCK-part(X) implies x|^ (-n) = 0.X
proof
defpred P[Nat] means x |^ (-$1) = 0.X;
assume x in BCK-part(X);
then
A1: ex y being Element of X st y=x & 0.X<=y;
A2: now
let n;
assume
A3: P[n];
per cases;
suppose -n=0;
then x |^(-(n+1)) =x` by Th5
.=0.X by A1;
hence P[n+1];
end;
suppose
A4: -n<0;
then BCI-power(X).(x`,|.-n.|) = 0.X by A3,Def2;
then BCI-power(X).(x`,--n) = 0.X by A4,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 A1;
then 0.X = x`|^ (n+1) by Th2
.=BCI-power(X).(x`,-(-(n+1)))
.=BCI-power(X).(x`,|.-(n+1).|) by ABSVALUE:def 1
.=x |^ (-(n+1)) by Def2;
hence P[n+1];
end;
end;
x |^ (-0) = x |^ 0
.= 0.X by Def1; then
A5: P[0];
for n holds P[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
::P19 theorem 1.4.3
theorem Th13:
a|^i in AtomSet(X)
proof
defpred P[Integer] means a |^ $1 in AtomSet(X);
0.X in AtomSet(X);
then
A1: P[0] by Def1;
per cases;
suppose
A2: i>=0;
A3: for i2 be Integer st i2>=0 holds P[i2] implies P[i2 + 1]
proof
let i2 be Integer;
assume i2>=0;
then reconsider j=i2 as Element of NAT by INT_1:3;
(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
A4: (a|^(j+1))``=a\(a |^ j)``` by BCIALG_1:29;
assume P[i2];
then (a|^(j+1))``=a\(a |^ j)` by A4,BCIALG_1:29;
then (a|^(j+1))``=a |^ (j+1) by Def1;
hence thesis by BCIALG_1:29;
end;
for i st i>=0 holds P[i] from INT_1:sch 2(A1,A3);
hence thesis by A2;
end;
suppose
A5: i<=0;
A6: for i2 be Integer st i2<=0 holds P[i2] implies P[i2 - 1]
proof
let i2 be Integer;
assume
A7: i2<=0;
assume
A8: P[i2];
per cases by A7;
suppose
A9: i2=0;
(a`)``=a` by BCIALG_1:8;
then a` in AtomSet(X) by BCIALG_1:29;
hence thesis by A9,Th5;
end;
suppose
A10: i2<0;
set j=i2;
reconsider m=-j as Element of NAT by A10,INT_1:3;
a|^(j-1)=(BCI-power(X).(a`,|.j-1.|)) by A10,Def2;
then a|^(j-1)=(BCI-power(X).(a`,-(j-1))) by A10,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 Th10;
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 A8,BCIALG_1:29;
then (a|^(j-1))``=a`\(a |^ -m )` by BCIALG_1:9;
then (a|^(j-1))``=a`\(a` |^ m )` by Th10;
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`,|.j-1.|)) by A10,ABSVALUE:def 1;
then (a|^(j-1))``=a|^(j-1) by A10,Def2;
hence thesis by BCIALG_1:29;
end;
end;
for i st i<=0 holds P[i] from INT_1:sch 3(A1,A6);
hence thesis by A5;
end;
end;
theorem Th14:
(a|^(n+1))` = (a|^n)`\a
proof
A1: a|^n in AtomSet(X) by Th13;
(a|^(n+1))` =( a\(a |^ n )`)` by Th2
.=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)
Lm1: a|^(n+m) = a|^m\(a|^n)`
proof
reconsider p = a|^n as Element of AtomSet(X) by Th13;
defpred P[Nat] means a|^(n+$1) = a|^$1\(a|^n)`;
A1: now
let m;
reconsider q = a|^(m+1) as Element of AtomSet(X) by Th13;
assume
A2: P[m];
a|^(n+(m+1))=a|^(n+m+1) .=a\(a|^m\(a|^n)`)` by A2,Th2
.=a\((a|^m)`\((a|^n)``)) by BCIALG_1:9
.=a\((a|^m)`\p) by BCIALG_1:29
.=p\((a|^m)`\a) by Th1
.=a|^n\(a|^(m+1))` by Th14
.=q\(p)` by Th1
.= a|^(m+1)\(a|^n)`;
hence P[m+1];
end;
a|^0\(a|^n)` = (a|^n)`` by Def1
.=p by BCIALG_1:29;
then
A3: P[0];
for m holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm2: (a|^m)|^n = a|^(m*n)
proof
defpred P[Nat] means (a|^m)|^$1 = a|^(m*$1);
A1: now
let n;
assume P[n];
then (a|^m)|^(n+1) =(a|^m)\((a|^(m*n)))` by Th2
.=(a|^(m+m*n)) by Lm1
.= a|^(m*(n+1));
hence P[n+1];
end;
(a|^m)|^0 =0.X by Def1;
then
A2: P[0] by Def1;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th15:
(a\b)|^n = a|^n\(b|^n)
proof
defpred P[Nat] means (a\b)|^$1 = a|^$1\(b|^$1);
A1: now
let n;
A2: (b|^n)` in AtomSet(X) by BCIALG_1:34;
A3: a|^(n+1) in AtomSet(X) by Th13;
assume P[n];
then (a\b)|^(n+1) = (a\b)\(a|^n\(b|^n))` by Th2
.= (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 A2,Th1
.= ((b|^n)`\b)\((a|^n)`\a) by BCIALG_1:7
.= (b|^(n+1))`\((a|^n)`\a) by Th14
.= (b|^(n+1))`\(a|^(n+1))` by Th14
.= ((b|^(n+1))\(a|^(n+1)))` by BCIALG_1:9
.= a|^(n+1)\(b|^(n+1)) by A3,BCIALG_1:30;
hence P[n+1];
end;
(a\b)|^0=0.X by Def1
.=(0.X)` by BCIALG_1:def 5
.=a|^0\0.X by Def1;
then
A4: P[0] by Def1;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem
(a\b)|^(-n) = a|^(-n)\(b|^(-n))
proof
set c = a`, d = b`;
reconsider c,d as Element of AtomSet(X) by BCIALG_1:34;
A1: c|^n = a|^(-n) & d|^n = b |^ (-n) by Th10;
(a\b)|^(-n)=((a\b)`)|^n by Th10
.=(a`\b`)|^n by BCIALG_1:9;
hence thesis by A1,Th15;
end;
theorem Th17:
a`|^n = (a|^n)`
proof
defpred P[Nat] means a`|^$1 = (a|^$1)`;
A1: now
let n;
assume P[n];
0.X in AtomSet(X);
then a`|^(n+1) =(0.X)|^(n+1)\(a|^(n+1)) by Th15
.= (a|^(n+1))` by Th7;
hence P[n+1];
end;
a`|^0 =0.X by Def1
.=(0.X)` by BCIALG_1:def 5;
then
A2: P[0] by Def1;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th18:
x`|^n = (x|^n)`
proof
defpred P[Nat] means x`|^$1 = (x|^$1)`;
A1: now
let n;
assume P[n];
then x`|^(n+1) =x`\((x|^ n)`)` by Th2
.=(x\(x|^ n )`)` by BCIALG_1:9
.= (x|^(n+1))` by Th2;
hence P[n+1];
end;
x`|^0 = 0.X by Def1
.=(0.X)` by BCIALG_1:def 5;
then
A2: P[0] by Def1;
for n holds P[n] from NAT_1:sch 2(A2,A1);
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 Th10
.= (c|^n)` by Th17
.= (a|^(-n))` by Th10;
hence thesis;
end;
theorem Th20:
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);
A1: now
let n;
assume
A2: P[n];
now
set b=(x``)|^n;
let a;
assume a=(x``)|^(n+1);
x`` in AtomSet(X) by BCIALG_1:34;
then reconsider b as Element of AtomSet(X) by Th13;
0.X in AtomSet(X) & x|^n in BranchV(b) by A2;
then (x|^n)` =((x``)|^n)` by BCIALG_1:37;
then
A3: x|^(n+1) =x\((x``)|^n)` by Th2;
((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 A3,Th2;
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);
hence a=(x``)|^(n+1) implies x|^(n+1) in BranchV(a);
end;
hence P[n+1];
end;
x|^0 = 0.X by Def1;
then 0.X \ x|^0 = 0.X by BCIALG_1:2;
then 0.X <= x|^0;
then (x``)|^0 <= x|^0 by Def1;
then
A4: P[0];
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th21:
(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 Th13;
0.X in AtomSet(X) & x|^n in BranchV(b) by Th20;
hence thesis by BCIALG_1:37;
end;
Lm3: i>0&j>0 implies a|^i \ a|^j = a|^(i-j)
proof
assume that
A1: i>0 and
A2: j>0;
per cases by XXREAL_0:1;
suppose
A3: 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 A3;
end;
suppose
A4: i>j;
set m=i-j;
m>0 by A4,XREAL_1:50;
then reconsider j,m as Element of NAT by A2,INT_1:3;
a|^i = a|^((i-j)+j) .=a|^j\(a|^m)` by Lm1;
then
A5: a|^i\a|^j=a|^j\a|^j\(a|^m)` by BCIALG_1:7;
a|^m in AtomSet(X) by Th13;
then (a|^m)``=a|^m by BCIALG_1:29;
hence thesis by A5,BCIALG_1:def 5;
end;
suppose
A6: i<j;
set m=j-i;
m>0 by A6,XREAL_1:50;
then reconsider i,m as Element of NAT by A1,INT_1:3;
A7: 0.X in AtomSet(X);
a|^j = a|^(i+(j-i)) .=a|^i\(a|^m)` by Lm1;
then a|^i\a|^j = (a|^m)` by A7,BCIALG_1:32;
then a|^i\a|^j = a`|^m by Th17;
then a|^i\a|^j = a|^(-m) by Th10;
hence thesis;
end;
end;
theorem Th22:
a|^i \ a|^j = a|^(i-j)
proof
per cases;
suppose
A1: i>0;
per cases;
suppose
j>0;
hence thesis by A1,Lm3;
end;
suppose
A2: j=0;
a|^(i-0) = a|^i\0.X by BCIALG_1:2
.=a|^i \ a|^0 by Def1;
hence thesis by A2;
end;
suppose
A3: j<0;
set m=-j;
reconsider i,m as Element of NAT by A1,A3,INT_1:3;
a|^j = BCI-power(X).(a`,|.j.|) by A3,Def2
.= a`|^m by A3,ABSVALUE:def 1
.= (a|^m)` by Th17;
then a|^i \ a|^j = a|^(i+m) by Lm1;
hence thesis;
end;
end;
suppose
A4: i=0;
per cases;
suppose
j>=0;
then reconsider j as Element of NAT by INT_1:3;
a|^0 \ a|^j = (a|^j)` by Def1
.= a`|^j by Th17
.=a|^ -j by Th10;
hence thesis by A4;
end;
suppose
A5: j<0;
set m=-j;
reconsider m as Element of NAT by A5,INT_1:3;
a|^j = BCI-power(X).(a`,|.j.|) by A5,Def2
.= a`|^m by A5,ABSVALUE:def 1
.= (a|^m)` by Th17;
then a|^0 \ a|^j = a|^(0+m) by Lm1;
hence thesis by A4;
end;
end;
suppose
A6: i<0;
then reconsider m=-i as Element of NAT by INT_1:3;
A7: -i>0 by A6;
per cases;
suppose
A8: j>=0;
set n=-(i-j);
reconsider n,j as Element of NAT by A6,A8,INT_1:3;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
A9: (a`|^j)` = b`|^j by Th17
.=a|^j by BCIALG_1:29;
A10: a|^i = BCI-power(X).(a`,|.i.|) by A6,Def2
.= a`|^m by A6,ABSVALUE:def 1;
a|^(i-j) = BCI-power(X).(a`,|.i-j.|) by A6,Def2
.= a`|^n by A6,ABSVALUE:def 1
.= b|^(j+m)
.= a`|^m\(a`|^j)` by Lm1;
hence thesis by A10,A9;
end;
suppose
A11: j<0;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
A12: -j>0 by A11;
reconsider n=-j as Element of NAT by A11,INT_1:3;
A13: a|^j = BCI-power(X).(a`,|.j.|) by A11,Def2
.= a`|^n by A11,ABSVALUE:def 1;
a|^i = BCI-power(X).(a`,|.i.|) by A6,Def2
.= a`|^m by A6,ABSVALUE:def 1;
then
A14: a|^i\a|^j = b|^(m-n) by A7,A12,A13,Lm3;
per cases;
suppose
m>=n;
then reconsider q=m-n as Element of NAT by INT_1:3,XREAL_1:48;
a|^i\a|^j = a|^(-q) by A14,Th10;
hence thesis;
end;
suppose
A15: m<n;
then n-m>0 by XREAL_1:50;
then reconsider p=n-m as Element of NAT by INT_1:3;
A16: m-n<0 by A15,XREAL_1:49;
then a|^i\a|^j=BCI-power(X).(b`,|.m-n.|) by A14,Def2
.=BCI-power(X).(b`,-(m-n)) by A16,ABSVALUE:def 1
.=a|^p by BCIALG_1:29;
hence thesis;
end;
end;
end;
end;
::1.4.11
theorem Th23:
(a|^i)|^j = a|^(i*j)
proof
per cases;
suppose
A1: i>=0;
per cases;
suppose
j>=0;
then reconsider i,j as Element of NAT by A1,INT_1:3;
(a|^i)|^j = a|^(i*j) by Lm2;
hence thesis;
end;
suppose
A2: j<0;
then reconsider m=-j as Element of NAT by INT_1:3;
reconsider i as Element of NAT by A1,INT_1:3;
per cases by A2;
suppose
A3: i*j<0;
then reconsider p=-i*j as Element of NAT by INT_1:3;
reconsider b=a` as Element of AtomSet(X) by BCIALG_1:34;
reconsider d = a|^i as Element of AtomSet(X) by Th13;
a|^(i*j)=BCI-power(X).(a`,|.i*j.|) by A3,Def2
.=a`|^p by A3,ABSVALUE:def 1
.=a`|^(i*(-j))
.=(b|^i)|^m by Lm2
.=(a|^i)`|^m by Th17
.=d|^(-m) by Th10
.=a|^i |^(-(-j));
hence thesis;
end;
suppose
A4: 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)`,|.j.|) by A2,Def2
.=(0.X)`|^m by A2,ABSVALUE:def 1
.=(d|^m)` by Th17
.=(0.X)` by Th7
.=0.X by BCIALG_1:2
.=a|^(i*j) by A4,Th3;
hence thesis by A2,A4,XCMPLX_1:6;
end;
end;
end;
suppose
A5: i<0;
then reconsider m=-i as Element of NAT by INT_1:3;
per cases;
suppose
A6: j>0;
then reconsider j as Element of NAT by INT_1:3;
reconsider b = a` as Element of AtomSet(X) by BCIALG_1:34;
reconsider p=-i*j as Element of NAT by A5,INT_1:3;
A7: i*j<0*j by A5,A6;
then a|^(i*j)=BCI-power(X).(a`,|.i*j.|) by Def2
.=a`|^p by A7,ABSVALUE:def 1
.=a`|^((-i)*j)
.=(b|^m)|^j by Lm2
.=(a|^(-m))|^j by Th10;
hence thesis;
end;
suppose
A8: j=0;
reconsider b = a|^i as Element of AtomSet(X) by Th13;
(a|^i)|^j = b|^0 by A8
.= 0.X by Def1
.=a|^(i*0) by Th3;
hence thesis by A8;
end;
suppose j<0;
then reconsider n=-j as Element of NAT by INT_1:3;
reconsider d = a|^m as Element of AtomSet(X) by Th13;
reconsider e =d` as Element of AtomSet(X) by BCIALG_1:34;
a|^i = BCI-power(X).(a`,|.i.|) by A5,Def2
.= a`|^m by A5,ABSVALUE:def 1;
then (a|^i)|^j =e|^(-n) by Th17
.=e`|^n by Th10
.=d|^n by BCIALG_1:29
.=a|^((-i)*(-j)) by Lm2;
hence thesis;
end;
end;
end;
theorem Th24:
a|^(i+j) = a|^i\(a|^j)`
proof
per cases;
suppose
j>0;
then reconsider j as Element of NAT by INT_1:3;
a|^i\(a|^j)`=a|^i\(a`|^j) by Th17
.=a|^i\(a|^(-j)) by Th10
.=a|^(i-(-j)) by Th22;
hence thesis;
end;
suppose
A1: 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 A1,Th3;
hence thesis;
end;
suppose
j<0;
then reconsider n=-j as Element of NAT by INT_1:3;
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 Th10
.=a|^i\(b`|^n) by Th17
.=a|^i\(a|^n) by BCIALG_1:29
.=a|^(i-n) by Th22;
hence thesis;
end;
end;
definition
let X,x;
attr x is finite-period means
ex n being Element of NAT st n<>0 & x|^ n in BCK-part(X);
end;
theorem Th25:
x is finite-period implies x`` is finite-period
proof
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
assume x is finite-period;
then consider p being Element of NAT such that
A1: p<>0 and
A2: x|^p in BCK-part(X);
ex y being Element of X st y = x|^p & 0.X <= y by A2;
then (x|^p)` = 0.X;
then (b|^p)` = 0.X by Th21;
then 0.X <= b|^p;
then b|^p in BCK-part(X);
hence thesis by A1;
end;
definition
let X,x such that
A1: x is finite-period;
func ord x -> Element of NAT means
:Def5:
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;
ex n being Element of NAT st n<>0 & x|^n in BCK-part(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 Element of NAT by ORDINAL1:def 12;
take k;
thus x|^k in BCK-part(X)&k <> 0 by A3;
let m be Element of NAT;
assume x |^ m in BCK-part(X) & m <> 0;
hence thesis by A4;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
assume 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)& 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 );
then n1 <= n2 & n2 <= n1;
hence thesis by XXREAL_0:1;
end;
end;
theorem Th26:
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 Def5;
then ex x being Element of X st x = a|^n & 0.X<=x;
then
A1: 0.X\a|^n = 0.X;
a|^n in AtomSet(X) by Th13;
then ex y being Element of X st y = a|^n & y is atom;
hence thesis by A1;
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;
A2: 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 that
x|^m in BCK-part(X) and
A3: m <> 0;
0+1<=m by A3,INT_1:7;
hence thesis;
end;
x`=0.X by A1,BCIALG_1:def 8;
then 0.X<=x;
then x in BCK-part(X);
then
A4: x|^1 in BCK-part(X) by Th4;
then x is finite-period;
hence thesis by A4,A2,Def5;
end;
assume
A5: 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;
z is finite-period & ord z = 1 by A5;
then z|^1 in BCK-part(X) by Def5;
then z in BCK-part(X) by Th4;
then
A6: ex z1 being Element of X st z=z1 & 0.X<=z1;
(y\z)\y = (y\y)\z by BCIALG_1:7;
then (y\z)\y = z` by BCIALG_1:def 5;
hence thesis by A6;
end;
then X is being_K;
hence thesis by BCIALG_1:18;
end;
theorem Th28:
x is finite-period & a is finite-period & x in BranchV(a)
implies ord x = ord a
proof
assume that
A1: x is finite-period and
A2: a is finite-period and
A3: x in BranchV(a);
set na = ord a;
na<>0 by A2,Def5;
then
A4: na>=1 by NAT_1:14;
per cases by A4,XXREAL_0:1;
suppose
A5: na=1;
then a|^1 in BCK-part(X) by A2,Def5;
then a in BCK-part(X) by Th4;
then ex aa being Element of X st a = aa & 0.X <= aa;
then
A6: a` = 0.X;
a in AtomSet(X);
then ex ab being Element of X st a = ab & ab is atom;
then a = 0.X by A6;
then
A7: x|^1 in BCK-part(X) by A3,Th4;
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 A1,A5,A7,Def5;
end;
suppose
A8: na>1;
0.X in AtomSet(X);
then
A9: x` = a` by A3,BCIALG_1:37;
A10: 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 that
A11: x|^m in BCK-part(X) and
A12: m <> 0;
ex xx being Element of X st x|^m = xx & 0.X <= xx by A11;
then (x|^m)` = 0.X;
then a`|^m = 0.X by A9,Th18;
then (a|^m)` = 0.X by Th17;
then 0.X <= a|^m;
then a|^m in BCK-part(X);
hence thesis by A2,A12,Def5;
end;
a|^na in BCK-part(X) by A2,Def5;
then ex aa being Element of X st a|^na = aa & 0.X <= aa;
then (a|^na)` = 0.X;
then x`|^na = 0.X by A9,Th17;
then (x|^na)` = 0.X by Th18;
then 0.X <= x|^na;
then x|^na in BCK-part(X);
hence thesis by A1,A8,A10,Def5;
end;
end;
theorem Th29: ::1.5.3
x is finite-period & ord x = n implies(x|^m in BCK-part(X) iff n divides m)
proof
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
reconsider bn = b|^n as Element of AtomSet(X) by Th13;
assume that
A1: x is finite-period and
A2: ord x = n;
A3: b is finite-period by A1,Th25;
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;
A4: for m being Nat st for k being Nat st k < m holds P[k] holds P[m]
proof
let m be Nat;
assume
A5: for k being Nat st k < m holds P[k];
assume
A6: x|^m in BCK-part(X);
per cases;
suppose
m = 0;
hence thesis by INT_2:12;
end;
suppose
A7: m <> 0;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
x|^mm in BCK-part(X) by A6;
then n <= m by A1,A2,A7,Def5;
then consider k being Nat such that
A8: m = n + k by NAT_1:10;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
A9: b is finite-period by A1,Th25;
b\x = 0.X by BCIALG_1:1;
then b<=x;
then x in BranchV(b);
then n = ord b by A1,A2,A9,Th28;
then b|^n in BCK-part(X) by A9,Def5;
then ex z being Element of X st z = b|^n & 0.X <= z;
then
A10: (b|^n)` = 0.X;
ex zz being Element of X st zz = x|^m & 0.X <= zz by A6;
then (x|^m)` = 0.X;
then (b|^(n+k))`= 0.X by A8,Th21;
then (b|^n\(b|^k)`)`= 0.X by Th24;
then ((b|^k)`)`` = 0.X by A10,BCIALG_1:9;
then (b|^k)` = 0.X by BCIALG_1:8;
then (x|^k)` = 0.X by Th21;
then 0.X <= x|^k;
then
A11: x|^k in BCK-part(X);
n<>0 by A1,A2,Def5;
then n divides k by A5,A8,A11,NAT_1:16;
then consider i being Nat such that
A12: k = n * i by NAT_D:def 3;
m =n * (1 + i) by A8,A12;
hence thesis by NAT_D:def 3;
end;
end;
for m being Nat holds P[m] from NAT_1:sch 4(A4);
hence thesis;
end;
assume n divides m;
then consider i being Nat such that
A13: m = n * i by NAT_D:def 3;
b\x = 0.X by BCIALG_1:1;
then b<=x;
then x in BranchV(b);
then n = ord b by A1,A2,A3,Th28;
then b|^n in BCK-part(X) by A3,Def5;
then ex z being Element of X st z = b|^n & 0.X <= z;
then
A14: (b|^n)` = 0.X;
(b|^m)` =((bn)|^i)` by A13,Th23;
then (b|^m)` =(0.X)|^i by A14,Th17;
then (b|^m)` =0.X by Th7;
then (x|^m)` =0.X by Th21;
then 0.X <= x|^m;
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 that
A1: x is finite-period and
A2: x|^m is finite-period and
A3: ord x = n and
A4: m>0;
reconsider b = x`` as Element of AtomSet(X) by BCIALG_1:34;
A5: b is finite-period by A1,Th25;
b\x = 0.X by BCIALG_1:1;
then b<=x;
then x in BranchV(b);
then
A6: n = ord b by A1,A3,A5,Th28;
then b|^n in BCK-part(X) by A5,Def5;
then
A7: ex z being Element of X st z = b|^n & 0.X <= z;
reconsider mgn=(m gcd n) as Element of NAT;
(m gcd n) divides n by INT_2:21;
then consider vn being Nat such that
A8: n = mgn * vn by NAT_D:def 3;
reconsider vn as Element of NAT by ORDINAL1:def 12;
m gcd n divides m by INT_2:21;
then consider i being Nat such that
A9: m = mgn * i by NAT_D:def 3;
reconsider i as Element of NAT by ORDINAL1:def 12;
A10: n = mgn * vn + 0 by A8;
A11: vn,i are_coprime
proof
(i gcd vn) divides i by NAT_D:def 5;
then consider b2 being Nat such that
A12: i = (i gcd vn)*b2 by NAT_D:def 3;
m = (m gcd n) * (i gcd vn)*b2 by A9,A12;
then
A13: (m gcd n) * (i gcd vn) divides m by NAT_D:def 3;
(i gcd vn) divides vn by NAT_D:def 5;
then consider b1 being Nat such that
A14: vn = (i gcd vn)*b1 by NAT_D:def 3;
n = (m gcd n) * (i gcd vn)*b1 by A8,A14;
then (m gcd n) * (i gcd vn) divides n by NAT_D:def 3;
then (m gcd n) * (i gcd vn) divides (m gcd n) by A13,NAT_D:def 5;
then consider c being Nat such that
A15: m gcd n = (m gcd n) * (i gcd vn)*c by NAT_D:def 3;
A16: m gcd n <>0 by A4,INT_2:5;
(m gcd n)*1 = (m gcd n) * ((i gcd vn)*c) by A15;
then 1 = i gcd vn by A16,NAT_1:15,XCMPLX_1:5;
hence thesis by INT_2:def 3;
end;
A17: 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 that
A18: (x|^m)|^mm in BCK-part(X) and
A19: mm<>0;
ex z being Element of X st z = (x|^m)|^mm & 0.X <= z by A18;
then ((x|^m)|^mm)` = 0.X;
then (x|^m)`|^mm = 0.X by Th18;
then (b|^m)`|^mm = 0.X by Th21;
then (b|^m|^mm)` = 0.X by Th18;
then (b|^(m*mm))` = 0.X by Th23;
then 0.X <= b|^(m*mm);
then b|^(m*mm) in BCK-part(X);
then mgn*vn divides mgn*i*mm by A8,A9,A5,A6,Th29;
then consider c being Nat such that
A20: mgn*i*mm = mgn*vn*c by NAT_D:def 3;
A21: mgn <>0 by A4,INT_2:5;
mgn*(i*mm) = mgn*(vn*c) by A20;
then i*mm = vn*c by A21,XCMPLX_1:5;
then vn divides i*mm by NAT_D:def 3;
then vn divides mm by A11,INT_2:25;
then consider cc being Nat such that
A22: mm = vn*cc by NAT_D:def 3;
cc<>0 by A19,A22;
hence thesis by A22,NAT_1:24;
end;
((x|^m)|^ vn)` = (x|^m)`|^ vn by Th18
.=(b|^m)`|^ vn by Th21
.=(b|^m|^ vn)` by Th18
.=(b|^(mgn*i*vn))` by A9,Th23
.=(b|^(n*i))` by A8
.=((b|^n)|^i)` by Th23
.=(b|^n)`|^i by Th18
.=(0.X)|^i by A7
.= 0.X by Th7;
then 0.X <= (x|^m)|^ vn;
then
A23: (x|^m)|^ vn in BCK-part(X);
n gcd m > 0 by A4,NEWTON:58;
then
A24: n div mgn = vn by A10,NAT_D:def 1;
vn <> 0 by A1,A3,A8,Def5;
hence thesis by A2,A24,A23,A17,Def5;
end;
theorem
x is finite-period & x` is finite-period implies ord x = ord(x`)
proof
assume that
A1: x is finite-period and
A2: x` is finite-period;
set m = ord(x`);
(x`)|^m in BCK-part(X) by A2,Def5;
then ex zz being Element of X st zz = (x`)|^m & 0.X <= zz;
then ((x`)|^m)` = 0.X;
then (x``)|^m = 0.X by Th18;
then ((x``)|^m)` = 0.X by BCIALG_1:def 5;
then (x|^m)` = 0.X by Th21;
then 0.X <= x|^m;
then
A3: x|^m in BCK-part(X);
set n = ord x;
m<>0 by A2,Def5;
then
A4: n<=m by A1,A3,Def5;
x|^n in BCK-part(X) by A1,Def5;
then ex zz being Element of X st zz = x|^n & 0.X <= zz;
then (x|^n)` = 0.X;
then (x`)|^n = 0.X by Th18;
then ((x`)|^n)` = 0.X by BCIALG_1:def 5;
then 0.X <= (x`)|^n;
then
A5: (x`)|^n in BCK-part(X);
n<>0 by A1,Def5;
then m<=n by A2,A5,Def5;
hence thesis by A4,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 that
A1: x\y is finite-period and
A2: x in BranchV(a) & y in BranchV(a);
A3: for m being Element of NAT st (x\y)|^m in BCK-part(X) & m <> 0 holds 1
<= m by NAT_1:14;
x\y in BCK-part(X) by A2,BCIALG_1:40;
then (x\y)|^1 in BCK-part(X) by Th4;
hence thesis by A1,A3,Def5;
end;
theorem
a\b is finite-period & x is finite-period & y is finite-period & a is
finite-period & b is finite-period & x in BranchV(a) & y in BranchV(b) implies
ord(a\b) divides (ord x lcm ord y)
proof
assume that
A1: a\b is finite-period and
A2: x is finite-period and
A3: y is finite-period and
A4: a is finite-period and
A5: b is finite-period and
A6: x in BranchV(a) and
A7: y in BranchV(b);
ord y divides (ord x lcm ord y) by NAT_D:def 4;
then consider yx being Nat such that
A8: ord x lcm ord y =(ord y)* yx by NAT_D:def 3;
reconsider na = ord a as Element of NAT;
reconsider xly = ord x lcm ord y as Element of NAT;
ord x divides (ord x lcm ord y) by NAT_D:def 4;
then consider xy being Nat such that
A9: ord x lcm ord y =(ord x)* xy by NAT_D:def 3;
(a\b)|^xly = a|^((ord x)* xy)\b|^((ord y)* yx) by A9,A8,Th15
.=(a|^(ord x))|^xy\b|^((ord y)* yx) by Th23
.=(a|^(ord x))|^xy\b|^(ord y)|^ yx by Th23
.=(a|^na)|^xy\b|^(ord y)|^ yx by A2,A4,A6,Th28
.=(0.X)|^xy\b|^(ord y)|^ yx by A4,Th26
.=(0.X)|^xy\b|^(ord b)|^ yx by A3,A5,A7,Th28
.=(0.X)|^xy\(0.X)|^ yx by A5,Th26
.=((0.X)|^ yx)` by Th7
.=(0.X)` by Th7
.=0.X by BCIALG_1:def 5;
then ((a\b)|^xly)` = 0.X by BCIALG_1:def 5;
then 0.X <=(a\b)|^xly;
then (a\b)|^xly in BCK-part(X);
hence thesis by A1,Th29;
end;
begin :: Definition of {BCI}-Homomorphisms
reserve X,X9,Y for BCI-algebra,
H9 for SubAlgebra of X9,
G for SubAlgebra of X,
A9 for non empty Subset of X9,
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 Th34:
for X being BCI-algebra for Y being SubAlgebra of X holds for x,
y being Element of X,x9,y9 being Element of Y st x = x9 & y = y9 holds x\y = x9
\y9
proof
let X be BCI-algebra;
let Y be SubAlgebra of X;
let x,y be Element of X,x9,y9 be Element of Y such that
A1: x = x9 & y = y9;
A2: [x9,y9] in [:the carrier of Y,the carrier of Y:] by ZFMISC_1:87;
x9\y9 = ((the InternalDiff of X)||the carrier of Y).(x9,y9) by
BCIALG_1:def 10
.= x\y by A1,A2,FUNCT_1:49;
hence thesis;
end;
definition
let X,X9 be non empty BCIStr_0;
let f be Function of X,X9;
attr f is multiplicative means
:Def6:
for a, b being Element of X holds f.(a \b) = f.a\f.b;
end;
registration
let X,X9 be BCI-algebra;
cluster multiplicative for Function of X,X9;
existence
proof
reconsider f = (the carrier of X) --> 0.X9 as Function of X, X9;
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.X9 by FUNCOP_1:7
.= (0.X9)` by BCIALG_1:2
.= f.x \ 0.X9 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
hence thesis;
end;
end;
definition
let X,X9 be BCI-algebra;
mode BCI-homomorphism of X,X9 is multiplicative Function of X,X9;
end;
reserve f for BCI-homomorphism of X,X9;
reserve g for BCI-homomorphism of X9,X;
reserve h for BCI-homomorphism of X9,Y;
definition
let X,X9,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,X9,f;
func Ker f -> set equals
{x where x is Element of X:f.x=0.X9};
coherence;
end;
theorem Th35:
f.(0.X) = 0.X9
proof
f.(0.X) = f.((0.X)`) by BCIALG_1:2
.=f.(0.X)\f.(0.X) by Def6;
hence thesis by BCIALG_1:def 5;
end;
registration
let X,X9,f;
cluster Ker f -> non empty;
coherence
proof
f.(0.X) = 0.X9 by Th35;
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 Def6
.=f.(0.X) by A1
.= 0.X9 by Th35;
hence thesis;
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 object;
assume a in Ker f;
then
A2: ex x being Element of X st a=x & f.x = 0.X9;
then reconsider a as Element of X;
f.a = f.(0.X) by A2,Th35;
then a = 0.X by A1,FUNCT_2:19;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume
A3: a in {0.X};
then reconsider a as Element of X by TARSKI:def 1;
a = 0.X by A3,TARSKI:def 1;
then f.a = 0.X9 by Th35;
hence thesis;
end;
assume
A4: Ker(f) = {0.X};
now
let a,b;
assume that
A5: a <> b and
A6: f.a = f.b;
f.b \ f.a = 0.X9 by A6,BCIALG_1:def 5;
then f.(b\a) = 0.X9 by Def6;
then b\a in Ker f;
then
A7: b\a = 0.X by A4,TARSKI:def 1;
f.a \ f.b = 0.X9 by A6,BCIALG_1:def 5;
then f.(a \ b) = 0.X9 by Def6;
then a\b in Ker f;
then a\b =0.X by A4,TARSKI:def 1;
hence contradiction by A5,A7,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";
dom f = the carrier of X by FUNCT_2:def 1;
then rng g = the carrier of X by A1,FUNCT_1:33;
then
A2: g is onto by FUNCT_2:def 3;
g is one-to-one by A1,FUNCT_1:40;
hence thesis by A2;
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:15
.= h.(f.a \ f.b) by Def6
.= (h.(f.a)) \ (h.(f.b)) by Def6
.= (g.a)\(h.(f.b)) by FUNCT_2:15
.= g.a \ g.b by FUNCT_2:15;
end;
hence thesis by Def6;
end;
theorem
for Z being SubAlgebra of X9 st the carrier of Z = rng f holds f is
BCI-homomorphism of X,Z
proof
let Z be SubAlgebra of X9;
A1: dom f = the carrier of X by FUNCT_2:def 1;
assume the carrier of Z = rng f;
then reconsider f9 = f as Function of X,Z by A1,RELSET_1:4;
now
let a,b;
thus f9.a \f9.b = f.a \ f.b by Th34
.= f9.(a \ b) by Def6;
end;
hence thesis by Def6;
end;
theorem Th41:
Ker f is closed Ideal of X
proof
now
let x be object;
assume x in Ker f;
then ex x9 being Element of X st x=x9 & f.x9 = 0.X9;
hence x in the carrier of X;
end;
then
A1: Ker f is non empty Subset of X by TARSKI:def 3;
A2: now
let x,y;
assume x\y in Ker f & y in Ker f;
then
(ex y9 being Element of X st y=y9 & f.y9 = 0.X9 )& ex x9 being Element
of X st x\y=x9 & f.x9 = 0.X9;
then f.x \ 0.X9 = 0.X9 by Def6;
then f.x = 0.X9 by BCIALG_1:2;
hence x in Ker f;
end;
f.(0.X) = 0.X9 by Th35;
then 0.X in Ker f;
then reconsider Kf=Ker f as Ideal of X by A1,A2,BCIALG_1:def 18;
Kf is closed
proof
let x be Element of Kf;
x in Kf;
then
A3: ex x9 being Element of X st x=x9 & f.x9=0.X9;
f.(x`)=f.(0.X)\f.x by Def6;
then f.(x`)=(0.X9)` by A3,Th35;
then f.(x`)=0.X9 by BCIALG_1:def 5;
hence thesis;
end;
hence thesis;
end;
registration
let X,X9,f;
cluster Ker f -> closed for Ideal of X;
coherence by Th41;
end;
theorem Th42:
f is onto implies for c being Element of X9 ex x st c = f.x
proof
A1: 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 object such that
A2: y in dom f and
A3: f.y = c by FUNCT_1:def 3;
reconsider y as Element of X by A2;
take y;
thus thesis by A3;
end;
given x such that
A4: c = f.x;
the carrier of X = dom f by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:def 3;
end;
assume f is onto;
then rng f = the carrier of X9 by FUNCT_2:def 3;
hence thesis by A1;
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 Def6;
then f.a=f.0.X\(f.0.X\f.a) by Def6;
then f.a=(f.0.X\f.a)` by Th35;
then f.a=(f.a)`` by Th35;
hence thesis by BCIALG_2:29;
end;
theorem
for a being Element of AtomSet(X),b being Element of AtomSet(X9)st b=f
.a holds f.:BranchV(a) c= BranchV(b)
proof
let a be Element of AtomSet(X),b be Element of AtomSet(X9) such that
A1: b=f.a;
let y be object;
assume y in f.:BranchV(a);
then consider x being object such that
x in dom f and
A2: x in BranchV(a) and
A3: y = f.x by FUNCT_1:def 6;
A4: ex x1 being Element of X st x=x1 & a<=x1 by A2;
reconsider x as Element of X by A2;
f.a\f.x=f.(a\x) by Def6;
then f.a\f.x=f.(0.X) by A4;
then f.a\f.x=0.X9 by Th35;
then b <= f.x by A1;
hence thesis by A3;
end;
::P76
theorem Th45:
A9 is Ideal of X9 implies f"A9 is Ideal of X
proof
assume
A1: A9 is Ideal of X9;
A2: now
let x,y be Element of X;
assume that
A3: x\y in f"A9 and
A4: y in f"A9;
f.(x\y) in A9 by A3,FUNCT_2:38;
then
A5: f.x\f.y in A9 by Def6;
f.y in A9 by A4,FUNCT_2:38;
then f.x in A9 by A1,A5,BCIALG_1:def 18;
hence x in f"A9 by FUNCT_2:38;
end;
0.X9 in A9 by A1,BCIALG_1:def 18;
then f.0.X in A9 by Th35;
then 0.X in f"A9 by FUNCT_2:38;
hence thesis by A2,BCIALG_1:def 18;
end;
theorem
A9 is closed Ideal of X9 implies f"A9 is closed Ideal of X
proof
assume
A1: A9 is closed Ideal of X9;
then reconsider XY=f"A9 as Ideal of X by Th45;
for y being Element of XY holds y` in XY
proof
let y be Element of XY;
A2: f.y in A9 by FUNCT_2:38;
reconsider y as Element of X;
(f.y)` in A9 by A1,A2,BCIALG_1:def 19;
then f.0.X\f.y in A9 by Th35;
then f.(y`) in A9 by Def6;
hence thesis by FUNCT_2:38;
end;
hence thesis by BCIALG_1:def 19;
end;
theorem Th47:
f is onto implies f.:I is Ideal of X9
proof
0.X in the carrier of X;
then
A1: 0.X in dom f by FUNCT_2:def 1;
0.X in I & f.(0.X)=0.X9 by Th35,BCIALG_1:def 18;
then reconsider imaf = f.:I as non empty Subset of X9 by A1,FUNCT_1:def 6;
0.X in the carrier of X;
then
A2: 0.X in dom f by FUNCT_2:def 1;
assume
A3: f is onto;
A4: for x,y being Element of X9 st x\y in imaf & y in imaf holds x in imaf
proof
let x,y be Element of X9;
assume that
A5: x\y in imaf and
A6: y in imaf;
consider y9 being object such that
A7: y9 in dom f and
A8: y9 in I and
A9: y = f.y9 by A6,FUNCT_1:def 6;
consider yy being Element of X such that
A10: f.yy=x by A3,Th42;
consider z being object such that
A11: z in dom f and
A12: z in I and
A13: x\y = f.z by A5,FUNCT_1:def 6;
reconsider y9,z as Element of X by A7,A11;
set u=yy\((yy\y9)\z);
(yy\y9\((yy\y9)\z))\z =0.X by BCIALG_1:1;
then (u\y9)\z = 0.X by BCIALG_1:7;
then (u\y9)\z in I by BCIALG_1:def 18;
then u\y9 in I by A12,BCIALG_1:def 18;
then
A14: u in I by A8,BCIALG_1:def 18;
u in the carrier of X;
then u in dom f by FUNCT_2:def 1;
then [u,f.u] in f by FUNCT_1:1;
then f.(yy\((yy\y9)\z))in f.:I by A14,RELAT_1:def 13;
then f.yy\f.((yy\y9)\z) in f.:I by Def6;
then f.yy\(f.(yy\y9)\f.z) in f.:I by Def6;
then f.yy\(x\y\(x\y))in f.:I by A9,A13,A10,Def6;
then f.yy\0.X9 in f.:I by BCIALG_1:def 5;
hence thesis by A10,BCIALG_1:2;
end;
0.X in I & f.(0.X)=0.X9 by Th35,BCIALG_1:def 18;
then 0.X9 in imaf by A2,FUNCT_1:def 6;
hence thesis by A4,BCIALG_1:def 18;
end;
theorem
f is onto implies f.:CI is closed Ideal of X9
proof
assume f is onto;
then reconsider Kf = f.:CI as Ideal of X9 by Th47;
now
let x9 be Element of Kf;
consider x being object such that
x in dom f and
A1: x in CI and
A2: x9 = f.x by FUNCT_1:def 6;
reconsider x as Element of CI by A1;
x` in the carrier of X;
then x` in dom f by FUNCT_2:def 1;
then x` in CI & [x`,f.(x`)] in f by BCIALG_1:def 19,FUNCT_1:1;
then f.(x`)in f.:CI by RELAT_1:def 13;
then f.(0.X)\f.x in f.:CI by Def6;
hence x9` in Kf by A2,Th35;
end;
hence thesis by BCIALG_1:def 19;
end;
definition
let X,X9 be BCI-algebra;
pred X,X9 are_isomorphic means
ex f being BCI-homomorphism of X,X9 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
:Def10:
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 3;
take y;
thus thesis;
end;
consider f being Function of X,X./.RI such that
A2: 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;
f.a = Class(RI,a) & f.b = Class(RI,b) by A2;
then f.a \ f.b=Class(RI,a\b) by BCIALG_2:def 17;
hence f.a\f.b=f.(a\b) by A2;
end;
then reconsider f as BCI-homomorphism of X,X./.RI by Def6;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be BCI-homomorphism of X,X./.RI;
assume that
A3: for x be Element of X holds f.x = Class(RI,x) and
A4: for x be Element of X holds g.x = Class(RI,x);
now
let x be Element of X;
f.x = Class(RI,x) by A3;
hence f.x = g.x by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
begin :: 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 object st y in the carrier of Y ex x being object st x in the
carrier of X & y = f.x
proof
let y be object;
assume
A1: y in the carrier of Y;
then reconsider y as Element of Y;
consider x being object such that
A2: x in the carrier of X and
A3: y = Class(RI,x) by A1,EQREL_1:def 3;
take x;
thus thesis by A2,A3,Def10;
end;
then rng f = the carrier of Y by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
theorem Th50:
I=Ker f implies ex h being BCI-homomorphism of X./.RI,X9 st f =
h*nat_hom(RI) & h is one-to-one
proof
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: dom(nat_hom(RI)) = the carrier of X by FUNCT_2:def 1;
assume
A2: I = Ker f;
A3: for x being Element of J ex y being Element of X9 st P[x,y]
proof
let x be Element of J;
x in Class(RI);
then consider y being object such that
A4: y in the carrier of X and
A5: x = Class(RI,y) by EQREL_1:def 3;
reconsider y as Element of X by A4;
reconsider t=f.y as Element of X9;
take t;
let a be Element of X;
assume x = Class(RI,a);
then y in Class(RI,a) by A5,EQREL_1:23;
then
A6: [a,y] in RI by EQREL_1:18;
then y\a in Ker f by A2,BCIALG_2:def 12;
then ex x2 being Element of X st y\a=x2 & f.x2=0.X9;
then
A7: f.y\f.a=0.X9 by Def6;
a\y in Ker f by A2,A6,BCIALG_2:def 12;
then ex x1 being Element of X st a\y=x1 & f.x1=0.X9;
then f.a\f.y=0.X9 by Def6;
hence thesis by A7,BCIALG_1:def 7;
end;
consider h being Function of J,X9 such that
A8: for x being Element of J holds P[x,h.x] from FUNCT_2:sch 3(A3);
now
let a,b be Element of J;
a in Class(RI);
then consider a1 being object such that
A9: a1 in the carrier of X and
A10: a = Class(RI,a1) by EQREL_1:def 3;
b in Class(RI);
then consider b1 being object such that
A11: b1 in the carrier of X and
A12: b = Class(RI,b1) by EQREL_1:def 3;
reconsider a1,b1 as Element of X by A9,A11;
A13: a\b=Class(RI,a1\b1) by A10,A12,BCIALG_2:def 17;
A14: h.b = f.b1 by A8,A12;
h.a = f.a1 by A8,A10;
then h.a\h.b =f.(a1\b1) by A14,Def6;
hence h.a\h.b=h.(a\b) by A8,A13;
end;
then reconsider h as BCI-homomorphism of X./.RI,X9 by Def6;
A15: h is one-to-one
proof
let y1,y2 be object;
assume that
A16: y1 in dom h & y2 in dom h and
A17: h.y1 = h.y2;
reconsider S=y1,T=y2 as Element of J by A16;
S in Class(RI);
then consider a1 being object such that
A18: a1 in the carrier of X and
A19: S = Class(RI,a1) by EQREL_1:def 3;
T in Class(RI);
then consider b1 being object such that
A20: b1 in the carrier of X and
A21: T = Class(RI,b1) by EQREL_1:def 3;
reconsider a1,b1 as Element of X by A18,A20;
A22: h.T = f.b1 by A8,A21;
A23: h.S = f.a1 by A8,A19;
then f.b1\f.a1=0.X9 by A17,A22,BCIALG_1:def 5;
then f.(b1\a1)=0.X9 by Def6;
then
A24: b1\a1 in Ker f;
f.a1\f.b1=0.X9 by A17,A23,A22,BCIALG_1:def 5;
then f.(a1\b1)=0.X9 by Def6;
then a1\b1 in Ker f;
then [a1,b1] in RI by A2,A24,BCIALG_2:def 12;
then b1 in Class(RI,a1) by EQREL_1:18;
hence thesis by A19,A21,EQREL_1:23;
end;
A25: dom f = the carrier of X by FUNCT_2:def 1;
A26: now
let x be object;
thus x in dom f implies x in dom nat_hom RI & (nat_hom RI).x in dom h
proof
assume
A27: x in dom f;
hence x in dom nat_hom RI by A1;
A28: dom h = the carrier of X./.RI by FUNCT_2:def 1;
(nat_hom RI).x in rng nat_hom RI by A1,A27,FUNCT_1:def 3;
hence thesis by A28;
end;
assume that
A29: x in dom nat_hom RI and
(nat_hom RI).x in dom h;
thus x in dom f by A25,A29;
end;
take h;
now
let x be object;
assume x in dom f;
then reconsider a = x as Element of X;
(nat_hom RI).a = Class(RI,a) by Def10;
hence f.x = h.((nat_hom RI).x) by A8;
end;
hence thesis by A15,A26,FUNCT_1:10;
end;
::$CT
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 object;
assume y in Ker h;
then consider x being Element of X such that
A1: y=x and
A2: h.x = 0.Y;
Class(RK,0.X)=Class(RK,x) by A2,Def10;
then x in Class(RK,0.X) by EQREL_1:23;
then [0.X,x] in RK by EQREL_1:18;
then x\0.X in K by BCIALG_2:def 12;
hence thesis by A1,BCIALG_1:2;
end;
let y be object;
assume
A3: y in K;
then reconsider x=y as Element of X;
x\0.X in K & x` in K by A3,BCIALG_1:2,def 19;
then [0.X,x] in RK by BCIALG_2:def 12;
then x in Class(RK,0.X) by EQREL_1:18;
then Class(RK,0.X)=Class(RK,x) by EQREL_1:23;
then h.x =0.Y by Def10;
hence thesis;
end;
Lm4: the carrier of H9 = rng f implies f is BCI-homomorphism of X,H9
proof
A1: the carrier of X=dom f by FUNCT_2:def 1;
assume the carrier of H9 = rng f;
then reconsider h=f as Function of X,H9 by A1,RELSET_1:4;
now
let a,b be Element of X;
h.a\h.b=f.a\f.b by Th34;
hence h.(a\b) = h.a\h.b by Def6;
end;
hence thesis by Def6;
end;
begin :: First Isomorphism Theorem
theorem
I = Ker f & the carrier of H9 = rng f implies X./.RI,H9 are_isomorphic
proof
assume that
A1: I = Ker f and
A2: the carrier of H9 = rng f;
defpred P[set,set] means for a being Element of X st $1=Class(RI,a) holds $2
= f.a;
set J = X./.RI;
A3: for x being Element of J ex y being Element of H9 st P[x,y]
proof
let x be Element of J;
x in Class(RI);
then consider y being object such that
A4: y in the carrier of X and
A5: x = Class(RI,y) by EQREL_1:def 3;
reconsider y as Element of X by A4;
dom f = the carrier of X by FUNCT_2:def 1;
then reconsider t=f.y as Element of H9 by A2,FUNCT_1:def 3;
take t;
let a be Element of X;
assume x = Class(RI,a);
then y in Class(RI,a) by A5,EQREL_1:23;
then
A6: [a,y] in RI by EQREL_1:18;
then y\a in Ker f by A1,BCIALG_2:def 12;
then ex x2 being Element of X st y\a=x2 & f.x2=0.X9;
then
A7: f.y\f.a=0.X9 by Def6;
a\y in Ker f by A1,A6,BCIALG_2:def 12;
then ex x1 being Element of X st a\y=x1 & f.x1=0.X9;
then f.a\f.y=0.X9 by Def6;
hence thesis by A7,BCIALG_1:def 7;
end;
consider h being Function of J,H9 such that
A8: for x being Element of J holds P[x,h.x] from FUNCT_2:sch 3(A3);
now
reconsider f as BCI-homomorphism of X,H9 by A2,Lm4;
let a,b be Element of J;
a in Class(RI);
then consider a1 being object such that
A9: a1 in the carrier of X and
A10: a = Class(RI,a1) by EQREL_1:def 3;
b in Class(RI);
then consider b1 being object such that
A11: b1 in the carrier of X and
A12: b = Class(RI,b1) by EQREL_1:def 3;
reconsider a1,b1 as Element of X by A9,A11;
A13: a\b=Class(RI,a1\b1) by A10,A12,BCIALG_2:def 17;
A14: h.b = f.b1 by A8,A12;
h.a = f.a1 by A8,A10;
then h.a \ h.b =f.(a1\b1) by A14,Def6;
hence h.a\h.b=h.(a\b) by A8,A13;
end;
then reconsider h as BCI-homomorphism of X./.RI,H9 by Def6;
A15: h is one-to-one
proof
let y1,y2 be object;
assume that
A16: y1 in dom h & y2 in dom h and
A17: h.y1 = h.y2;
reconsider y1,y2 as Element of J by A16;
y1 in Class(RI);
then consider a1 being object such that
A18: a1 in the carrier of X and
A19: y1 = Class(RI,a1) by EQREL_1:def 3;
y2 in Class(RI);
then consider b1 being object such that
A20: b1 in the carrier of X and
A21: y2 = Class(RI,b1) by EQREL_1:def 3;
reconsider a1,b1 as Element of X by A18,A20;
A22: h.y2 = f.b1 by A8,A21;
A23: h.y1 = f.a1 by A8,A19;
then f.b1\f.a1=0.X9 by A17,A22,BCIALG_1:def 5;
then f.(b1\a1)=0.X9 by Def6;
then
A24: b1\a1 in Ker f;
f.a1\f.b1=0.X9 by A17,A23,A22,BCIALG_1:def 5;
then f.(a1\b1)=0.X9 by Def6;
then a1\b1 in Ker f;
then [a1,b1] in RI by A1,A24,BCIALG_2:def 12;
then b1 in Class(RI,a1) by EQREL_1:18;
hence thesis by A19,A21,EQREL_1:23;
end;
the carrier of H9 c= rng h
proof
let y be object;
A25: the carrier of J = dom h by FUNCT_2:def 1;
assume y in the carrier of H9;
then consider x being object such that
A26: x in dom f and
A27: y=f.x by A2,FUNCT_1:def 3;
reconsider S=Class(RI,x) as Element of J by A26,EQREL_1:def 3;
h.S = f.x by A8,A26;
hence thesis by A27,A25,FUNCT_1:def 3;
end;
then rng h = the carrier of H9;
then h is onto by FUNCT_2:def 3;
hence thesis by A15;
end;
theorem Th53:
I = Ker f & f is onto implies X./.RI,X9 are_isomorphic
proof
assume that
A1: I = Ker f and
A2: f is onto;
consider h being BCI-homomorphism of X./.RI,X9 such that
A3: f=h*nat_hom(RI) and
A4: h is one-to-one by A1,Th50;
for y being object st y in the carrier of X9 ex z being object st z in
the carrier of X./.RI&h.z = y
proof
let y be object;
assume y in the carrier of X9;
then y in rng f by A2,FUNCT_2:def 3;
then consider x being object such that
A5: x in dom f and
A6: y=f.x by FUNCT_1:def 3;
take (nat_hom RI).x;
A7: dom(nat_hom(RI)) = the carrier of X by FUNCT_2:def 1;
then (nat_hom RI).x in rng nat_hom RI by A5,FUNCT_1:def 3;
hence thesis by A3,A5,A6,A7,FUNCT_1:13;
end;
then rng h = the carrier of X9 by FUNCT_2:10;
then h is onto by FUNCT_2:def 3;
hence thesis by A4;
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 Z2={Class(RK,a) where a is Element of G:Class(RK,a) in the carrier of
X./.RK};
set Z1 =union{Class(RK,a) where a is Element of G:Class(RK,a) in the
carrier of X./.RK};
A1: now
let x be object;
assume x in Z1;
then consider g being set such that
A2: x in g and
A3: g in Z2 by TARSKI:def 4;
ex a being Element of G st g=Class(RK,a) & Class(RK,a) in the carrier
of X./.RK by A3;
hence x in the carrier of X by A2;
end;
0.X = 0.G by BCIALG_1:def 10;
then
A4: Class(RK,0.X) in Z2;
[0.X,0.X] in RK by EQREL_1:5;
then 0.X in Class(RK,0.X) by EQREL_1:18;
hence thesis by A4,A1,TARSKI:def 3,def 4;
end;
end;
::P72
Lm5: for w being Element of Union(G,RK) holds ex a being Element of G st w in
Class(RK,a)
proof
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
A1: w in g and
A2: g in Z2 by TARSKI:def 4;
consider a being Element of G such that
A3: g=Class(RK,a) and
Class(RK,a) in the carrier of X./.RK by A2;
take a;
thus thesis by A1,A3;
end;
definition
let X,G,K,RK;
func HKOp(G,RK) -> BinOp of Union(G,RK) means
:Def12:
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
A2: w1 in Class(RK,a) by Lm5;
A3: [a,w1] in RK by A2,EQREL_1:18;
consider b being Element of G such that
A4: w2 in Class(RK,b) by Lm5;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider a1=a,b1=b as Element of X;
Class(RK,a1\b1) in the carrier of X./.RK by EQREL_1:def 3;
then Class(RK,a\b) in the carrier of X./.RK by Th34;
then
A5: Class(RK,a\b) in {Class(RK,c) where c is Element of G: Class(RK,c)
in the carrier of X./.RK};
A6: [b,w2] in RK by A4,EQREL_1:18;
reconsider w1,w2 as Element of X;
[a1\b1,w1\w2] in RK by A3,A6,BCIALG_2:def 9;
then w1\w2 in Class(RK,a1\b1) by EQREL_1:18;
then w1\w2 in Class(RK,a\b) by Th34;
then reconsider C = w1\w2 as Element of Union(G,RK) by A5,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
A7: 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
A8: 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 A7;
hence o1.(w1,w2)=o2.(w1,w2) by A8;
end;
hence thesis;
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 0.G in Class(RK,0.G) & Class(RK,0.G) in {Class(RK,c) where c is
Element of G: Class(RK,c) in the carrier of X./.RK} by EQREL_1:20;
hence thesis by A1,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 Th54:
HK(G,RK) is BCI-algebra
proof
reconsider IT = HK(G,RK) as non empty BCIStr_0;
A1: IT is being_BCI-4
proof
let x,y be Element of IT;
reconsider x1=x,y1=y as Element of Union(G,RK);
reconsider x2=x1,y2=y1 as Element of X;
assume x\y=0.IT & y\x=0.IT;
then x2\y2 = 0.X & y2\x2 = 0.X by Def12;
hence thesis by BCIALG_1:def 7;
end;
A2: 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;
x2\y2 = x1\y1 & z2\y2=z1\y1 by Def12;
then
A3: (x2\y2)\(z2\y2) = x1\y1\(z1\y1) by Def12;
x2\z2=x1\z1 by Def12;
then ((x2\y2)\(z2\y2))\(x2\z2)=((x1\y1)\(z1\y1))\(x1\z1)by A3,Def12;
hence ((x\y)\(z\y))\(x\z)=0.IT by BCIALG_1:def 3;
end;
A4: IT is being_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\z2=x1\z1 by Def12;
then
A5: (x2\z2)\y2=(x1\z1)\y1 by Def12;
x2\y2 = x1\y1 by Def12;
then (x2\y2)\z2 = (x1\y1)\z1 by Def12;
then ((x2\y2)\z2)\((x2\z2)\y2)=((x1\y1)\z1)\((x1\z1)\y1) by A5,Def12;
hence thesis by BCIALG_1:def 4;
end;
IT is being_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 Def12;
hence thesis by BCIALG_1:def 5;
end;
hence thesis by A2,A4,A1,BCIALG_1:def 3;
end;
registration
let X,G,K,RK;
cluster HK(G,RK) -> strict being_B being_C being_I being_BCI-4;
coherence by Th54;
end;
theorem Th55:
HK(G,RK) is SubAlgebra of X
proof
set IT = HK(G,RK);
set V1=the carrier of IT;
reconsider D = V1 as non empty set;
set A = (the InternalDiff of X)||V1;
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:] by RELAT_1:61;
then
A1: dom A = [:D,D:] by XBOOLE_1:28,ZFMISC_1:96;
for y being object holds y in D iff
ex z being object st z in dom A & y = A.z
proof
let y be object;
A2: now
given z being set such that
A3: z in dom A and
A4: y = A.z;
consider x1,x2 being object such that
A5: x1 in D & x2 in D and
A6: z = [x1,x2] by A1,A3,ZFMISC_1:def 2;
reconsider x1,x2 as Element of Union(G,RK) by A5;
reconsider v1 = x1, v2 = x2 as Element of VV;
y = v1\v2 by A3,A4,A6,FUNCT_1:47;
then y = x1\x2 by Def12;
hence y in D;
end;
y in D implies ex z being set st z in dom A & y = A.z
proof
assume
A7: y in D;
then reconsider y1=y,y2=0.IT as Element of X;
A8: [y,0.IT] in [:D,D:] by A7,ZFMISC_1:87;
then A.[y,0.IT] = y1\y2 by FUNCT_1:49
.= y by BCIALG_1:2;
hence thesis by A1,A8;
end;
hence thesis by A2;
end;
then rng A = D by FUNCT_1:def 3;
then reconsider A as BinOp of V1 by A1,FUNCT_2:def 1,RELSET_1:4;
set B = the InternalDiff of IT;
now
let x,y be Element of V1;
x in V1 & y in V1;
then reconsider vx=x,vy=y as Element of VV;
[x,y] in [:V1,V1:] by ZFMISC_1:def 2;
then A.(x,y)=vx\vy by FUNCT_1:49;
hence A.(x,y)=B.(x,y) by Def12;
end;
then 0.IT = 0.X & A=B;
hence thesis by 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: 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 that
A2: x\y in GK and
A3: y in GK;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider x1=x,y1=y as Element of X;
x\y in K by A2,XBOOLE_0:def 4;
then
A4: x1\y1 in K by Th34;
y1 in K by A3,XBOOLE_0:def 4;
then x in K by A4,BCIALG_1:def 18;
hence thesis by XBOOLE_0:def 4;
end;
A5: 0.G = 0.X by BCIALG_1:def 10;
then
A6: 0.G in K by BCIALG_1:def 18;
then
A7: 0.G in GK by XBOOLE_0:def 4;
for x being object st x in GK holds x in the carrier of G by XBOOLE_0:def 4;
then GK is non empty Subset of G by A6,TARSKI:def 3,XBOOLE_0:def 4;
then reconsider GK as Ideal of G by A7,A1,BCIALG_1:def 18;
for x being Element of GK holds x` in GK
proof
let x be Element of GK;
A8: x in K by XBOOLE_0:def 4;
then reconsider y=x as Element of X;
y` in K by A8,BCIALG_1:def 19;
then x` in K by A5,Th34;
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 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 that
A1: RK1=RK and
A2: I=(the carrier of G)/\K;
defpred P[Element of G,set] means $2 = Class(RK1,$1);
A3: the carrier of G c= the carrier of HK(G,RK)
proof
let xx be object;
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
A4: x in the carrier of X;
then Class(RK,x) in the carrier of X./.RK by EQREL_1:def 3;
then
A5: Class(RK,x) in {Class(RK,a) where a is Element of G:Class(RK,a) in
the carrier of X./.RK};
[x,x] in RK by A4,EQREL_1:5;
then x in Class(RK,x) by EQREL_1:18;
hence thesis by A5,TARSKI:def 4;
end;
A6: 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 3;
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(A6);
now
let a,b be Element of G;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider xa=a,xb=b as Element of X;
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 3;
reconsider a1=a,b1=b as Element of HK(G,RK) by A3;
Wa=f.a & Wb=f.b by A7;
then
A8: f.a\f.b=Class(RK1,a1\b1) by BCIALG_2:def 17;
HK(G,RK) is SubAlgebra of X by Th55;
then xa\xb=a1\b1 by Th34;
then f.a\f.b=Class(RK1,a\b) by A8,Th34;
hence f.(a\b)=f.a\f.b by A7;
end;
then reconsider f as BCI-homomorphism of G, HK(G,RK)./.RK1 by Def6;
A9: Ker f = I
proof
set X9 = HK(G,RK)./.RK1;
thus Ker f c= I
proof
let h be object;
assume h in Ker f;
then consider x being Element of G such that
A10: h=x and
A11: f.x = 0.X9;
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,A7,A11;
then 0.X in Class(RK,x) by EQREL_1:23;
then [x,0.X] in RK by EQREL_1:18;
then
A12: x\0.X in K by BCIALG_2:def 12;
x in K by A12,BCIALG_1:def 18;
hence thesis by A2,A10,XBOOLE_0:def 4;
end;
let h be object;
assume
A13: h in I;
then reconsider x=h as Element of X by A2;
h in K by A2,A13,XBOOLE_0:def 4;
then x\0.X in K & x` in K by BCIALG_1:2,def 19;
then [x,0.X] in RK by BCIALG_2:def 12;
then 0.X in Class(RK,x) by EQREL_1:18;
then Class(RK1,h)= Class(RK1,0.X)by A1,EQREL_1:23;
then f.h = 0.X9 by A7,A13;
hence thesis by A13;
end;
now
let y be object;
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 object such that
A14: x in the carrier of HK(G,RK) and
A15: y=Class(RK1,x) by EQREL_1:def 3;
consider a being Element of G such that
A16: x in Class(RK,a) by A14,Lm5;
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 A1,A15,A16,EQREL_1:23;
then
A17: y=f.a by A7;
dom f = the carrier of G by FUNCT_2:def 1;
hence thesis by A17,FUNCT_1:def 3;
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;
then f is onto by FUNCT_2:def 3;
hence thesis by A9,Th53;
end;