:: Isomorphisms of Direct Products of Finite Cyclic Groups
:: by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 27, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

registration

let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;

cluster <*G*> -> non empty AbGroup-yielding for FinSequence;

correctness
coherence
for b₁ being FinSequence st b₁ = <*G*> holds
( not b₁ is empty & b₁ is AbGroup-yielding );

proof end;

end;

registration

let G, F be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;

cluster <*G,F*> -> non empty AbGroup-yielding for FinSequence;

correctness
coherence
for b₁ being FinSequence st b₁ = <*G,F*> holds
( not b₁ is empty & b₁ is AbGroup-yielding );

proof end;

end;

theorem Th1: :: GROUP_14:1

for X being AbGroup ex I being Homomorphism of X,(product <*X*>) st
( I is bijective & ( for x being Element of X holds I . x = <*x*> ) )

proof end;

registration

let G, F be non empty AbGroup-yielding FinSequence;

cluster G ^ F -> AbGroup-yielding ;

correctness
coherence
G ^ F is AbGroup-yielding ;

proof end;

end;

theorem Th2: :: GROUP_14:2

for X, Y being AbGroup ex I being Homomorphism of [:X,Y:],(product <*X,Y*>) st
( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = <*x,y*> ) )

proof end;

theorem Th3: :: GROUP_14:3

for X, Y being Group-Sequence ex I being Homomorphism of [:(product X),(product Y):],(product (X ^ Y)) st
( I is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) )

proof end;

theorem Th4: :: GROUP_14:4

for G, F being AbGroup holds
( ( for x being set holds
( x is Element of (product <*G,F*>) iff ex x1 being Element of G ex x2 being Element of F st x = <*x1,x2*> ) ) & ( for x, y being Element of (product <*G,F*>)
for x1, y1 being Element of G
for x2, y2 being 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 being Element of (product <*G,F*>)
for x1 being Element of G
for x2 being Element of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) )

proof end;

theorem :: GROUP_14:5

for G, F being AbGroup holds
( ( for x being set holds
( x is Element of [:G,F:] iff ex x1 being Element of G ex x2 being Element of F st x = [x1,x2] ) ) & ( for x, y being Element of [:G,F:]
for x1, y1 being Element of G
for x2, y2 being 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 being Element of [:G,F:]
for x1 being Element of G
for x2 being Element of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) )

proof end;

theorem Th6: :: GROUP_14:6

for G, H, I being AddGroup
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

proof end;

definition

let G, H, I be AddGroup;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
:: original: *
redefine func h1 * h -> Homomorphism of G,I;
coherence
h * h1 is Homomorphism of G,I by Th6;

end;

theorem Th7: :: GROUP_14:7

for G, H being AddGroup
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G

proof end;

theorem :: GROUP_14:8

for X, Y being Group-Sequence ex I being Homomorphism of (product <*(product X),(product Y)*>),(product (X ^ Y)) st
( I is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) ) )

proof end;

theorem Th9: :: GROUP_14:9

for X, Y being AbGroup ex I being Homomorphism of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )

proof end;

theorem :: GROUP_14:10

for X being Group-Sequence
for Y being AbGroup ex I being Homomorphism of [:(product X),Y:],(product (X ^ <*Y*>)) st
( I is bijective & ( for x being Element of (product X)
for y being Element of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

proof end;

theorem Th11: :: GROUP_14:11

for n being non zero Nat holds
( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed )

proof end;

definition

let n be natural Number ;

func Z/Z n -> addLoopStr equals :: GROUP_14:def 1
addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);

coherence
addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is addLoopStr ;

end;

:: deftheorem defines Z/Z GROUP_14:def 1 :
for n being natural Number holds Z/Z n = addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);

registration

let n be natural non zero Number ;

cluster Z/Z n -> non empty strict ;

coherence
( not Z/Z n is empty & Z/Z n is strict ) ;

end;

registration

let n be natural non zero Number ;

cluster Z/Z n -> right_complementable Abelian add-associative right_zeroed ;

coherence
( Z/Z n is Abelian & Z/Z n is right_complementable & Z/Z n is add-associative & Z/Z n is right_zeroed ) by Th11;

end;

theorem Th12: :: GROUP_14:12

for X being Group-Sequence
for x, y, z being Element of (product X)
for x1, y1, z1 being FinSequence st x = x1 & y = y1 & z = z1 holds
( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) )

proof end;

theorem Th13: :: GROUP_14:13

for m being CR_Sequence
for j being Nat
for x being Integer st j in dom m holds
(x mod (Product m)) mod (m . j) = x mod (m . j)

proof end;

Lm1: for m being non zero Nat
for x being Integer holds x mod m in Segm m

proof end;

theorem Th14: :: GROUP_14:14

for m being CR_Sequence
for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being 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 being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m)

proof end;

theorem Th15: :: GROUP_14:15

for X, Y being non empty set ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )

proof end;

theorem Th16: :: GROUP_14:16

for X being non empty set holds card (product <*X*>) = card X

proof end;

theorem Th17: :: GROUP_14:17

for X being non-empty non empty FinSequence
for Y being non empty set ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds
ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

proof end;

theorem Th18: :: GROUP_14:18

for m being FinSequence of NAT
for X being non-empty non empty FinSequence st len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product m

proof end;

theorem Th19: :: GROUP_14:19

for m being CR_Sequence
for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) holds
card the carrier of (product X) = Product m

proof end;

theorem Th20: :: GROUP_14:20

for m being CR_Sequence
for X being Group-Sequence
for I being Function of (Z/Z (Product m)),(product X) st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) & ( for x being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) holds
I is one-to-one

proof end;

theorem :: GROUP_14:21

for m being CR_Sequence
for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being 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 being Integer st x in the carrier of (Z/Z (Product m)) holds
I . x = mod (x,m) ) )

proof end;