:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008-2016 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;
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
:: BCIALG_6:def 1
for x being Element of G holds it.(x,0)=0.G &
for n holds it.(x,n + 1) = x\(it.(x,n))`;
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
:: BCIALG_6:def 2
BCI-power(X).(x,|.i.|) if 0 <= i
otherwise (BCI-power(X).(x`,|.i.|));
end;
definition
let X,x; let n be natural Number;
redefine func x |^ n equals
:: BCIALG_6:def 3
BCI-power(X).(x,n);
end;
theorem :: BCIALG_6:1
a\(x\b) = b\(x\a);
theorem :: BCIALG_6:2
x |^ (n+1) = x\(x |^ n )`;
theorem :: BCIALG_6:3
x |^ 0 = 0.X;
theorem :: BCIALG_6:4
x |^ 1 = x;
theorem :: BCIALG_6:5
x |^ -1 = x`;
theorem :: BCIALG_6:6
x |^ 2 = x\x`;
theorem :: BCIALG_6:7
0.X |^ n = 0.X;
::P18-theorem 1.4.2(1-4)
theorem :: BCIALG_6:8
(a |^ (-1))|^ (-1) = a;
theorem :: BCIALG_6:9
x |^(-n) =(x``)|^(-n);
theorem :: BCIALG_6:10
a` |^ n = a |^ -n;
theorem :: BCIALG_6:11
x in BCK-part(X) & n>=1 implies x|^n = x;
theorem :: BCIALG_6:12
x in BCK-part(X) implies x|^ (-n) = 0.X;
::P19 theorem 1.4.3
theorem :: BCIALG_6:13
a|^i in AtomSet(X);
theorem :: BCIALG_6:14
(a|^(n+1))` = (a|^n)`\a;
theorem :: BCIALG_6:15
(a\b)|^n = a|^n\(b|^n);
theorem :: BCIALG_6:16
(a\b)|^(-n) = a|^(-n)\(b|^(-n));
theorem :: BCIALG_6:17
a`|^n = (a|^n)`;
theorem :: BCIALG_6:18
x`|^n = (x|^n)`;
theorem :: BCIALG_6:19
a`|^(-n) = (a|^(-n))`;
theorem :: BCIALG_6:20
a=(x``)|^n implies x|^n in BranchV(a);
theorem :: BCIALG_6:21
(x|^n)` = ((x``)|^n)`;
theorem :: BCIALG_6:22
a|^i \ a|^j = a|^(i-j);
::1.4.11
theorem :: BCIALG_6:23
(a|^i)|^j = a|^(i*j);
theorem :: BCIALG_6:24
a|^(i+j) = a|^i\(a|^j)`;
definition
let X,x;
attr x is finite-period means
:: BCIALG_6:def 4
ex n being Element of NAT st n<>0 & x|^ n in BCK-part(X);
end;
theorem :: BCIALG_6:25
x is finite-period implies x`` is finite-period;
definition
let X,x such that
x is finite-period;
func ord x -> Element of NAT means
:: BCIALG_6:def 5
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;
end;
theorem :: BCIALG_6:26
a is finite-period & ord a = n implies a|^n = 0.X;
theorem :: BCIALG_6:27
X is BCK-algebra iff for x holds x is finite-period & ord x = 1;
theorem :: BCIALG_6:28
x is finite-period & a is finite-period & x in BranchV(a)
implies ord x = ord a;
theorem :: BCIALG_6:29 ::1.5.3
x is finite-period & ord x = n implies(x|^m in BCK-part(X) iff n divides m);
theorem :: BCIALG_6:30 ::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);
theorem :: BCIALG_6:31
x is finite-period & x` is finite-period implies ord x = ord(x`);
theorem :: BCIALG_6:32
x\y is finite-period & x in BranchV(a) & y in BranchV(a) implies ord(x \y)=1;
theorem :: BCIALG_6:33
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);
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 :: BCIALG_6:34
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;
definition
let X,X9 be non empty BCIStr_0;
let f be Function of X,X9;
attr f is multiplicative means
:: BCIALG_6:def 6
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;
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
:: BCIALG_6:def 7
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
:: BCIALG_6:def 8
{x where x is Element of X:f.x=0.X9};
end;
theorem :: BCIALG_6:35
f.(0.X) = 0.X9;
registration
let X,X9,f;
cluster Ker f -> non empty;
end;
theorem :: BCIALG_6:36
x <= y implies f.x <= f.y;
theorem :: BCIALG_6:37
f is one-to-one iff Ker(f) = {0.X};
theorem :: BCIALG_6:38
f is bijective & g=f" implies g is bijective;
theorem :: BCIALG_6:39
h*f is BCI-homomorphism of X,Y;
theorem :: BCIALG_6:40
for Z being SubAlgebra of X9 st the carrier of Z = rng f holds f is
BCI-homomorphism of X,Z;
theorem :: BCIALG_6:41
Ker f is closed Ideal of X;
registration
let X,X9,f;
cluster Ker f -> closed for Ideal of X;
end;
theorem :: BCIALG_6:42
f is onto implies for c being Element of X9 ex x st c = f.x;
::P75
theorem :: BCIALG_6:43
for a being Element of X st a is minimal holds f.a is minimal;
theorem :: BCIALG_6:44
for a being Element of AtomSet(X),b being Element of AtomSet(X9)st b=f
.a holds f.:BranchV(a) c= BranchV(b);
::P76
theorem :: BCIALG_6:45
A9 is Ideal of X9 implies f"A9 is Ideal of X;
theorem :: BCIALG_6:46
A9 is closed Ideal of X9 implies f"A9 is closed Ideal of X;
theorem :: BCIALG_6:47
f is onto implies f.:I is Ideal of X9;
theorem :: BCIALG_6:48
f is onto implies f.:CI is closed Ideal of X9;
definition
let X,X9 be BCI-algebra;
pred X,X9 are_isomorphic means
:: BCIALG_6:def 9
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;
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
:: BCIALG_6:def 10
for x holds it.x = Class(RI,x);
end;
begin :: Fundamental Theorem of Homomorphisms
:: f
:: X--------->X'
:: | /
:: g| / h
:: | /
:: | /
:: | /
:: V /
:: X/Ker(f)
theorem :: BCIALG_6:49
nat_hom RI is onto;
theorem :: BCIALG_6:50
I=Ker f implies ex h being BCI-homomorphism of X./.RI,X9 st f =
h*nat_hom(RI) & h is one-to-one;
::$CT
theorem :: BCIALG_6:52
Ker(nat_hom RK) = K;
begin :: First Isomorphism Theorem
theorem :: BCIALG_6:53
I = Ker f & the carrier of H9 = rng f implies X./.RI,H9 are_isomorphic;
theorem :: BCIALG_6:54
I = Ker f & f is onto implies X./.RI,X9 are_isomorphic;
begin :: Second Isomorphism Theorem
definition
let X,G,K,RK;
func Union(G,RK) -> non empty Subset of X equals
:: BCIALG_6:def 11
union{Class(RK,a) where a
is Element of G:Class(RK,a) in the carrier of X./.RK};
end;
definition
let X,G,K,RK;
func HKOp(G,RK) -> BinOp of Union(G,RK) means
:: BCIALG_6:def 12
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;
end;
definition
let X,G,K,RK;
func zeroHK(G,RK) -> Element of Union(G,RK) equals
:: BCIALG_6:def 13
0.X;
end;
definition
let X,G,K,RK;
func HK(G,RK) -> BCIStr_0 equals
:: BCIALG_6:def 14
BCIStr_0(#Union(G,RK),HKOp(G,RK),zeroHK(G,
RK) #);
end;
registration
let X,G,K,RK;
cluster HK(G,RK) -> non empty;
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
:: BCIALG_6:def 15
HKOp(G,RK).(w1,w2);
end;
theorem :: BCIALG_6:55
HK(G,RK) is BCI-algebra;
registration
let X,G,K,RK;
cluster HK(G,RK) -> strict being_B being_C being_I being_BCI-4;
end;
theorem :: BCIALG_6:56
HK(G,RK) is SubAlgebra of X;
theorem :: BCIALG_6:57
(the carrier of G)/\K is closed Ideal of G;
theorem :: BCIALG_6:58
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;