:: by Dariusz Surowik

::

:: Received November 22, 1991

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

Lm1: for x being set

for n being Nat st x in Segm n holds

x is Element of NAT

;

definition

for b_{1} being Element of bool [:[:INT,INT:],INT:] holds

( b_{1} = addint iff for i1, i2 being Element of INT holds b_{1} . (i1,i2) = addreal . (i1,i2) )
end;

redefine func addint means :: GR_CY_1:def 1

for i1, i2 being Element of INT holds it . (i1,i2) = addreal . (i1,i2);

compatibility for i1, i2 being Element of INT holds it . (i1,i2) = addreal . (i1,i2);

for b

( b

proof end;

:: deftheorem defines addint GR_CY_1:def 1 :

for b_{1} being Element of bool [:[:INT,INT:],INT:] holds

( b_{1} = addint iff for i1, i2 being Element of INT holds b_{1} . (i1,i2) = addreal . (i1,i2) );

for b

( b

theorem :: GR_CY_1:1

definition

let I be FinSequence of INT ;

coherence

Sum I is Element of INT

for b_{1} being Element of INT holds

( b_{1} = Sum I iff b_{1} = addint $$ I )
by Th2;

end;
coherence

Sum I is Element of INT

proof end;

compatibility for b

( b

Lm2: for G being Group

for a being Element of G holds Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT))

proof end;

Lm3: for G being Group

for a being Element of G

for I being FinSequence of INT

for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds

Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))

proof end;

theorem Th4: :: GR_CY_1:4

for G being Group

for a being Element of G

for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)

for a being Element of G

for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)

proof end;

:: Finite groups and their some properties

theorem Th5: :: GR_CY_1:5

for G being Group

for a, b being Element of G holds

( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )

for a, b being Element of G holds

( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )

proof end;

theorem Th10: :: GR_CY_1:10

for n being Nat

for G being finite Group

for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))

for G being finite Group

for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))

proof end;

registration

let G be non empty associative multMagma ;

coherence

multMagma(# the carrier of G, the multF of G #) is associative by BINOP_1:def 3;

end;
coherence

multMagma(# the carrier of G, the multF of G #) is associative by BINOP_1:def 3;

registration
end;

theorem :: GR_CY_1:12

for p being Nat

for G being finite strict Group st card G = p & p is prime holds

for H being strict Subgroup of G holds

( H = (1). G or H = G )

for G being finite strict Group st card G = p & p is prime holds

for H being strict Subgroup of G holds

( H = (1). G or H = G )

proof end;

definition

let n be natural Number ;

assume A1: n > 0 ;

ex b_{1} being BinOp of (Segm n) st

for k, l being Element of Segm n holds b_{1} . (k,l) = (k + l) mod n

for b_{1}, b_{2} being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b_{1} . (k,l) = (k + l) mod n ) & ( for k, l being Element of Segm n holds b_{2} . (k,l) = (k + l) mod n ) holds

b_{1} = b_{2}

end;
assume A1: n > 0 ;

func addint n -> BinOp of (Segm n) means :Def4: :: GR_CY_1:def 4

for k, l being Element of Segm n holds it . (k,l) = (k + l) mod n;

existence for k, l being Element of Segm n holds it . (k,l) = (k + l) mod n;

ex b

for k, l being Element of Segm n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines addint GR_CY_1:def 4 :

for n being natural Number st n > 0 holds

for b_{2} being BinOp of (Segm n) holds

( b_{2} = addint n iff for k, l being Element of Segm n holds b_{2} . (k,l) = (k + l) mod n );

for n being natural Number st n > 0 holds

for b

( b

definition

let n be non zero Nat;

multMagma(# (Segm n),(addint n) #) is non empty strict multMagma ;

end;
func INT.Group n -> non empty strict multMagma equals :: GR_CY_1:def 5

multMagma(# (Segm n),(addint n) #);

coherence multMagma(# (Segm n),(addint n) #);

multMagma(# (Segm n),(addint n) #) is non empty strict multMagma ;

:: deftheorem defines INT.Group GR_CY_1:def 5 :

for n being non zero Nat holds INT.Group n = multMagma(# (Segm n),(addint n) #);

for n being non zero Nat holds INT.Group n = multMagma(# (Segm n),(addint n) #);

registration

let n be non zero Nat;

coherence

( INT.Group n is finite & INT.Group n is associative & INT.Group n is Group-like )

end;
coherence

( INT.Group n is finite & INT.Group n is associative & INT.Group n is Group-like )

proof end;

Lm4: for k being Nat holds (@' 1) |^ k = k

proof end;

Lm5: INT.Group = gr {(@' 1)}

proof end;

:: deftheorem Def7 defines cyclic GR_CY_1:def 7 :

for IT being Group holds

( IT is cyclic iff ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a} );

for IT being Group holds

( IT is cyclic iff ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a} );

registration
end;

registration

existence

ex b_{1} being Group st

( b_{1} is strict & b_{1} is finite & b_{1} is cyclic )

end;
ex b

( b

proof end;

theorem Th17: :: GR_CY_1:17

for G being Group holds

( G is cyclic Group iff ex a being Element of G st

for b being Element of G ex j1 being Integer st b = a |^ j1 )

( G is cyclic Group iff ex a being Element of G st

for b being Element of G ex j1 being Integer st b = a |^ j1 )

proof end;

theorem Th18: :: GR_CY_1:18

for G being finite Group holds

( G is cyclic iff ex a being Element of G st

for b being Element of G ex n being Nat st b = a |^ n )

( G is cyclic iff ex a being Element of G st

for b being Element of G ex n being Nat st b = a |^ n )

proof end;

theorem Th22: :: GR_CY_1:22

for n being non zero Nat ex g being Element of (INT.Group n) st

for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

proof end;

registration
end;

registration
end;