:: Isomorphisms of Direct Products of Finite Cyclic Groups
:: by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 27, 2012
:: Copyright (c) 2012-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 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;
definitions PRVECT_1;
equalities FINSEQ_1, BINOP_1, ALGSTR_0, STRUCT_0, PRVECT_1, PRVECT_3, INT_3,
ORDINAL1;
expansions ALGSTR_0;
theorems FUNCT_1, CARD_3, FUNCT_2, TARSKI, FINSEQ_2, XREAL_1, ORDINAL1,
FINSEQ_1, FINSEQ_3, NAT_1, XBOOLE_0, RELAT_1, XXREAL_0, RLVECT_1,
RVSUM_1, RELSET_1, ALGSTR_0, PRVECT_1, PRVECT_3, ZFMISC_1, SUBSET_1,
CARD_1, INT_1, INT_3, INT_6, GR_CY_1, FINSEQ_5, NAT_D, PARTFUN3, CARD_2,
FINSEQ_4, WELLORD2, TOPGEN_5, MOD_4, VECTSP_1, XTUPLE_0, NDIFF_5;
schemes NAT_1, BINOP_1, FUNCT_2;
begin
registration
let G be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr;
cluster <* G *> -> non empty AbGroup-yielding for FinSequence;
correctness
proof
now let S be set;
assume S in rng <*G*>;
then consider i be object such that
A1: i in dom <*G*> & <*G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*G*> = {1} by FINSEQ_1:2,def 8;
then i = 1 by A1,TARSKI:def 1;
hence S is AbGroup by A1;
end;
hence thesis by PRVECT_1:def 10;
end;
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;
correctness
proof
now let S be set;
assume S in rng <*G,F*>;
then consider i be object such that
A1: i in dom <*G,F*> & <*G,F*>.i = S by FUNCT_1:def 3;
dom <*G,F*> = {1,2} by FINSEQ_1:2,89;
then i=1 or i=2 by A1,TARSKI:def 2;
hence S is AbGroup by A1;
end;
hence thesis by PRVECT_1:def 10;
end;
end;
theorem Th1:
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*>)
proof
let X be AbGroup;
set CarrX = the carrier of X;
consider I be Function of CarrX,product <*CarrX*> such that
A1: I is one-to-one & I is onto & (for x be object st x in CarrX holds
I.x = <*x*>) by PRVECT_3:4;
len carr <*X*> = len <*X*> by PRVECT_1:def 11;
then
A2: len carr <*X*> = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by FINSEQ_1:2,def 8;
A4: <*X*>.1 = X;
1 in {1} by TARSKI:def 1;
then (carr <*X*>).1 = the carrier of X by A3,A4,PRVECT_1:def 11;
then
A5: carr <*X*> = <* CarrX *> by A2,FINSEQ_1:40;
then reconsider I as Function of X,product <*X*>;
for v,w be Element of X holds I.(v+w) = I.v + I.w
proof
let v,w be Element of X;
A6: I.v = <*v*> & I.w = <*w*> & I.(v+w) = <*v+w*> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X*>;
1 in {1} by TARSKI:def 1;
then reconsider j1 = 1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A8: (addop <*X*>).j1 = the addF of (<*X*>.j1) by PRVECT_1:def 12;
A9: ([:addop <*X*>:].(Iv,Iw)).j1 = ((addop <*X*>).j1).(Iv.j1,Iw.j1)
by PRVECT_1:def 8
.= v+w by A8,A6;
consider Ivw be Function such that
A10: I.v + I.w = Ivw & dom Ivw = dom carr <*X*> & (for i be object st
i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i) by CARD_3:def 5;
A11: dom Ivw = Seg 1 by A2,A10,FINSEQ_1:def 3;
then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A11,FINSEQ_1:def 3;
hence thesis by A6,A10,A9,FINSEQ_1:40;
end;
then reconsider I as Homomorphism of X,product <*X*> by VECTSP_1:def 20;
take I;
thus thesis by A1,A5;
end;
registration
let G,F be non empty AbGroup-yielding FinSequence;
cluster G^F -> AbGroup-yielding;
correctness
proof
let S be set;
assume S in rng (G^F);
then consider i be object such that
A1: i in dom (G^F) & (G^F).i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
per cases by A1,FINSEQ_1:25;
suppose
A2: i in dom G;
then
A3: (G^F).i = G.i by FINSEQ_1:def 7;
G.i in rng G by A2,FUNCT_1:3;
hence S is AbGroup by A3,A1,PRVECT_1:def 10;
end;
suppose ex n be Nat st n in dom F & i=len G + n;
then consider n be Nat such that
A4: n in dom F & i=len G + n;
A5: (G^F).i = F.n by A4,FINSEQ_1:def 7;
F.n in rng F by A4,FUNCT_1:3;
hence S is AbGroup by A5,A1,PRVECT_1:def 10;
end;
end;
end;
theorem Th2:
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*>)
proof
let X,Y be AbGroup;
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
consider I be Function of [:CarrX,CarrY:],product <*CarrX,CarrY*> such that
A1: I is one-to-one & I is onto &
for x,y be object st x in CarrX & y in CarrY
holds I.(x,y) = <*x,y*> by PRVECT_3:5;
len carr <*X,Y*> = len <*X,Y*> by PRVECT_1:def 11;
then
A2: len carr <*X,Y*> = 2 by FINSEQ_1:44;
then
A3: dom carr <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
len <*X,Y*> = 2 by FINSEQ_1:44;
then
A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
A5: <*X,Y*>.1 = X & <*X,Y*>.2 = Y;
1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
then (carr <*X,Y*>).1 = CarrX & (carr <*X,Y*>).2 = CarrY
by A4,A5,PRVECT_1:def 11;
then
A6: carr <*X,Y*> = <* CarrX,CarrY *> by A2,FINSEQ_1:44;
then reconsider I as Function of [:X,Y:],product <*X,Y*>;
for v,w be Element of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Element of [:X,Y:];
consider x1 be Element of X, y1 be Element of Y such that
A7: v = [x1,y1] by SUBSET_1:43;
consider x2 be Element of X, y2 be Element of Y such that
A8: w = [x2,y2] by SUBSET_1:43;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A7,A8;
then
A9: I.v = <*x1,y1*> & I.w = <*x2,y2*> by A1;
A10: I.(v+w) =I.(x1+x2,y1+y2) by A7,A8,PRVECT_3:def 1
.= <* x1+x2,y1+y2 *> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X,Y*>;
reconsider j1=1, j2=2 as Element of dom (carr <*X,Y*>) by A3,TARSKI:def 2;
A12: (addop <*X,Y*>).j1 = the addF of (<*X,Y*>.j1) by PRVECT_1:def 12;
A13: ([:addop <*X,Y*>:].(Iv,Iw)).j1 = ((addop <*X,Y*>).j1).(Iv.j1,Iw.j1)
by PRVECT_1:def 8
.= x1+x2 by A12,A9;
A14: (addop <*X,Y*>).j2 = the addF of (<*X,Y*>.j2) by PRVECT_1:def 12;
A15: ([:addop <*X,Y*>:].(Iv,Iw)).j2 = ((addop <*X,Y*>).j2).(Iv.j2,Iw.j2)
by PRVECT_1:def 8
.= y1+y2 by A14,A9;
consider Ivw be Function such that
A16: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y*> & (for i be object st
i in dom carr <*X,Y*> holds Ivw.i in carr (<*X,Y*>).i) by CARD_3:def 5;
A17: dom Ivw = Seg 2 by A2,A16,FINSEQ_1:def 3;
then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A17,FINSEQ_1:def 3;
hence thesis by A10,A16,A13,A15,FINSEQ_1:44;
end;
then reconsider I as Homomorphism of [:X,Y:],product <*X,Y*>
by VECTSP_1:def 20;
take I;
thus thesis by A1,A6;
end;
theorem Th3:
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)
proof
let X,Y be Group-Sequence;
reconsider CX = carr X, CY = carr Y as non-empty FinSequence;
A1: len CX = len X & len CY = len Y & len carr (X^Y) = len (X^Y)
by PRVECT_1:def 11;
consider I be Function of [:product CX,product CY:],product (CX^CY)
such that
A2: I is one-to-one & I is onto & (for x,y be FinSequence st x in product CX &
y in product CY holds I.(x,y) = x^y) by PRVECT_3:6;
set PX = product X;
set PY = product Y;
len carr (X^Y) = len X + len Y & len (CX^CY) =len X + len Y
by A1,FINSEQ_1:22;
then
A3: dom carr (X^Y) = dom (CX^CY) by FINSEQ_3:29;
A4: for k be Nat st k in dom carr (X^Y) holds carr (X^Y).k = (CX^CY).k
proof
let k be Nat;
assume
A5: k in dom carr (X^Y);
then reconsider k1 = k as Element of dom (X^Y) by A1,FINSEQ_3:29;
A6: carr (X^Y).k = the carrier of ((X^Y).k1) by PRVECT_1:def 11;
A7: k in dom (X^Y) by A1,A5,FINSEQ_3:29;
per cases by A7,FINSEQ_1:25;
suppose
A8: k in dom X;
then
A9: k in dom CX by A1,FINSEQ_3:29;
reconsider k2 = k1 as Element of dom X by A8;
thus carr (X^Y).k = the carrier of (X.k2) by A6,FINSEQ_1:def 7
.= CX.k by PRVECT_1:def 11
.= (CX^CY).k by A9,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom Y & k=len X + n;
then consider n be Nat such that
A10: n in dom Y & k = len X + n;
A11: n in dom CY by A1,A10,FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A10;
thus carr (X^Y).k = the carrier of (Y.n1) by A6,A10,FINSEQ_1:def 7
.= CY.n by PRVECT_1:def 11
.= (CX^CY).k by A11,A10,A1,FINSEQ_1:def 7;
end;
end;
then
A12: carr (X^Y) = CX^CY by A3,FINSEQ_1:13;
reconsider I as Function of [:PX,PY:],product (X^Y) by A3,A4,FINSEQ_1:13;
A13: 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
proof
let x be Element of PX, y be Element of PY;
reconsider x1=x, y1=y as FinSequence by NDIFF_5:9;
I.(x,y) = x1^y1 by A2;
hence thesis;
end;
for v,w be Element of [:PX,PY:] holds I.(v+w) = I.v + I.w
proof
let v,w be Element of [:PX,PY:];
consider x1 be Element of PX, y1 be Element of PY such that
A14: v = [x1,y1] by SUBSET_1:43;
consider x2 be Element of PX, y2 be Element of PY such that
A15: w = [x2,y2] by SUBSET_1:43;
reconsider xx1=x1, xx2=x2 as FinSequence by NDIFF_5:9;
reconsider yy1=y1, yy2=y2 as FinSequence by NDIFF_5:9;
reconsider xx12=x1+x2, yy12=y1+y2 as FinSequence by NDIFF_5:9;
A16: dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX & dom yy1 =
dom CY & dom yy2 = dom CY & dom yy12 = dom CY by CARD_3:9;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A14,A15;
then
A17: I.v = xx1^yy1 & I.w = xx2^yy2 by A2;
I.(v+w) = I.(x1+x2,y1+y2) by A14,A15,PRVECT_3:def 1;
then
A18: I.(v+w) = xx12^yy12 by A2;
then
A19: dom (xx12^yy12) = dom carr (X^Y) by CARD_3:9;
reconsider Iv = I.v, Iw = I.w as Element of product carr (X^Y);
reconsider Ivw = I.v + I.w as FinSequence by NDIFF_5:9;
for j0 be Nat st j0 in dom Ivw holds Ivw.j0 = (xx12^yy12).j0
proof
let j0 be Nat;
assume j0 in dom Ivw;
then reconsider j=j0 as Element of dom carr (X^Y) by CARD_3:9;
A20: Ivw.j0 = ((addop (X^Y)).j).(Iv.j,Iw.j) by PRVECT_1:def 8
.= (the addF of (X^Y).j).(Iv.j,Iw.j) by PRVECT_1:def 12;
per cases by A20,A3,FINSEQ_1:25;
suppose
A21: j0 in dom CX;
then j0 in dom X by A1,FINSEQ_3:29;
then
A22: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A23: Iv.j = xx1.j & Iw.j = xx2.j by A21,A16,A17,FINSEQ_1:def 7;
A24: (xx12^yy12).j0 = xx12.j0 by A21,A16,FINSEQ_1:def 7;
reconsider j1=j0 as Element of dom carr X by A21;
(the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop X ).j1).(xx1.j1,xx2.j1)
by A22,A23,PRVECT_1:def 12
.= (xx12^yy12).j0 by A24,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A20;
end;
suppose ex n be Nat st n in dom CY & j0=len CX + n;
then consider n be Nat such that
A25: n in dom CY & j0 = len CX + n;
A26: len CX = len xx1 & len CX = len xx2 & len CX = len xx12
by A16,FINSEQ_3:29;
n in dom Y by A1,A25,FINSEQ_3:29;
then
A27: (X^Y).j = Y.n by A25,A1,FINSEQ_1:def 7;
A28: Iv.j = yy1.n & Iw.j = yy2.n by A16,A17,A25,A26,FINSEQ_1:def 7;
A29: (xx12^yy12).j0 = yy12.n by A25,A26,A16,FINSEQ_1:def 7;
reconsider j1=n as Element of dom carr Y by A25;
(the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop Y).j1).(yy1.j1,yy2.j1)
by A27,A28,PRVECT_1:def 12
.= (xx12^yy12).j0 by A29,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A20;
end;
end;
hence thesis by A18,A19,CARD_3:9,FINSEQ_1:13;
end;
then reconsider I as Homomorphism of [:product X,product Y:], product (X^Y)
by VECTSP_1:def 20;
take I;
thus thesis by A13,A2,A12;
end;
theorem
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 *>)
proof
let G,F be AbGroup;
consider I be Homomorphism of [:G,F:],product <*G,F*> such that
A1: I is bijective &
(for x be Element of G, y be Element of F holds I.(x,y) = <*x,y*>) by Th2;
thus
A2: 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 *>)
proof
let y be set;
hereby assume y is Element of product <*G,F*>;
then y in the carrier of product <*G,F*>;
then y in rng I by A1,FUNCT_2:def 3;
then consider x be Element of the carrier of [:G,F:] such that
A3: y = I.x by FUNCT_2:113;
consider x1 be Element of G, x2 be Element of F such that
A4: x=[x1,x2] by SUBSET_1:43;
take x1,x2;
I.(x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3,A4;
end;
now assume ex x1 be Element of G, x2 be Element of F st y = <*x1,x2*>;
then consider x1 be Element of G, x2 be Element of F such that
A5: y = <*x1,x2*>;
A6: I.[x1,x2] in rng I by FUNCT_2:112;
I.(x1,x2) = <*x1,x2*> by A1;
hence y is Element of product <*G,F*> by A5,A6;
end;
hence thesis;
end;
thus
A7: 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*>
proof
let x,y be Element of product <*G,F*>;
let x1,y1 be Element of G, x2,y2 be Element of F;
assume
A8: x = <*x1,x2*> & y = <*y1,y2*>;
reconsider z=[x1,x2], w=[y1,y2] as Element of [:G,F:];
A9: z+w = [x1+y1,x2+y2] by PRVECT_3:def 1;
I.(x1+y1,x2+y2) = <* x1+y1,x2+y2 *> & I.(x1,x2) = <* x1,x2 *> &
I.(y1,y2) = <* y1,y2 *> by A1;
hence <* x1+y1,x2+y2 *> =x+y by A9,A8,VECTSP_1:def 20;
end;
thus
A10: 0.product <*G,F*> = <* 0.G,0.F *>
proof
thus 0.product <*G,F*> = I.(0.[:G,F:]) by MOD_4:40
.= I.(0.G,0.F)
.= <* 0.G,0.F *> by A1;
end;
thus 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 *>
proof
let x be Element of product <*G,F*>;
let x1 be Element of G, x2 be Element of F;
assume
A11: x=<* x1,x2 *>;
reconsider y = <* -x1,-x2 *> as Element of product <*G,F*> by A2;
x+y = <* x1+-x1,x2+-x2 *> by A7,A11
.= <* 0.G,x2+-x2 *> by RLVECT_1:def 10
.= 0.(product <*G,F*>) by A10,RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
end;
theorem
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])
proof
let G,F be AbGroup;
thus 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]) by SUBSET_1:43;
thus 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] by PRVECT_3:def 1;
thus 0.[:G,F:] = [0.G,0.F];
thus 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]
proof
let x be Element of [:G,F:];
let x1 be Element of G, x2 be Element of F;
assume
A1: x=[x1,x2];
reconsider y= [-x1,-x2 ] as Element of [:G,F:];
x+y = [x1+-x1,x2+-x2] by A1,PRVECT_3:def 1
.= [0.G,x2+-x2] by RLVECT_1:def 10
.= 0.[:G,F:] by RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
end;
theorem Th6:
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
proof
let G,H,I be AddGroup;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
reconsider f = h1 * h as Function of G, I;
now
let a,b be Element of G;
thus f.(a + b) = h1.(h.(a + b)) by FUNCT_2:15
.= h1.(h.a + h.b) by VECTSP_1:def 20
.= (h1.(h.a)) + (h1.(h.b)) by VECTSP_1:def 20
.= f.a + (h1.(h.b)) by FUNCT_2:15
.= f.a + f.b by FUNCT_2:15;
end;
hence thesis by VECTSP_1:def 20;
end;
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; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th6;
end;
theorem Th7:
for G,H being AddGroup, h being Homomorphism of G,H st h is bijective holds
h" is Homomorphism of H,G
proof
let G,H be AddGroup, h be Homomorphism of G,H;
assume
A1: h is bijective;
then
A2: h is one-to-one & rng h = the carrier of H by FUNCT_2:def 3;
then reconsider h1 = h" as Function of H,G by FUNCT_2:25;
now
let a,b be Element of H;
set a1 = h1.a, b1 = h1.b;
h.a1 = a & h.b1 = b by A2,FUNCT_1:32;
hence h1.(a + b) = h1.(h.(a1 + b1)) by VECTSP_1:def 20
.= h1.a + h1.b by A1,FUNCT_2:26;
end;
hence thesis by VECTSP_1:def 20;
end;
theorem
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)
proof
let X,Y be Group-Sequence;
set PX = product X;
set PY = product Y;
set PXY = product(X^Y);
consider K be Homomorphism of [:PX,PY:],PXY such that
A1: K is bijective & (for x be Element of PX, y be Element of PY
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & K.(x,y) = x1^y1) by Th3;
consider J be Homomorphism of [:PX,PY:],product<*PX,PY*> such that
A2: J is bijective & (for x be Element of PX, y be Element of PY
holds J.(x,y) = <*x,y*>) by Th2;
reconsider JB = J" as Homomorphism of product <*PX,PY*>,[:PX,PY:] by A2,Th7;
dom J = the carrier of [:PX,PY:] by FUNCT_2:def 1;
then rng JB = the carrier of [:PX,PY:] by A2,FUNCT_1:33;
then
A3: JB is onto by FUNCT_2:def 3;
reconsider I= K*JB as Homomorphism of product <*PX,PY*>,PXY;
take I;
I is onto by A1,A3,FUNCT_2:27;
hence I is bijective by A1,A2;
thus for x be Element of PX, y be Element of PY holds ex x1,y1 be FinSequence
st x = x1 & y = y1 & I.<*x,y*> = x1^y1
proof
let x be Element of PX, y be Element of PY;
consider x1,y1 be FinSequence such that
A4: x=x1 & y=y1 & K.(x,y) = x1^y1 by A1;
A5: J.(x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:PX,PY:];
then
A6: [x,y] in dom J by FUNCT_2:def 1;
I.<*x,y*> = K.(JB.(J.[x,y])) by A5,FUNCT_2:15;
then I.<*x,y*> = x1^y1 by A4,A6,A2,FUNCT_1:34;
hence thesis by A4;
end;
end;
theorem Th9:
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*>])
proof
let X,Y be AbGroup;
consider J be Homomorphism of Y, product <*Y*> such that
A1: J is bijective & (for y be Element of Y holds J.y = <*y*>) by Th1;
defpred P[object,object,object] means $3 = [$1,<* $2 *>];
A2: for x,y be object st x in the carrier of X & y in the carrier of Y
ex z be object st z in the carrier of [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be object;
assume
A3: x in the carrier of X & y in the carrier of Y;
then reconsider y0=y as Element of Y;
reconsider z=[x,<*y0*>] as set by TARSKI:1;
take z;
J.y0 = <*y0*> by A1;
hence thesis by A3,ZFMISC_1:87;
end;
consider I be Function of [:the carrier of X,the carrier of Y:],
the carrier of [:X,product <*Y*>:] such that
A4: for x,y be object st x in the carrier of X & y in the carrier of Y holds
P[x,y,I.(x,y)] from BINOP_1:sch 1(A2);
reconsider I as Function of [:X,Y:],[:X,product <*Y*>:];
for v,w be Element of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Element of [:X,Y:];
consider x1 be Element of X, x2 be Element of Y such that
A5: v=[x1,x2] by SUBSET_1:43;
consider y1 be Element of X, y2 be Element of Y such that
A6: w=[y1,y2] by SUBSET_1:43;
A7: I.(v+w) = I.(x1+y1,x2+y2) by A5,A6,PRVECT_3:def 1
.= [x1+y1,<*x2+y2*>] by A4;
I.v = I.(x1,x2) & I.w = I.(y1,y2) by A5,A6;
then
A8: I.v = [x1,<*x2*>] & I.w = [y1,<*y2*>] by A4;
A9: J.x2 = <*x2*> & J.y2 = <*y2*> by A1;
then reconsider xx2=<*x2*> as Element of product <*Y*>;
reconsider yy2=<*y2*> as Element of product <*Y*> by A9;
<*x2+y2*> = J.(x2+y2) by A1
.= xx2+yy2 by A9,VECTSP_1:def 20;
hence I.v + I.w = I.(v+w) by A7,A8,PRVECT_3:def 1;
end;
then reconsider I as Homomorphism of [:X,Y:],[:X,product <*Y*>:]
by VECTSP_1:def 20;
take I;
now let z1,z2 be object;
assume
A10: z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I.z1 = I.z2;
consider x1,y1 be object such that
A11: x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1]
by A10,ZFMISC_1:def 2;
consider x2,y2 be object such that
A12: x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2]
by A10,ZFMISC_1:def 2;
[x1,<*y1*>] = I.(x1,y1) by A4,A11
.= I.(x2,y2) by A10,A11,A12
.= [x2,<*y2*>] by A4,A12;
then x1 = x2 & <*y1*> = <*y2*> by XTUPLE_0:1;
hence z1 = z2 by A11,A12,FINSEQ_1:76;
end;
then
A13: I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in the carrier of [:X,product <*Y*>:];
then consider x,y1 be object such that
A14: x in the carrier of X & y1 in the carrier of product <*Y*> &
w = [x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A14,FUNCT_2:def 3;
then consider y be object such that
A15: y in the carrier of Y & y1 = J.y by FUNCT_2:11;
reconsider z = [x,y] as Element of [:the carrier of X,the carrier of Y:]
by A14,A15,ZFMISC_1:87;
J.y = <*y*> by A15,A1;
then w = I.(x,y) by A4,A14,A15;
then w = I.z;
hence w in rng I by FUNCT_2:4;
end;
then the carrier of [:X,product <*Y*>:] c= rng I by TARSKI:def 3;
then I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence I is bijective by A13;
thus for x be Element of X, y be Element of Y holds I.(x,y) = [x,<*y*>]
by A4;
end;
theorem
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)
proof
let X be Group-Sequence;
let Y be AbGroup;
consider I be Homomorphism of [:product X,Y:],[:product X,product <*Y*>:]
such that
A1: I is bijective & (for x be Element of product X, y be Element of Y holds
I.(x,y) = [x,<*y*>]) by Th9;
consider J be Homomorphism of [:product X,product <*Y*>:], product (X^<*Y*>)
such that
A2: J 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 & J.(x,y) = x1^y1) by Th3;
set K = J*I;
reconsider K as Homomorphism of [:product X,Y:],product (X^<*Y*>);
take K;
A3: rng J = the carrier of product (X^<*Y*>) by A2,FUNCT_2:def 3;
rng I = the carrier of [:product X,product <*Y*>:] by A1,FUNCT_2:def 3;
then rng(J*I) = J.:(the carrier of [:product X,product <*Y*>:])
by RELAT_1:127
.= the carrier of product (X^<*Y*>) by A3,RELSET_1:22;
then K is onto by FUNCT_2:def 3;
hence K is bijective by A1,A2;
thus for x be Element of product X, y be Element of Y holds ex x1,y1 be
FinSequence st x = x1 & <*y*> = y1 & K.(x,y) = x1^y1
proof
let x be Element of product X, y be Element of Y;
A4: I.(x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [:product X,Y:];
then [x,<*y*>] in the carrier of [:product X,product <*Y*>:]
by A4,FUNCT_2:5;
then reconsider yy=<*y*> as Element of product <*Y*> by ZFMISC_1:87;
consider x1,y1 be FinSequence such that
A5: x = x1 & yy = y1 & J.(x,yy) = x1^y1 by A2;
J.(x,yy) = J.(I.([x,y])) by A4
.= K.(x,y) by FUNCT_2:15;
hence thesis by A5;
end;
end;
theorem Th11:
for n be non zero Nat holds
the addLoopStr of INT.Ring n is non empty Abelian right_complementable
add-associative right_zeroed
proof
let n be non zero Nat;
A1: 1 <= n by NAT_1:14;
now per cases;
suppose n=1;
hence INT.Ring n is Ring by INT_3:10;
end;
suppose n<>1;
then 1 < n by A1,XXREAL_0:1;
hence INT.Ring n is Ring by INT_3:11;
end;
end;
then reconsider R = INT.Ring n as Ring;
set S = the addLoopStr of INT.Ring n;
A2: for v,w being Element of S holds v + w = w + v
proof
let v,w be Element of S;
reconsider v1=v,w1=w as Element of R;
thus v+w = v1+w1
.= w1+v1
.= w+v;
end;
A3: for x being Element of S holds x is right_complementable
proof
let v be Element of S;
reconsider v1=v as Element of R;
consider w1 being Element of R such that
A4: v1 + w1 = 0.R by ALGSTR_0:def 11;
reconsider w=w1 as Element of S;
v+w = 0.S by A4;
hence thesis;
end;
A5: for u,v,w being Element of S holds (u + v) + w = u + (v + w)
proof
let u,v,w be Element of S;
reconsider u1=u,v1=v,w1=w as Element of R;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w);
end;
A6: for v being Element of S holds v + (0.S) = v
proof
let v be Element of S;
reconsider v1=v as Element of R;
thus v + (0.S) = v1 + 0.R
.= v;
end;
thus thesis by A2,A3,A5,A6,RLVECT_1:def 2,RLVECT_1:def 3,
RLVECT_1:def 4;
end;
definition
let n be natural Number;
func Z/Z n -> addLoopStr equals
the addLoopStr of INT.Ring n;
coherence;
end;
registration
let n be non zero natural Number;
cluster Z/Z n -> non empty strict;
coherence;
end;
registration
let n be non zero natural Number;
cluster Z/Z n -> Abelian right_complementable add-associative right_zeroed;
coherence by Th11;
end;
theorem Th12:
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))
proof
let X be Group-Sequence, x,y,z be Element of product X, x1,y1,z1 be
FinSequence;
assume
A1: x = x1 & y = y1 & z = z1;
hereby assume
A2: z = x+y;
thus for j be Element of dom carr X holds z1.j = (the addF of (X.j)).
((x1.j),(y1.j))
proof
let j be Element of dom carr X;
thus z1.j = ((addop X).j).((x1.j),(y1.j)) by A1,A2,PRVECT_1:def 8
.= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 12;
end;
end;
assume
A3: for j be Element of dom carr X holds z1.j = (the addF of (X.j)).
((x1.j),(y1.j));
reconsider Ixy = x+y as FinSequence by NDIFF_5:9;
A4: dom Ixy = dom carr X by CARD_3:9;
for j0 being Nat st j0 in dom z1 holds z1.j0 = Ixy.j0
proof
let j0 be Nat;
assume j0 in dom z1;
then reconsider j = j0 as Element of dom carr X by CARD_3:9,A1;
Ixy. j0 = ((addop X).j).((x1.j),(y1.j)) by A1,PRVECT_1:def 8
.= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 12
.= z1.j by A3;
hence thesis;
end;
hence z = x + y by A1,CARD_3:9,A4,FINSEQ_1:13;
end;
theorem Th13:
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
proof
let m be CR_Sequence, j be Nat, x be Integer;
assume
A1: j in dom m;
consider z being Integer such that
A2: z * m.j = Product(m) by A1,INT_6:10;
(x mod Product(m)) mod m.j = (x - (x div (z * m.j)) * (z * m.j)) mod m.j
by A2,INT_1:def 10
.= ((x mod m.j) - (0 + ((x div (z * m.j)) * z) * m.j mod m.j)) mod m.j
by INT_6:7
.= ((x mod m.j) - (0 mod m.j)) mod m.j by NAT_D:61
.= (x - 0) mod m.j by INT_6:7
.= x mod m.j;
hence thesis;
end;
Lm1: for m be non zero Nat, x be Integer holds
(x mod m) in Segm m
proof
let m be non zero Nat, x be Integer;
x mod m >= 0 & (x mod m) < m by NAT_D:62;
x mod m in NAT by INT_1:3;
thus thesis by NAT_1:44,NAT_D:62;
end;
theorem Th14:
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))
proof
let m be CR_Sequence, X be Group-Sequence;
assume
A1: 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));
set ZZ = Z/Z (Product(m));
reconsider CX = carr X as non-empty FinSequence;
len (carr X) = len X by PRVECT_1:def 11;
then
A2: dom (carr X) = Seg (len X) by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
defpred P[object,object] means
ex x be Integer st $1 = x & $2 = mod(x,m);
A3: for x be object st x in the carrier of Z/Z (Product(m))
ex y be object st y in
the carrier of (product X) & P[x,y]
proof
let x be object;
assume x in the carrier of Z/Z (Product(m));
then reconsider x1 = x as Integer;
A4: dom (mod(x1,m)) = Seg len (mod(x1,m)) by FINSEQ_1:def 3
.=Seg len m by INT_6:def 3
.=Seg len (carr X) by A1,PRVECT_1:def 11
.=dom (carr X) by FINSEQ_1:def 3;
now let i be object;
assume
A5: i in dom carr X;
then reconsider i0 = i as Element of dom carr X;
reconsider i1 = i as Nat by A5;
consider mi be non zero Nat such that
A6: mi=m.i0 & X.i0 = Z/Z (mi) by A1,A2;
(mod(x1,m)).i = x1 mod m.i1 by A4,A5,INT_6:def 3;
then (mod(x1,m)).i in the carrier of (X.i0) by A6,Lm1;
hence (mod(x1,m)).i in (carr X).i by A2,PRVECT_1:def 11;
end;
hence thesis by CARD_3:9,A4;
end;
consider I being Function of the carrier of Z/Z (Product(m)),the carrier of
(product X) such that
A7: for x be object st x in the carrier of Z/Z (Product(m)) holds P[x,I.x]
from FUNCT_2:sch 1 (A3);
A8: for x be Integer st x in the carrier of Z/Z (Product(m))
holds I.x = mod(x,m)
proof
let x be Integer;
assume x in the carrier of Z/Z (Product(m));
then ex x0 be Integer st x = x0 & I.x = mod(x0,m) by A7;
hence I.x = mod(x,m);
end;
for v,w being Point of ZZ holds I.(v + w) = (I.v) + (I.w)
proof
let v,w be Point of ZZ;
reconsider v1 = v, w1 = w, vw1 = v + w as Integer;
reconsider Iv = I.v, Iw = I.w, Ivw = I.(v + w) as FinSequence
by NDIFF_5:9;
A9: I.v1 = mod(v1,m) by A8;
A10: I.w1 = mod(w1,m) by A8;
A11: I.(vw1) = mod(vw1,m) by A8;
I.v in the carrier of (product X);
then mod(v1,m) in product (carr X) by A8;
then
A12: dom (mod(v1,m)) = dom (carr X) by CARD_3:9;
I.w in the carrier of (product X);
then mod(w1,m) in product (carr X) by A8;
then
A13: dom (mod(w1,m)) = dom (carr X) by CARD_3:9;
I.(v+w) in the carrier of (product X);
then mod(vw1,m) in product (carr X) by A8;
then
A14: dom (mod(vw1,m)) = dom (carr X) by CARD_3:9;
now let j be Element of dom (carr X);
reconsider j0=j as Nat;
consider mj be non zero Nat such that
A15: mj = m.j0 & X.j0 = Z/Z (mj) by A2,A1;
A16: dom m = Seg (len X) by A1,FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
A17: (v1 mod m.j0) in Segm mj & (w1 mod m.j0) in Segm mj by Lm1,A15;
A18: Iw.j0 = w1 mod m.j0 by A13,A10,INT_6:def 3;
A19: Ivw.j0 = vw1 mod m.j0 by A14,A11,INT_6:def 3;
thus Ivw.j
= ((v1+w1) mod Product(m)) mod m.j0 by GR_CY_1:def 4,A19
.= ((v1+w1)) mod m.j0 by A2,A16,Th13
.= ((v1 mod m.j0) +(w1 mod m.j0)) mod m.j0 by NAT_D:66
.= (addint(mj)).((v1 mod m.j0),(w1 mod m.j0)) by A17,A15,GR_CY_1:def 4
.= (the addF of (X.j)).((Iv.j),(Iw.j)) by A12,A9,INT_6:def 3,A18,A15;
end;
hence I.(v + w) = (I.v) + (I.w) by Th12;
end;
then reconsider I as Homomorphism of Z/Z (Product(m)),product X
by VECTSP_1:def 20;
take I;
thus thesis by A8;
end;
theorem Th15:
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*>])
proof
let X,Y be non empty set;
A1: product <*Y*> <> {}
proof
assume product <*Y*> = {};
then {} in rng <*Y*> by CARD_3:26;
then {} in { Y } by FINSEQ_1:39;
hence contradiction by TARSKI:def 1;
end;
consider J be Function of Y,product <*Y*> such that
A2: J is one-to-one & J is onto &
(for y be object st y in Y holds J.y = <*y*>)
by PRVECT_3:4;
defpred P[object,object,object] means $3 = [$1,<* $2 *>];
A3: for x,y be object st x in X & y in Y
ex z be object st z in [:X,product <*Y*>:]
& P[x,y,z]
proof
let x,y be object;
assume
A4: x in X & y in Y;
reconsider z = [x,<*y*>] as set by TARSKI:1;
take z;
J.y = <* y *> by A2,A4;
then <* y *> in product <*Y*> by A4,A1,FUNCT_2:5;
hence thesis by A4,ZFMISC_1:87;
end;
consider I be Function of [:X,Y:],[:X,product <*Y*>:] such that
A5: for x,y be object st x in X & y in Y holds P[x,y,I.(x,y)]
from BINOP_1:sch 1(A3);
reconsider I as Function of [:X,Y:],[:X,product <*Y*>:];
take I;
thus I is one-to-one
proof
now let z1,z2 be object;
assume
A6: z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1 = I.z2;
then consider x1,y1 be object such that
A7: x1 in X & y1 in Y & z1 = [x1,y1] by ZFMISC_1:def 2;
consider x2,y2 be object such that
A8: x2 in X & y2 in Y & z2 = [x2,y2] by A6,ZFMISC_1:def 2;
A9: [x1,<*y1*>] = I.(x1,y1) by A5,A7
.= I.(x2,y2) by A6,A7,A8
.= [x2,<*y2*>] by A5,A8;
then <*y1*> = <*y2*> by XTUPLE_0:1;
then y1 = y2 by FINSEQ_1:76;
hence z1 = z2 by A7,A8,A9,XTUPLE_0:1;
end;
hence thesis by FUNCT_2:19,A1;
end;
thus I is onto
proof
now let w be object;
assume w in [:X, product <*Y*>:];
then consider x,y1 be object such that
A10: x in X & y1 in product <*Y*> & w = [x,y1] by ZFMISC_1:def 2;
y1 in rng J by A2,A10,FUNCT_2:def 3;
then consider y be object such that
A11: y in Y & y1 = J.y by FUNCT_2:11;
A12: J.y = <*y*> by A11,A2;
reconsider z = [x,y] as Element of [:X,Y:] by A10,A11,ZFMISC_1:87;
w = I.(x,y) by A5,A10,A11,A12
.= I.z;
hence w in rng I by FUNCT_2:4,A1;
end;
then [:X,product <*Y*>:] c= rng I by TARSKI:def 3;
hence thesis by FUNCT_2:def 3,XBOOLE_0:def 10;
end;
thus for x,y be set st x in X & y in Y holds I.(x,y) = [x,<*y*>] by A5;
end;
theorem Th16:
for X be non empty set holds card(product <*X*>) = card X
proof
let X be non empty set;
consider I be Function of X,product <*X*> such that
A1: I is one-to-one & I is onto &
for x be object st x in X holds I.x = <*x*>
by PRVECT_3:4;
not {} in rng <*X*>
proof
assume not not {} in rng <*X*>;
then {} in { X } by FINSEQ_1:39;
hence contradiction by TARSKI:def 1;
end;
then product (<*X*>) <> {} by CARD_3:26;
then
A2: dom I = X by FUNCT_2:def 1;
rng I = product (<*X*>) by A1,FUNCT_2:def 3;
hence card(X) = card(product(<*X*>)) by CARD_1:5,A1,A2,WELLORD2:def 4;
end;
theorem Th17:
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)
proof
let X be non-empty non empty FinSequence, Y be non empty set;
A1: product <*Y*> <> {}
proof
assume product <*Y*> = {};
then {} in rng <*Y*> by CARD_3:26;
then {} in { Y } by FINSEQ_1:39;
hence contradiction by TARSKI:def 1;
end;
consider I be Function of [:product X,Y:],[:product X,product <*Y*>:]
such that
A2: I is one-to-one & I is onto & (for x,y be set st x in product X & y in Y
holds I.(x,y) = [x,<*y*>]) by Th15;
<*Y*> is non-empty
proof
assume not (<*Y*> is non-empty);
then {} in rng <*Y*> by RELAT_1:def 9;
then {} in {Y} by FINSEQ_1:39;
hence contradiction by TARSKI:def 1;
end;
then reconsider YY=<*Y*> as non-empty non empty FinSequence;
consider J be Function of [:product X,product YY:],product(X^YY)
such that
A3: J is one-to-one & J is onto & (for x,y be FinSequence st x in product X &
y in product YY holds J.(x,y) = x^y) by PRVECT_3:6;
set K = J*I;
reconsider K as Function of [:product X,Y:],product (X^<*Y*>);
take K;
thus K is one-to-one by A2,A3;
A4: rng J = product (X^<*Y*>) by A3,FUNCT_2:def 3;
rng I = [:product X,product<*Y*>:] by A2,FUNCT_2:def 3;
then rng(J * I) = J.:([:product X,product <*Y*>:]) by RELAT_1:127
.= product (X^<*Y*>) by A4,RELSET_1:22;
hence K is onto by FUNCT_2:def 3;
thus for x,y be set st x in product X & y in Y ex x1,y1 be FinSequence st
x = x1 & <*y*> =y1 & K.(x,y) = x1^y1
proof
let x,y be set;
assume
A5: x in product X & y in Y;
then
A6: I.(x,y) = [x,<*y*>] by A2;
A7: [x,y] in [: product X,Y:] by A5,ZFMISC_1:87;
then [x,<*y*>] in [:product X,product <*Y*>:] by A6,A1,FUNCT_2:5;
then
A8: <*y*> in product <*Y*> by ZFMISC_1:87;
reconsider xx=x as Function by A5;
dom xx = dom X by CARD_3:9,A5
.=Seg (len X) by FINSEQ_1:def 3;
then reconsider x1=xx as FinSequence by FINSEQ_1:def 2;
set y1 = <*y*>;
A9: J.(x,<*y*>) = x1^y1 by A3,A5,A8;
J.(x,<*y*>) = K.(x,y) by A6,A7,FUNCT_2:15;
hence thesis by A9;
end;
end;
theorem Th18:
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)
proof
defpred P[Nat] means for m being FinSequence of NAT, X be non-empty non empty
FinSequence st len m = $1 & 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);
A1: P[0];
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
now let m be FinSequence of NAT, X be non-empty non empty FinSequence;
assume
A4: len m = n + 1 & len m = len X & (for i be Element of NAT st i in dom X
holds card(X.i) = m.i);
now per cases;
suppose
A5: n = 0;
A6: m = <*m.1*> by A5,FINSEQ_1:40,A4;
A7: X = <*X.1*> by A5,FINSEQ_1:40,A4;
n+1 in Seg (n+1) by FINSEQ_1:4;
then
A8: 1 in dom X by A5,FINSEQ_1:def 3,A4;
thus card(product X) = card (X.1) by Th16,A7,A8
.= m.1 by A8,A4
.= Product(m) by A6,RVSUM_1:95;
end;
suppose
A9: n <> 0;
set X1 = X | n;
reconsider m1 = m | n as FinSequence of NAT;
A10: len m1 = n by NAT_1:11,A4,FINSEQ_1:59;
A11: len X1 = n by NAT_1:11,A4,FINSEQ_1:59;
A12: dom X1 = Seg (len X1) by FINSEQ_1:def 3
.= Seg n by NAT_1:11,A4,FINSEQ_1:59;
A13: dom m1 = Seg (len m1) by FINSEQ_1:def 3
.= Seg n by NAT_1:11,A4,FINSEQ_1:59;
reconsider X1 as non-empty non empty FinSequence by A9;
now let i be Element of NAT;
assume
A15: i in dom X1;
Seg n c= Seg (n+1) by NAT_1:11,FINSEQ_1:5;
then i in Seg (len X) by A4,A12,A15;
then
A16: i in dom X by FINSEQ_1:def 3;
thus card(X1.i) = card(X.i) by FUNCT_1:47,A15
.= m.i by A4,A16
.= m1.i by FUNCT_1:47,A15,A13,A12;
end;
then
A17: card(product X1) = Product m1 by A3,A10,A11;
A18: n < len X by NAT_1:19,A4;
A20: X = X| (n + 1) by FINSEQ_1:58,A4
.= X1^(<*X.(len X) *>) by A18,FINSEQ_5:83,A4;
A21: n < len m by NAT_1:19,A4;
A22: m = m| (n+1) by FINSEQ_1:58,A4
.= m1^(<*m.(len m) *>) by A21,FINSEQ_5:83,A4;
len X in Seg (len X) by A4,FINSEQ_1:4;
then
A23: len X in dom X by FINSEQ_1:def 3;
then
A24: card(X.(len X)) = m.(len m) by A4;
consider I be Function of [:product X1,(X.(len X)):],
product(X1^<*(X.(len X))*>) such that
A25: I is one-to-one & I is onto & (for x,y be set st x in product X1 &
y in (X.(len X))
ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1)
by A23,Th17;
not {} in rng (X1^<*(X.(len X))*>)
proof
assume not not {} in rng (X1^<*(X.(len X))*>);
then {} in ( rng X1 \/ rng <*(X.(len X))*>) by FINSEQ_1:31;
then {} in rng X1 or {} in rng <*(X.(len X))*> by XBOOLE_0:def 3;
then not X1 is non-empty or {} in { X.(len X) }
by FINSEQ_1:39;
hence contradiction by TARSKI:def 1,A23;
end;
then product(X1^<*(X.(len X))*>) <> {} by CARD_3:26;
then
A26: dom I = [:product X1,(X.(len X)):] by FUNCT_2:def 1;
rng I = product(X1^<*(X.(len X))*>) by A25,FUNCT_2:def 3;
then
A27: card([:product X1,(X.(len X)):]) = card(product(X1^<*(X.(len X))*>))
by CARD_1:5,A25,A26,WELLORD2:def 4;
A28: card(product X) = card(product <*(product X1),(X.(len X))*>)
by CARD_1:5,A20,A27,TOPGEN_5:8;
A29: product X1 is finite set & X.(len X) is finite set by A24,A17;
card(product <*(product X1),(X.(len X))*>) =
card([:product X1,(X.(len X)):]) by CARD_1:5,TOPGEN_5:8
.= (Product m1) * (m.(len m)) by A24,A17,A29,CARD_2:46;
hence card (product X) = Product(m) by RVSUM_1:96,A22,A28;
end;
end;
hence card (product X) = Product(m);
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th19:
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)
proof
let m be CR_Sequence, X be Group-Sequence;
assume
A1: 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));
A2: dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3
.=Seg (len X) by PRVECT_1:def 11
.= dom X by FINSEQ_1:def 3;
A3: dom X = Seg (len X) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3,A1;
A4: for i be Element of NAT st i in dom (carr X) holds card((carr X).i) = m.i
proof
let i be Element of NAT;
assume
A5: i in dom (carr X);
reconsider i0=i as Element of dom X by A2,A5;
consider mi be non zero Nat such that
A6: mi = m.i & X.i = Z/Z (mi) by A2,A5,A1;
thus card((carr X).i) = card(the carrier of (X.i0)) by PRVECT_1:def 11
.=m.i by A6;
end;
A7: len carr X = len m by A1,PRVECT_1:def 11;
now let i be Nat;
assume i in dom m;
then ex mi be non zero Nat st mi = m.i & X.i = Z/Z (mi)
by A3,A1;
hence m.i in NAT by ORDINAL1:def 12;
end;
then m is FinSequence of NAT by FINSEQ_2:12;
hence thesis by A4,A7,Th18;
end;
theorem Th20:
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
proof
let m be CR_Sequence, X be Group-Sequence, I be Function of
Z/Z (Product(m)),product X;
assume
A1: 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));
for x1,x2 be object
st x1 in the carrier of Z/Z (Product(m)) & x2 in the carrier
of Z/Z (Product(m)) & I.x1 = I.x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A2: x1 in the carrier of Z/Z (Product(m)) & x2 in the carrier of
Z/Z (Product(m)) & I.x1 = I.x2;
then reconsider xx1 = x1,xx2 = x2 as Integer;
A3: 0<=xx1 & xx1 < Product(m) by A2,NAT_1:44;
A4: 0<=xx2 & xx2 < Product(m) by A2,NAT_1:44;
A5: I.x2 = mod(xx2,m) by A1,A2;
reconsider I0 = 0 as Integer;
reconsider u = {} as INT-valued FinSequence;
A6: dom (mod(xx1,m)) = Seg len (mod(xx1,m)) by FINSEQ_1:def 3
.=Seg len m by INT_6:def 3
.=dom m by FINSEQ_1:def 3;
A7: now let i be Nat;
assume
A8: i in dom m;
A9: i in dom (mod(xx2,m)) by A5,A6,A1,A2,A8;
m.i in rng m by FUNCT_1:3,A8;
then
A10: m.i > 0 by PARTFUN3:def 1;
A11: xx1 mod (m.i) = (mod(xx1,m)).i by A6,A8,INT_6:def 3
.= (mod(xx2,m)).i by A1,A2,A5
.= xx2 mod (m .i) by A9,INT_6:def 3;
then
A12: (m.i) divides ((xx1 - xx2) - I0) by INT_1:def 4,NAT_D:64,A10;
A13: (m . i) divides ((xx2 - xx1) - I0) by INT_1:def 4,NAT_D:64,A10,A11;
u.i = I0;
hence (xx1 - xx2),u.i are_congruent_mod (m.i) & (xx2 - xx1),u.i
are_congruent_mod (m.i) by A12,A13,INT_1:def 4;
end;
A14: for i being Nat st i in dom m holds I0,u.i
are_congruent_mod (m.i)
proof
let i be Nat;
assume i in dom m;
A15: u.i = I0;
I0 - I0 = (I0 - I0) * (m.i);
hence I0,u.i are_congruent_mod (m.i) by A15,INT_1:def 4,INT_1:def 3;
end;
A16: xx1 mod Product(m) >=0 & xx1 mod Product(m) < Product(m) by NAT_D:62;
A17: xx2 mod Product(m) >=0 & xx2 mod Product(m) < Product(m) by NAT_D:62;
A18: xx1 mod Product(m) = xx1 by A3,NAT_D:63;
A19: xx2 mod Product(m) = xx2 by A4,NAT_D:63;
per cases;
suppose xx2 <= xx1;
then
A20: xx1-xx2 in NAT by INT_1:5;
xx1-xx2 <= xx1 mod Product(m) by A18,XREAL_1:43,A2;
then xx1-xx2 - Product(m) < xx1 mod Product(m) - (xx1 mod Product(m))
by A16,XREAL_1:15;
then
A21: xx1-xx2 < xx1-xx2 - (xx1-xx2 - Product(m)) by XREAL_1:46;
for i being Nat st i in dom m holds (xx1 - xx2),u.i
are_congruent_mod (m.i) by A7;
then xx1 - xx2 = I0 by INT_6:42,A14,A20,A21;
hence x1 = x2;
end;
suppose not xx2 <= xx1;
then
A22: xx2-xx1 in NAT by INT_1:5;
xx2-xx1 <= xx2 mod Product(m) by A19,XREAL_1:43,A2;
then xx2-xx1 - Product(m) < xx2 mod Product(m) - (xx2 mod Product(m))
by A17,XREAL_1:15;
then
A23: xx2-xx1 < xx2-xx1 - (xx2-xx1 - Product(m)) by XREAL_1:46;
for i being Nat st i in dom m holds (xx2 - xx1),u.i
are_congruent_mod (m.i) by A7;
then xx2 - xx1 =I0 by INT_6:42,A14,A22,A23;
hence x1 = x2;
end;
end;
hence I is one-to-one by FUNCT_2:19;
end;
theorem
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))
proof
let m be CR_Sequence, X be Group-Sequence;
assume
A1: 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));
then consider I be Homomorphism of Z/Z (Product(m)),product X such that
A2: (for x be Integer st x in the carrier of Z/Z (Product(m)) holds I.x =
mod(x,m)) by Th14;
A3: I is one-to-one by A1,Th20,A2;
Product(m) is Nat by TARSKI:1; then
A4: card(Segm Product(m)) = Product(m);
A5: card(the carrier of product X) = Product(m) by A1,Th19;
then the carrier of product X is finite;
then I is onto by A3,A4,A5,FINSEQ_4:63;
hence thesis by A2,A3;
end;