:: Isomorphisms of Direct Products of Finite Cyclic Groups
:: by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 27, 2012
:: Copyright (c) 2012 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, ORDINAL1, PRVECT_1, INT_3, XCMPLX_0, INT_1, INT_6,
ZFMISC_1, VECTSP_1, FUNCSDOM, GROUP_6, GROUP_14;
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, FUNCSDOM, 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,
XTUPLE_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions FINSEQ_1, BINOP_1, ALGSTR_0, STRUCT_0, PRVECT_1, PRVECT_3, INT_3,
CARD_1;
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,
STIRL2_1, 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 set 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,FINSEQ_1:40;
end;
hence thesis by PRVECT_1:def 9;
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 set 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,FINSEQ_1:44;
end;
hence thesis by PRVECT_1:def 9;
end;
end;
theorem Th11:
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 set st x in CarrX holds
I.x = <*x*>) by PRVECT_3:4;
len carr <*X*> = len <*X*> by PRVECT_1:def 10;
then
A2: len carr <*X*> = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by FINSEQ_1:2,def 8;
A4: <*X*>.1 = X by FINSEQ_1:def 8;
1 in {1} by TARSKI:def 1;
then (carr <*X*>).1 = the carrier of X by A3,A4,PRVECT_1:def 10;
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;
A8: I.v = <*v*> & I.w = <*w*> & I.(v+w) = <*v+w*> by A1;
A9: <*v*>.1 = v & <*w*>.1 = w by FINSEQ_1:40;
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;
A10: (addop <*X*>).j1 = the addF of (<*X*>.j1) by PRVECT_1:def 11;
A11: ([:addop <*X*>:].(Iv,Iw)).j1 = ((addop <*X*>).j1).(Iv.j1,Iw.j1)
by PRVECT_1:def 8
.= v+w by A10,A8,A9,FINSEQ_1:40;
consider Ivw be Function such that
A12: I.v + I.w = Ivw & dom Ivw = dom carr <*X*> & (for i be set st
i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i) by CARD_3:def 5;
A13: dom Ivw = Seg 1 by A2,A12,FINSEQ_1:def 3;
then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A13,FINSEQ_1:def 3;
hence thesis by A8,A12,A11,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 set 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 9;
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 9;
end;
end;
end;
theorem Th12:
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 set 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 10;
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 by FINSEQ_1:44;
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 10;
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
A9: v = [x1,y1] by SUBSET_1:43;
consider x2 be Element of X, y2 be Element of Y such that
A10: w = [x2,y2] by SUBSET_1:43;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A9,A10;
then
A11: I.v = <*x1,y1*> & I.w = <*x2,y2*> by A1;
A12: I.(v+w) =I.(x1+x2,y1+y2) by A9,A10,PRVECT_3:def 1
.= <* x1+x2,y1+y2 *> by A1;
A13: <*x1,y1*>.1 = x1 & <*x2,y2*>.1 = x2 & <*x1,y1*>.2 = y1 & <*x2,y2*>.2 = y2
by FINSEQ_1:44;
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;
A14: (addop <*X,Y*>).j1 = the addF of (<*X,Y*>.j1) by PRVECT_1:def 11;
A15: ([:addop <*X,Y*>:].(Iv,Iw)).j1 = ((addop <*X,Y*>).j1).(Iv.j1,Iw.j1)
by PRVECT_1:def 8
.= x1+x2 by A14,A11,A13,FINSEQ_1:44;
A16: (addop <*X,Y*>).j2 = the addF of (<*X,Y*>.j2) by PRVECT_1:def 11;
A17: ([:addop <*X,Y*>:].(Iv,Iw)).j2 = ((addop <*X,Y*>).j2).(Iv.j2,Iw.j2)
by PRVECT_1:def 8
.= y1+y2 by A16,A11,A13,FINSEQ_1:44;
consider Ivw be Function such that
A18: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y*> & (for i be set st
i in dom carr <*X,Y*> holds Ivw.i in carr (<*X,Y*>).i) by CARD_3:def 5;
A19: dom Ivw = Seg 2 by A2,A18,FINSEQ_1:def 3;
then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A19,FINSEQ_1:def 3;
hence thesis by A12,A18,A15,A17,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 Th13:
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 10;
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 10;
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 10
.= (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 10
.= (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
A15: v = [x1,y1] by SUBSET_1:43;
consider x2 be Element of PX, y2 be Element of PY such that
A16: 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;
A17: 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 A15,A16;
then
A18: I.v = xx1^yy1 & I.w = xx2^yy2 by A2;
I.(v+w) = I.(x1+x2,y1+y2) by A15,A16,PRVECT_3:def 1;
then
A19: I.(v+w) = xx12^yy12 by A2;
then
A20: 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;
A22: 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 11;
per cases by A22,A3,FINSEQ_1:25;
suppose
A23: j0 in dom CX;
then j0 in dom X by A1,FINSEQ_3:29;
then
A24: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A25: Iv.j = xx1.j & Iw.j = xx2.j by A23,A17,A18,FINSEQ_1:def 7;
A26: (xx12^yy12).j0 = xx12.j0 by A23,A17,FINSEQ_1:def 7;
reconsider j1=j0 as Element of dom carr X by A23;
(the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop X ).j1).(xx1.j1,xx2.j1)
by A24,A25,PRVECT_1:def 11
.= (xx12^yy12).j0 by A26,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
suppose ex n be Nat st n in dom CY & j0=len CX + n;
then consider n be Nat such that
A27: n in dom CY & j0 = len CX + n;
A28: len CX = len xx1 & len CX = len xx2 & len CX = len xx12
by A17,FINSEQ_3:29;
n in dom Y by A1,A27,FINSEQ_3:29;
then
A29: (X^Y).j = Y.n by A27,A1,FINSEQ_1:def 7;
A30: Iv.j = yy1.n & Iw.j = yy2.n by A17,A18,A27,A28,FINSEQ_1:def 7;
A31: (xx12^yy12).j0 = yy12.n by A27,A28,A17,FINSEQ_1:def 7;
reconsider j1=n as Element of dom carr Y by A27;
(the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop Y).j1).(yy1.j1,yy2.j1)
by A29,A30,PRVECT_1:def 11
.= (xx12^yy12).j0 by A31,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
end;
hence thesis by A19,A20,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 Th19:
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 Th12;
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 Th48:
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;
coherence by Th48;
end;
theorem Th72:
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 Th13;
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 Th12;
reconsider JB = J" as Homomorphism of product <*PX,PY*>,[:PX,PY:] by A2,Th72;
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
A4: 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,A4,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
A7: x=x1 & y=y1 & K.(x,y) = x1^y1 by A1;
A8: J.(x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:PX,PY:];
then
A9: [x,y] in dom J by FUNCT_2:def 1;
<*x,y*> is Element of product <*PX,PY*> by Th19;
then I.<*x,y*> = K.(JB.(J.[x,y])) by A8,FUNCT_2:15;
then I.<*x,y*> = x1^y1 by A7,A9,A2,FUNCT_1:34;
hence thesis by A7;
end;
end;
theorem Th21:
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 Th11;
defpred P[set,set,set] means $3 = [$1,<* $2 *>];
A2: for x,y be set st x in the carrier of X & y in the carrier of Y ex z be set
st z in the carrier of [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be set;
assume
A3: x in the carrier of X & y in the carrier of Y;
then reconsider y0=y as Element of Y;
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 set 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
A10: v=[x1,x2] by SUBSET_1:43;
consider y1 be Element of X, y2 be Element of Y such that
A11: w=[y1,y2] by SUBSET_1:43;
A12: I.(v+w) = I.(x1+y1,x2+y2) by A10,A11,PRVECT_3:def 1
.= [x1+y1,<*x2+y2*>] by A4;
I.v = I.(x1,x2) & I.w = I.(y1,y2) by A10,A11;
then
A13: I.v = [x1,<*x2*>] & I.w = [y1,<*y2*>] by A4;
A14: 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 A14;
<*x2+y2*> = J.(x2+y2) by A1
.= xx2+yy2 by A14,VECTSP_1:def 20;
hence I.v + I.w = I.(v+w) by A12,A13,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 set;
assume
A5: z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I.z1 = I.z2;
consider x1,y1 be set such that
A6: x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1]
by A5,ZFMISC_1:def 2;
consider x2,y2 be set such that
A7: x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2]
by A5,ZFMISC_1:def 2;
[x1,<*y1*>] = I.(x1,y1) by A4,A6
.= I.(x2,y2) by A5,A6,A7
.= [x2,<*y2*>] by A4,A7;
then x1 = x2 & <*y1*> = <*y2*> by XTUPLE_0:1;
hence z1 = z2 by A6,A7,FINSEQ_1:76;
end;
then
B1: I is one-to-one by FUNCT_2:19;
now let w be element;
assume w in the carrier of [:X,product <*Y*>:];
then consider x,y1 be set such that
A8: 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,A8,FUNCT_2:def 3;
then consider y be set such that
A9: 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 A8,A9,ZFMISC_1:87;
J.y = <*y*> by A9,A1;
then w = I.(x,y) by A4,A8,A9;
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 B1;
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 Th21;
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 Th13;
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 ThX01:
for n be non zero natural number holds
the addLoopStr of INT.Ring n is non empty Abelian right_complementable
add-associative right_zeroed
proof
let n be non zero natural number;
P0: 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 P0,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;
P1: 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;
P2: 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
P3: v1 + w1 = 0.R by ALGSTR_0:def 11;
reconsider w=w1 as Element of S;
v+w = 0.S by P3;
hence thesis by ALGSTR_0:def 11;
end;
P4: 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;
P5: 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 P1,P2,P4,P5,RLVECT_1:def 2,ALGSTR_0:def 16,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 ThX01;
end;
theorem Lm5:
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
AS1: x = x1 & y = y1 & z = z1;
hereby assume
AS2: 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 AS1,AS2,PRVECT_1:def 8
.= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 11;
end;
end;
assume
AS3: 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;
A2: 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,AS1;
Ixy. j0 = ((addop X).j).((x1.j),(y1.j)) by AS1,PRVECT_1:def 8
.= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 11
.= z1.j by AS3;
hence thesis;
end;
hence z = x + y by AS1,CARD_3:9,A2,FINSEQ_1:13;
end;
theorem LMThX021A:
for m being CR_Sequence, j being natural number, 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 natural number, x be Integer;
assume
AS1: j in dom m;
consider z being Integer such that
A1: z * m.j = Product(m) by AS1,INT_6:10;
(x mod Product(m)) mod m.j = (x - (x div (z * m.j)) * (z * m.j)) mod m.j
by A1,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;
LMThX021B: for m be non zero natural number, x be Integer holds
(x mod m) in Segm m
proof
let m be non zero natural number, x be Integer;
x mod m >= 0 & (x mod m) < m by NAT_D:62;
then x mod m in NAT by INT_1:3;
hence thesis by NAT_1:44,NAT_D:62;
end;
theorem LMThX021:
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 natural number
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
AS1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
non zero natural number 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 10;
then
A1: dom (carr X) = Seg (len X) by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
defpred P[set,set] means ex x be Integer st $1 = x & $2 = mod(x,m);
F0: for x be set st x in the carrier of Z/Z (Product(m)) ex y be set st y in
the carrier of (product X) & P[x,y]
proof
let x be set;
assume x in the carrier of Z/Z (Product(m));
then reconsider x1 = x as Integer;
F1: 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 AS1,PRVECT_1:def 10
.=dom (carr X) by FINSEQ_1:def 3;
now let i be set;
assume
F2: i in dom carr X;
then reconsider i0 = i as Element of dom carr X;
reconsider i1 = i as natural number by F2;
consider mi be non zero natural number such that
F3: mi=m.i0 & X.i0 = Z/Z (mi) by AS1,A1;
(mod(x1,m)).i = x1 mod m.i1 by F1,F2,INT_6:def 3;
then (mod(x1,m)).i in the carrier of (X.i0) by F3,LMThX021B;
hence (mod(x1,m)).i in (carr X).i by A1,PRVECT_1:def 10;
end;
hence thesis by CARD_3:9,F1;
end;
consider I being Function of the carrier of Z/Z (Product(m)),the carrier of
(product X) such that
A2: for x be set st x in the carrier of Z/Z (Product(m)) holds P[x,I.x]
from FUNCT_2:sch 1 (F0);
A3: 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 A2;
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;
B1: I.v1 = mod(v1,m) by A3;
B2: I.w1 = mod(w1,m) by A3;
B3: I.(vw1) = mod(vw1,m) by A3;
I.v in the carrier of (product X);
then mod(v1,m) in product (carr X) by A3;
then
B4: 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 A3;
then
B5: 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 A3;
then
B6: dom (mod(vw1,m)) = dom (carr X) by CARD_3:9;
now let j be Element of dom (carr X);
reconsider j0=j as natural number;
consider mj be non zero natural number such that
B7: mj = m.j0 & X.j0 = Z/Z (mj) by A1,AS1;
B8: dom m = Seg (len X) by AS1,FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
B9: (v1 mod m.j0) in Segm mj & (w1 mod m.j0) in Segm mj by LMThX021B,B7;
B10: Iw.j0 = w1 mod m.j0 by B5,B2,INT_6:def 3;
B11: Ivw.j0 = vw1 mod m.j0 by B6,B3,INT_6:def 3;
thus Ivw.j
= ((v1+w1) mod Product(m)) mod m.j0 by GR_CY_1:def 4,B11
.= ((v1+w1)) mod m.j0 by A1,B8,LMThX021A
.= ((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 B9,B7,GR_CY_1:def 4
.= (the addF of (X.j)).((Iv.j),(Iw.j)) by B4,B1,INT_6:def 3,B10,B7;
end;
hence I.(v + w) = (I.v) + (I.w) by Lm5;
end;
then reconsider I as Homomorphism of Z/Z (Product(m)),product X
by VECTSP_1:def 20;
take I;
thus thesis by A3;
end;
theorem Th23C:
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;
A0: 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
A1: J is one-to-one & J is onto & (for y be set st y in Y holds J.y = <*y*>)
by PRVECT_3:4;
defpred P[set,set,set] means $3 = [$1,<* $2 *>];
A2: for x,y be set st x in X & y in Y ex z be set st z in [:X,product <*Y*>:]
& P[x,y,z]
proof
let x,y be set;
assume
A3: x in X & y in Y;
then J.y = <* y *> by A1;
then <* y *> in product <*Y*> by A3,A0,FUNCT_2:5;
hence thesis by A3,ZFMISC_1:87;
end;
consider I be Function of [:X,Y:],[:X,product <*Y*>:] such that
A4: for x,y be set st x in X & y in Y holds P[x,y,I.(x,y)]
from BINOP_1:sch 1(A2);
reconsider I as Function of [:X,Y:],[:X,product <*Y*>:];
take I;
thus I is one-to-one
proof
now let z1,z2 be set;
assume
A5: z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1 = I.z2;
then consider x1,y1 be set such that
A6: x1 in X & y1 in Y & z1 = [x1,y1] by ZFMISC_1:def 2;
consider x2,y2 be set such that
A7: x2 in X & y2 in Y & z2 = [x2,y2] by A5,ZFMISC_1:def 2;
A8: [x1,<*y1*>] = I.(x1,y1) by A4,A6
.= I.(x2,y2) by A5,A6,A7
.= [x2,<*y2*>] by A4,A7;
then <*y1*> = <*y2*> by XTUPLE_0:1;
then y1 = y2 by FINSEQ_1:76;
hence z1 = z2 by A6,A7,A8,XTUPLE_0:1;
end;
hence thesis by FUNCT_2:19,A0;
end;
thus I is onto
proof
now let w be element;
assume w in [:X, product <*Y*>:];
then consider x,y1 be set such that
A9: x in X & y1 in product <*Y*> & w = [x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A9,FUNCT_2:def 3;
then consider y be set such that
A10: y in Y & y1 = J.y by FUNCT_2:11;
A11: J.y = <*y*> by A10,A1;
reconsider z = [x,y] as Element of [:X,Y:] by A9,A10,ZFMISC_1:87;
w = I.(x,y) by A4,A9,A10,A11
.= I.z;
hence w in rng I by FUNCT_2:4,A0;
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 A4;
end;
theorem Lm300F:
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 set 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 Lm300C:
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;
A0: 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
A1: 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 Th23C;
<*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
A2: 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 A1,A2;
A3: rng J = product (X^<*Y*>) by A2,FUNCT_2:def 3;
rng I = [:product X,product<*Y*>:] by A1,FUNCT_2:def 3;
then rng(J * I) = J.:([:product X,product <*Y*>:]) by RELAT_1:127
.= product (X^<*Y*>) by A3,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
A4: x in product X & y in Y;
then
A5: I.(x,y) = [x,<*y*>] by A1;
A6: [x,y] in [: product X,Y:] by A4,ZFMISC_1:87;
then [x,<*y*>] in [:product X,product <*Y*>:] by A5,A0,FUNCT_2:5;
then
A7: <*y*> in product <*Y*> by ZFMISC_1:87;
reconsider xx=x as Function by A4;
dom xx = dom X by CARD_3:9,A4
.=Seg (len X) by FINSEQ_1:def 3;
then reconsider x1=xx as FinSequence by FINSEQ_1:def 2;
set y1 = <*y*>;
A8: J.(x,<*y*>) = x1^y1 by A2,A4,A7;
J.(x,<*y*>) = K.(x,y) by A5,A6,FUNCT_2:15;
hence thesis by A8;
end;
end;
theorem Lm300D:
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);
A0: P[0];
A1: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume
A2: P[n];
now let m be FinSequence of NAT, X be non-empty non empty FinSequence;
assume
A3: 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
F0: n = 0;
F1: m = <*m.1*> by F0,FINSEQ_1:40,A3;
F2: X = <*X.1*> by F0,FINSEQ_1:40,A3;
n+1 in Seg (n+1) by FINSEQ_1:4;
then
F3: 1 in dom X by F0,FINSEQ_1:def 3,A3;
thus card(product X) = card (X.1) by Lm300F,F2,F3
.= m.1 by F3,A3
.= Product(m) by F1,RVSUM_1:95;
end;
suppose
F4: n <> 0;
set X1 = X | n;
reconsider m1 = m | n as FinSequence of NAT;
F6: len m1 = n by NAT_1:11,A3,FINSEQ_1:59;
F7: len X1 = n by NAT_1:11,A3,FINSEQ_1:59;
F8: dom X1 = Seg (len X1) by FINSEQ_1:def 3
.= Seg n by NAT_1:11,A3,FINSEQ_1:59;
F9: dom m1 = Seg (len m1) by FINSEQ_1:def 3
.= Seg n by NAT_1:11,A3,FINSEQ_1:59;
X1 is non-empty
proof
assume not X1 is non-empty;
then
F10: {} in rng X1 by RELAT_1:def 9;
rng X1 c= rng X by RELAT_1:70;
hence contradiction by F10,RELAT_1:def 9;
end;
then reconsider X1 as non-empty non empty FinSequence by F4,F7;
now let i be Element of NAT;
assume
F11: i in dom X1;
Seg n c= Seg (n+1) by NAT_1:11,FINSEQ_1:5;
then i in Seg (len X) by A3,F8,F11;
then
F12: i in dom X by FINSEQ_1:def 3;
thus card(X1.i) = card(X.i) by FUNCT_1:47,F11
.= m.i by A3,F12
.= m1.i by FUNCT_1:47,F11,F9,F8;
end;
then
F13: card(product X1) = Product m1 by A2,F6,F7;
F14: n < len X by NAT_1:19,A3;
F15: X is FinSequence of (rng X) by FINSEQ_1:def 4;
F16: X = X| (n + 1) by FINSEQ_1:58,A3
.= X1^(<*X.(len X) *>) by F14,F15,FINSEQ_5:83,A3;
F17: n < len m by NAT_1:19,A3;
F18: m = m| (n+1) by FINSEQ_1:58,A3
.= m1^(<*m.(len m) *>) by F17,FINSEQ_5:83,A3;
len X in Seg (len X) by A3,FINSEQ_1:4;
then
F19: len X in dom X by FINSEQ_1:def 3;
then
F20: card(X.(len X)) = m.(len m) by A3;
consider I be Function of [:product X1,(X.(len X)):],
product(X1^<*(X.(len X))*>) such that
F21: 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 F19,Lm300C;
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 RELAT_1:def 9,FINSEQ_1:39;
hence contradiction by TARSKI:def 1,F19;
end;
then product(X1^<*(X.(len X))*>) <> {} by CARD_3:26;
then
F22: dom I = [:product X1,(X.(len X)):] by FUNCT_2:def 1;
rng I = product(X1^<*(X.(len X))*>) by F21,FUNCT_2:def 3;
then
F23: card([:product X1,(X.(len X)):]) = card(product(X1^<*(X.(len X))*>))
by CARD_1:5,F21,F22,WELLORD2:def 4;
F24: card(product X) = card(product <*(product X1),(X.(len X))*>)
by CARD_1:5,F16,F23,TOPGEN_5:8;
F25: product X1 is finite set & X.(len X) is finite set by F20,F13;
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 F20,F13,F25,CARD_2:46;
hence card (product X) = Product(m) by RVSUM_1:96,F18,F24;
end;
end;
hence card (product X) = Product(m);
end;
hence P[n+1];
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A0,A1);
hence thesis;
end;
theorem Lm300:
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 natural number
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
AS1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
non zero natural number st mi=m.i & X.i = Z/Z (mi));
A1: dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3
.=Seg (len X) by PRVECT_1:def 10
.= dom X by FINSEQ_1:def 3;
A2: dom X = Seg (len X) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3,AS1;
A3: 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
A4: i in dom (carr X);
reconsider i0=i as Element of dom X by A1,A4;
consider mi be non zero natural number such that
A6: mi = m.i & X.i = Z/Z (mi) by A1,A4,AS1;
thus card((carr X).i) = card(the carrier of (X.i0)) by PRVECT_1:def 10
.=m.i by CARD_1:def 2,A6;
end;
A8: len carr X = len m by AS1,PRVECT_1:def 10;
now let i be Nat;
assume i in dom m;
then ex mi be non zero natural number st mi = m.i & X.i = Z/Z (mi)
by A2,AS1;
hence m.i in NAT by ORDINAL1:def 12;
end;
then m is FinSequence of NAT by FINSEQ_2:12;
hence thesis by A3,A8,Lm300D;
end;
theorem Lm400:
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 natural number
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
AS1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
non zero natural number 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 set 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 set;
assume
AS2: 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;
A2: 0<=xx1 & xx1 < Product(m) by AS2,NAT_1:44;
A3: 0<=xx2 & xx2 < Product(m) by AS2,NAT_1:44;
A4: I.x2 = mod(xx2,m) by AS1,AS2;
reconsider I0 = 0 as Integer;
reconsider u = {} as INT-valued FinSequence;
A5: 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;
A6: now let i be natural number;
assume
AS3: i in dom m;
A7: i in dom (mod(xx2,m)) by A4,A5,AS1,AS2,AS3;
m.i in rng m by FUNCT_1:3,AS3;
then
A8: m.i > 0 by PARTFUN3:def 1;
A9: xx1 mod (m.i) = (mod(xx1,m)).i by A5,AS3,INT_6:def 3
.= (mod(xx2,m)).i by AS1,AS2,A4
.= xx2 mod (m .i) by A7,INT_6:def 3;
then
A10: (m.i) divides ((xx1 - xx2) - I0) by INT_1:def 4,NAT_D:64,A8;
A11: (m . i) divides ((xx2 - xx1) - I0) by INT_1:def 4,NAT_D:64,A8,A9;
u.i = I0;
hence (xx1 - xx2),u.i are_congruent_mod (m.i) & (xx2 - xx1),u.i
are_congruent_mod (m.i) by A10,A11,INT_1:def 4;
end;
A12: for i being natural number st i in dom m holds I0,u.i
are_congruent_mod (m.i)
proof
let i be natural number;
assume i in dom m;
A13: u.i = I0;
I0 - I0 = (I0 - I0) * (m.i);
hence I0,u.i are_congruent_mod (m.i) by A13,INT_1:def 4,INT_1:def 3;
end;
A14: xx1 mod Product(m) >=0 & xx1 mod Product(m) < Product(m) by NAT_D:62;
A15: xx2 mod Product(m) >=0 & xx2 mod Product(m) < Product(m) by NAT_D:62;
A16: xx1 mod Product(m) = xx1 by A2,NAT_D:63;
A17: xx2 mod Product(m) = xx2 by A3,NAT_D:63;
per cases;
suppose xx2 <= xx1;
then
A18: xx1-xx2 in NAT by INT_1:5;
xx1-xx2 <= xx1 mod Product(m) by A16,XREAL_1:43,AS2;
then xx1-xx2 - Product(m) < xx1 mod Product(m) - (xx1 mod Product(m))
by A14,XREAL_1:15;
then
A19: xx1-xx2 < xx1-xx2 - (xx1-xx2 - Product(m)) by XREAL_1:46;
for i being natural number st i in dom m holds (xx1 - xx2),u.i
are_congruent_mod (m.i) by A6;
then xx1 - xx2 = I0 by INT_6:42,A12,A18,A19;
hence x1 = x2;
end;
suppose not xx2 <= xx1;
then
A20: xx2-xx1 in NAT by INT_1:5;
xx2-xx1 <= xx2 mod Product(m) by A17,XREAL_1:43,AS2;
then xx2-xx1 - Product(m) < xx2 mod Product(m) - (xx2 mod Product(m))
by A15,XREAL_1:15;
then
A21: xx2-xx1 < xx2-xx1 - (xx2-xx1 - Product(m)) by XREAL_1:46;
for i being natural number st i in dom m holds (xx2 - xx1),u.i
are_congruent_mod (m.i) by A6;
then xx2 - xx1 =I0 by INT_6:42,A12,A20,A21;
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 natural number
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
AS1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
non zero natural number st mi = m.i & X.i = Z/Z (mi));
then consider I be Homomorphism of Z/Z (Product(m)),product X such that
A1: (for x be Integer st x in the carrier of Z/Z (Product(m)) holds I.x =
mod(x,m)) by LMThX021;
A2: I is one-to-one by AS1,Lm400,A1;
A3: card(Segm Product(m)) = Product(m) by CARD_1:def 2;
A4: card(the carrier of product X) = Product(m) by AS1,Lm300;
then the carrier of product X is finite;
then I is onto by A2,A3,A4,STIRL2_1:60;
hence thesis by A1,A2;
end;