:: by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 27, 2012

:: Copyright (c) 2012-2017 Association of Mizar Users

registration

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

correctness

coherence

for b_{1} being FinSequence st b_{1} = <*G*> holds

( not b_{1} is empty & b_{1} is AbGroup-yielding );

end;
correctness

coherence

for b

( not b

proof end;

registration

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

correctness

coherence

for b_{1} being FinSequence st b_{1} = <*G,F*> holds

( not b_{1} is empty & b_{1} is AbGroup-yielding );

end;
correctness

coherence

for b

( not b

proof 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*> ) )

( 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;

correctness

coherence

G ^ F is AbGroup-yielding ;

end;
correctness

coherence

G ^ F is AbGroup-yielding ;

proof 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*> ) )

( 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 ) ) )

( 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)*> ) )

( ( 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)] ) )

( ( 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

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;
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;

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

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 ) ) )

( 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*>] ) )

( 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 ) ) )

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 )

( 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 ;

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

end;
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) #);

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

:: 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) #);

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
end;

registration

let n be natural non zero Number ;

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;
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;

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)) )

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)

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)

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*>] ) )

( 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 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 ) ) )

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

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

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

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) ) )

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;