:: Isomorphisms of Direct Products of Finite Cyclic Groups
:: by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 27, 2012
:: Copyright (c) 2012-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 FINSEQ_1, FUNCT_1, RELAT_1, CARD_3, TARSKI, BINOP_2, FINSET_1,
XXREAL_0, GROUP_2, CARD_1, NUMBERS, ALGSTR_0, FUNCT_2, SUBSET_1,
XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3,
RLVECT_1, SUPINF_2, PRVECT_1, INT_3, XCMPLX_0, INT_1, INT_6, ZFMISC_1,
VECTSP_1, FUNCSDOM, GROUP_6, GROUP_14, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, CARD_1,
XTUPLE_0, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, CARD_3, FINSEQ_1, RVSUM_1,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1, GR_CY_1, PRVECT_1,
INT_3, INT_6, PRVECT_3, WSIERP_1, MOD_4;
constructors REALSET1, MONOID_0, PRALG_1, GROUP_4, GROUP_7, FUNCT_7, RELSET_1,
REAL_1, SQUARE_1, RUSUB_4, ALGSTR_1, CARD_2, PRVECT_2, NAT_D, LOPBAN_1,
XTUPLE_0, BINOP_2, FINSEQ_4, FINSEQOP, PRVECT_3, SETWISEO, BINOM, INT_3,
INT_6, POLYNOM1, WELLORD2, WSIERP_1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, ORDINAL1, NAT_1, FUNCT_2, CARD_1,
CARD_3, XXREAL_0, RELSET_1, FINSEQ_1, MEMBERED, FUNCT_1, VALUED_0,
ALGSTR_0, PRVECT_1, INT_1, INT_6, RLVECT_1, PRVECT_3, RELAT_1, SUBSET_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin
registration
let G be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr;
cluster <* G *> -> non empty AbGroup-yielding for FinSequence;
end;
registration
let G,F be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr;
cluster <* G,F *> -> non empty AbGroup-yielding for FinSequence;
end;
theorem :: GROUP_14:1
for X be AbGroup holds
ex I being Homomorphism of X,product <*X*>
st I is bijective & (for x be Element of X holds I.x = <*x*>);
registration
let G,F be non empty AbGroup-yielding FinSequence;
cluster G^F -> AbGroup-yielding;
end;
theorem :: GROUP_14:2
for X,Y be AbGroup holds
ex I be Homomorphism of [:X,Y:],product <*X,Y*> st I is bijective &
(for x be Element of X, y be Element of Y holds I.(x,y) = <*x,y*>);
theorem :: GROUP_14:3
for X,Y be Group-Sequence holds
ex I be Homomorphism of [:product X,product Y:],product (X^Y)
st I is bijective &
(for x be Element of product X, y be Element of product Y holds
ex x1,y1 be FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1);
theorem :: GROUP_14:4
for G,F be AbGroup holds
(for x be set holds x is Element of product <*G,F*> iff
ex x1 be Element of G, x2 be Element of F st x = <* x1,x2 *>) &
(for x,y be Element of product <*G,F*>, x1,y1 be Element of G,
x2,y2 be Element of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x+y = <*x1+y1,x2+y2*>) & 0.(product <*G,F*>) = <* 0.G,0.F *> &
(for x be Element of product <*G,F*>, x1 be Element of G, x2 be Element of F
st x = <* x1,x2 *> holds -x = <* -x1,-x2 *>);
theorem :: GROUP_14:5
for G,F be AbGroup holds
(for x be set holds x is Element of [:G,F:] iff ex x1 be Element of G,
x2 be Element of F st x = [x1,x2]) &
(for x,y be Element of [:G,F:], x1,y1 be Element of G, x2,y2 be Element of F
st x = [x1,x2] & y = [y1,y2] holds x+y = [x1+y1,x2+y2]) &
0.[:G,F:] = [0.G,0.F] &
(for x be Element of [:G,F:], x1 be Element of G, x2 be Element of F
st x = [x1,x2] holds -x = [-x1,-x2]);
theorem :: GROUP_14:6
for G,H,I being AddGroup, h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
h1 * h is Homomorphism of G,I;
definition
let G,H,I be AddGroup;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
redefine func h1 * h -> Homomorphism of G,I;
end;
theorem :: GROUP_14:7
for G,H being AddGroup, h being Homomorphism of G,H st h is bijective holds
h" is Homomorphism of H,G;
theorem :: GROUP_14:8
for X,Y be Group-Sequence holds
ex I be Homomorphism of product <* product X,product Y *>,product (X^Y)
st I is bijective &
(for x be Element of product X, y be Element of product Y holds
ex x1,y1 be FinSequence st x = x1 & y = y1 & I.<*x,y*> = x1^y1);
theorem :: GROUP_14:9
for X,Y be AbGroup holds
ex I be Homomorphism of [:X,Y:],[:X,product <*Y*>:] st I is bijective &
(for x be Element of X, y be Element of Y holds I.(x,y) = [x,<*y*>]);
theorem :: GROUP_14:10
for X be Group-Sequence, Y be AbGroup holds
ex I be Homomorphism of [:product X,Y:],product(X^<*Y*>) st I is bijective &
(for x be Element of product X, y be Element of Y ex x1,y1 be FinSequence
st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1);
theorem :: GROUP_14:11
for n be non zero Nat holds
the addLoopStr of INT.Ring n is non empty Abelian right_complementable
add-associative right_zeroed;
definition
let n be natural Number;
func Z/Z n -> addLoopStr equals
:: GROUP_14:def 1
the addLoopStr of INT.Ring n;
end;
registration
let n be non zero natural Number;
cluster Z/Z n -> non empty strict;
end;
registration
let n be non zero natural Number;
cluster Z/Z n -> Abelian right_complementable add-associative right_zeroed;
end;
theorem :: GROUP_14:12
for X be Group-Sequence, x,y,z be Element of product X,
x1,y1,z1 be FinSequence st x = x1 & y = y1 & z = z1 holds
z = x+y iff for j be Element of dom carr X holds
z1.j = (the addF of (X.j)).((x1.j),(y1.j));
theorem :: GROUP_14:13
for m being CR_Sequence, j being Nat, x be Integer st j in dom m
holds (x mod Product(m)) mod m.j = x mod m.j;
theorem :: GROUP_14:14
for m being CR_Sequence, X be Group-Sequence st len m = len X &
(for i be Element of NAT st i in dom X holds ex mi be non zero Nat
st mi = m.i & X.i = Z/Z (mi)) holds
ex I being Homomorphism of Z/Z (Product(m)),product X
st (for x be Integer st x in the carrier of Z/Z (Product(m)) holds
I.x = mod(x,m));
theorem :: GROUP_14:15
for X,Y be non empty set ex I be Function of [:X,Y:],[:X,product<*Y*>:]
st I is one-to-one onto &
(for x,y be set st x in X & y in Y holds I.(x,y) = [x,<*y*>]);
theorem :: GROUP_14:16
for X be non empty set holds card(product <*X*>) = card X;
theorem :: GROUP_14:17
for X be non-empty non empty FinSequence, Y be non empty set
ex I be Function of [:product X,Y:],product(X^<*Y*>)
st I is one-to-one onto &
(for x,y be set st x in product X & y in Y ex x1,y1 be FinSequence
st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1);
theorem :: GROUP_14:18
for m being FinSequence of NAT, X being non-empty non empty FinSequence
st len m = len X &
(for i be Element of NAT st i in dom X holds card(X.i) = m.i) holds
card(product X) = Product(m);
theorem :: GROUP_14:19
for m being CR_Sequence, X be Group-Sequence st len m = len X &
(for i be Element of NAT st i in dom X holds ex mi be non zero Nat
st mi = m.i & X.i = Z/Z (mi)) holds
card(the carrier of product X) = Product(m);
theorem :: GROUP_14:20
for m being CR_Sequence, X be Group-Sequence,
I be Function of Z/Z (Product(m)),product X st len m = len X &
(for i be Element of NAT st i in dom X holds ex mi be non zero Nat
st mi = m.i & X.i = Z/Z (mi)) &
(for x be Integer st x in the carrier of Z/Z (Product(m)) holds
I.x = mod(x,m)) holds
I is one-to-one;
theorem :: GROUP_14:21
for m being CR_Sequence, X be Group-Sequence st len m = len X &
(for i be Element of NAT st i in dom X holds ex mi be non zero Nat
st mi = m.i & X.i = Z/Z (mi)) holds
ex I being Homomorphism of Z/Z (Product(m)),product X st I is bijective &
(for x be Integer st x in the carrier of Z/Z (Product(m)) holds
I.x = mod(x,m));