:: Cyclic Groups and Some of Their Properties - Part I
:: by Dariusz Surowik
::
:: Received November 22, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

registration
let n be non zero Nat;
cluster Segm n ->  non empty ;
coherence
 not Segm n is empty ;
end;

Lm1:  for x being set
for n being Nat st x in Segm n holds
x is Element of NAT
;

definition
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 b1 being Element of bool [:[:INT,INT:],INT:] holds
( b1 = addint iff for i1, i2 being Element of INT holds b1 . (i1,i2) = addreal . (i1,i2) )
proofend;
end;

:: deftheorem  defines addint GR_CY_1:def_1_:_
 for b1 being Element of bool [:[:INT,INT:],INT:] holds
( b1 = addint iff for i1, i2 being Element of INT holds b1 . (i1,i2) = addreal . (i1,i2) );

theorem :: GR_CY_1:1
for i1 being Element of INT st i1 = 0 holds
i1 is_a_unity_wrt addint by BINOP_2:4, SETWISEO:14;

theorem Th2: :: GR_CY_1:2
for I being FinSequence of INT holds Sum I = addint $$ I
proofend;

definition
let I be FinSequence of INT ;
:: original:Sum
redefine func Sum I ->  Element of INT  equals :: GR_CY_1:def 2
addint $$ I;
coherence
 Sum I is Element of INT
proofend;
compatibility
 for b1 being Element of INT holds
( b1 = Sum I iff b1 = addint $$ I ) by Th2;
end;

:: deftheorem  defines Sum GR_CY_1:def_2_:_
 for I being FinSequence of INT holds Sum I = addint $$ I;

theorem Th3: :: GR_CY_1:3
Sum (<*> INT) = 0 by BINOP_2:4, FINSOP_1:10;

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

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*>))
proofend;

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

:: Finite groups and their some properties
theorem Th5: :: GR_CY_1:5
for G being Group
for b, a being Element of G holds
( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
proofend;

theorem Th6: :: GR_CY_1:6
for G being finite Group
for a being Element of G holds not a is being_of_order_0
proofend;

theorem Th7: :: GR_CY_1:7
for G being finite Group
for a being Element of G holds ord a = card (gr {a})
proofend;

theorem Th8: :: GR_CY_1:8
for G being finite Group
for a being Element of G holds ord a divides card G
proofend;

theorem Th9: :: GR_CY_1:9
for G being finite Group
for a being Element of G holds a |^ (card G) = 1_ G
proofend;

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

registration
let G be non empty associative multMagma ;
cluster multMagma(# the carrier of G, the multF of G #) ->  associative ;
coherence
 multMagma(# the carrier of G, the multF of G #) is associative
proofend;
end;

registration
let G be Group;
cluster multMagma(# the carrier of G, the multF of G #) ->  Group-like ;
coherence
 multMagma(# the carrier of G, the multF of G #) is Group-like
proofend;
end;

theorem Th11: :: GR_CY_1:11
for G being finite strict Group st card G > 1 holds
ex a being Element of G st a <> 1_ G
proofend;

theorem :: GR_CY_1:12
for p being Nat
for G being finite strict Group st card G = p &amp; p is prime holds
for H being strict Subgroup of G holds
( H = (1). G or H = G )
proofend;

definition
func INT.Group  ->  non empty strict multMagma  equals :: GR_CY_1:def 3
 multMagma(# INT,addint #);
coherence
 multMagma(# INT,addint #) is non empty strict multMagma ;
end;

:: deftheorem  defines INT.Group GR_CY_1:def_3_:_
 INT.Group = multMagma(# INT,addint #);

registration
cluster INT.Group  ->  non empty strict Group-like associative ;
coherence
 ( INT.Group is associative &amp; INT.Group is Group-like )
proofend;
end;

registration
cluster the carrier of INT.Group ->  integer-membered ;
coherence
 the carrier of INT.Group is integer-membered ;
end;

registration
let a, b be Element of INT.Group;
identifya * b with a + b;
compatibility
 a * b = a + b by BINOP_2:def_20;
end;

registration
let n be Nat;
cluster Segm n ->  natural-membered ;
coherence
 Segm n is natural-membered ;
end;

definition
let n be Nat;
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
 ex b1 being BinOp of (Segm n) st
for k, l being Element of Segm n holds b1 . (k,l) = (k + l) mod n
proofend;
uniqueness
 for b1, b2 being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b1 . (k,l) = (k + l) mod n ) &amp; ( for k, l being Element of Segm n holds b2 . (k,l) = (k + l) mod n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines addint GR_CY_1:def_4_:_
 for n being Nat st n > 0 holds
for b2 being BinOp of (Segm n) holds
( b2 = addint n iff for k, l being Element of Segm n holds b2 . (k,l) = (k + l) mod n );

definition
let n be non zero Nat;
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) #) is non empty strict multMagma ;
end;

:: deftheorem  defines INT.Group GR_CY_1:def_5_:_
 for n being non zero Nat holds INT.Group n = multMagma(# (Segm n),(addint n) #);

registration
let n be non zero Nat;
cluster INT.Group n ->  non empty finite strict Group-like associative ;
coherence
 ( INT.Group n is finite &amp; INT.Group n is associative &amp; INT.Group n is Group-like )
proofend;
end;

theorem Th13: :: GR_CY_1:13
1_ INT.Group = 0
proofend;

theorem Th14: :: GR_CY_1:14
for n being non zero Nat holds 1_ (INT.Group n) = 0
proofend;

definition
let h be Integer;
func @' h ->  Element of INT.Group equals :: GR_CY_1:def 6
h;
coherence
 h is Element of INT.Group by INT_1:def_2;
end;

:: deftheorem  defines @' GR_CY_1:def_6_:_
 for h being Integer holds @' h = h;

theorem Th15: :: GR_CY_1:15
for h being Element of INT.Group holds h " = - h
proofend;

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

theorem Th16: :: GR_CY_1:16
for j1 being Integer holds j1 = (@' 1) |^ j1
proofend;

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

definition
let IT be Group;
attrIT is cyclic  means :Def7: :: GR_CY_1:def 7
 ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a};
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} );

registration
cluster non empty strict unital Group-like associative cyclic for multMagma ;
existence
 ex b1 being Group st
( b1 is strict &amp; b1 is cyclic )
proofend;
end;

registration
let G be Group;
cluster (1). G ->  cyclic ;
coherence
 (1). G is cyclic
proofend;
end;

registration
cluster non empty finite strict unital Group-like associative cyclic for multMagma ;
existence
 ex b1 being Group st
( b1 is strict &amp; b1 is finite &amp; b1 is cyclic )
proofend;
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 )
proofend;

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

theorem Th19: :: GR_CY_1:19
for G being finite Group holds
( G is cyclic iff ex a being Element of G st ord a = card G )
proofend;

theorem :: GR_CY_1:20
for G being finite Group
for H being strict Subgroup of G st G is cyclic holds
H is cyclic
proofend;

theorem :: GR_CY_1:21
for G being finite strict Group st card G is prime holds
G is cyclic Group
proofend;

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

registration
cluster non empty Group-like associative cyclic  ->  commutative for multMagma ;
coherence
 for b1 being Group st b1 is cyclic holds
b1 is commutative
proofend;
end;

theorem :: GR_CY_1:23
INT.Group = gr {(@' 1)} by Lm5;

registration
cluster INT.Group  ->  non empty strict cyclic ;
coherence
 INT.Group is cyclic
proofend;
end;

registration
let n be non zero Nat;
cluster INT.Group n ->  non empty strict cyclic ;
coherence
 INT.Group n is cyclic
proofend;
end;