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

begin

registration

let n be natural non zero number ;
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

canceled;
redefine func addint means :: GR_CY_1:def 2
for i1, i2 being Element of INT holds it . (i1,i2) = addreal . (i1,i2);
compatibility
for b₁ being Element of bool [:[:INT,INT:],INT:] holds
( b₁ = addint iff for i1, i2 being Element of INT holds b₁ . (i1,i2) = addreal . (i1,i2) )

proof end;

end;

:: deftheorem GR_CY_1:def 1 :
canceled;

:: deftheorem defines addint GR_CY_1:def 2 :
for b₁ being Element of bool [:[:INT,INT:],INT:] holds
( b₁ = addint iff for i1, i2 being Element of INT holds b₁ . (i1,i2) = addreal . (i1,i2) );

theorem :: GR_CY_1:1

canceled;

theorem :: GR_CY_1:2

canceled;

theorem :: GR_CY_1:3

canceled;

theorem :: GR_CY_1:4

canceled;

theorem :: GR_CY_1:5

canceled;

theorem :: GR_CY_1:6

canceled;

theorem :: GR_CY_1:7

canceled;

theorem :: GR_CY_1:8

canceled;

theorem :: GR_CY_1:9

canceled;

theorem :: GR_CY_1:10

canceled;

theorem :: GR_CY_1:11

canceled;

theorem :: GR_CY_1:12

canceled;

theorem :: GR_CY_1:13

canceled;

theorem :: GR_CY_1:14

canceled;

theorem :: GR_CY_1:15

for i1 being Element of INT st i1 = 0 holds
i1 is_a_unity_wrt addint by BINOP_2:4, SETWISEO:22;

theorem Th16: :: GR_CY_1:16

for I being FinSequence of INT holds Sum I = addint $$ I

proof end;

definition

let I be FinSequence of INT ;
:: original: Sum
redefine func Sum I -> Element of INT equals :: GR_CY_1:def 3
addint $$ I;
coherence
Sum I is Element of INT

proof end;

compatibility
for b₁ being Element of INT holds
( b₁ = Sum I iff b₁ = addint $$ I ) by Th16;

end;

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

theorem :: GR_CY_1:17

canceled;

theorem :: GR_CY_1:18

canceled;

theorem :: GR_CY_1:19

canceled;

theorem :: GR_CY_1:20

canceled;

theorem :: GR_CY_1:21

canceled;

theorem Th22: :: GR_CY_1:22

Sum (<*> INT) = 0 by BINOP_2:4, FINSOP_1:11;

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 :: GR_CY_1:23

canceled;

theorem Th24: :: GR_CY_1:24

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)

proof end;

theorem Th25: :: GR_CY_1:25

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 )

proof end;

theorem Th26: :: GR_CY_1:26

for G being finite Group
for a being Element of G holds not a is being_of_order_0

proof end;

theorem Th27: :: GR_CY_1:27

for G being finite Group
for a being Element of G holds ord a = card (gr {a})

proof end;

theorem Th28: :: GR_CY_1:28

for G being finite Group
for a being Element of G holds ord a divides card G

proof end;

theorem Th29: :: GR_CY_1:29

for G being finite Group
for a being Element of G holds a |^ (card G) = 1_ G

proof end;

theorem Th30: :: GR_CY_1:30

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

proof end;

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

proof end;

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

proof end;

end;

theorem Th31: :: GR_CY_1:31

for G being finite strict Group st card G > 1 holds
ex a being Element of G st a <> 1_ G

proof end;

theorem :: GR_CY_1:32

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 )

proof end;

theorem Th33: :: GR_CY_1:33

( multMagma(# INT,addint #) is associative & multMagma(# INT,addint #) is Group-like )

proof end;

definition

func INT.Group -> strict Group equals :: GR_CY_1:def 4
multMagma(# INT,addint #);
coherence
multMagma(# INT,addint #) is strict Group by Th33;

end;

:: deftheorem defines INT.Group GR_CY_1:def 4 :
INT.Group = multMagma(# INT,addint #);

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;
identify a * b with a + b;
compatibility
a * b = a + b by BINOP_2:def 20;

end;

registration

let n be natural number ;
cluster Segm n -> natural-membered ;
coherence
Segm n is natural-membered ;

end;

definition

let n be natural number ;
assume A1: n > 0 ;
func addint n -> BinOp of (Segm n) means :Def5: :: GR_CY_1:def 5
for k, l being Element of Segm n holds it . (k,l) = (k + l) mod n;
existence
ex b₁ being BinOp of (Segm n) st
for k, l being Element of Segm n holds b₁ . (k,l) = (k + l) mod n

proof end;

uniqueness
for b₁, b₂ being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b₁ . (k,l) = (k + l) mod n ) & ( for k, l being Element of Segm n holds b₂ . (k,l) = (k + l) mod n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines addint GR_CY_1:def 5 :
for n being natural number st n > 0 holds
for b₂ being BinOp of (Segm n) holds
( b₂ = addint n iff for k, l being Element of Segm n holds b₂ . (k,l) = (k + l) mod n );

theorem Th34: :: GR_CY_1:34

for n being natural non zero number holds
( multMagma(# (Segm n),(addint n) #) is associative & multMagma(# (Segm n),(addint n) #) is Group-like )

proof end;

definition

let n be natural number ;
assume A1: n > 0 ;
func INT.Group n -> strict Group equals :Def6: :: GR_CY_1:def 6
multMagma(# (Segm n),(addint n) #);
coherence
multMagma(# (Segm n),(addint n) #) is strict Group by A1, Th34;

end;

:: deftheorem Def6 defines INT.Group GR_CY_1:def 6 :
for n being natural number st n > 0 holds
INT.Group n = multMagma(# (Segm n),(addint n) #);

registration

let n be natural non zero number ;
cluster INT.Group n -> finite strict ;
coherence
INT.Group n is finite

proof end;

end;

theorem Th35: :: GR_CY_1:35

1_ INT.Group = 0

proof end;

theorem Th36: :: GR_CY_1:36

for n being natural number st n > 0 holds
1_ (INT.Group n) = 0

proof end;

definition

let h be Integer;
canceled;
func @' h -> Element of INT.Group equals :: GR_CY_1:def 8
h;
coherence
h is Element of INT.Group by INT_1:def 2;

end;

:: deftheorem GR_CY_1:def 7 :
canceled;

:: deftheorem defines @' GR_CY_1:def 8 :
for h being Integer holds @' h = h;

theorem Th37: :: GR_CY_1:37

for h being Element of INT.Group holds h " = - h

proof end;

theorem :: GR_CY_1:38

canceled;

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

proof end;

theorem Th39: :: GR_CY_1:39

for j1 being Integer holds j1 = (@' 1) |^ j1

proof end;

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

proof end;

definition

let IT be Group;
attr IT is cyclic means :Def9: :: GR_CY_1:def 9
ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a};

end;

:: deftheorem Def9 defines cyclic GR_CY_1:def 9 :
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 multMagma ;
existence
ex b₁ being Group st
( b₁ is strict & b₁ is cyclic )

proof end;

end;

theorem Th40: :: GR_CY_1:40

for G being Group holds (1). G is cyclic

proof end;

registration

let G be Group;
cluster (1). G -> cyclic ;
coherence
(1). G is cyclic by Th40;

end;

registration

cluster non empty finite strict unital Group-like associative cyclic multMagma ;
existence
ex b₁ being Group st
( b₁ is strict & b₁ is finite & b₁ is cyclic )

proof end;

end;

theorem Th41: :: GR_CY_1:41

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 )

proof end;

theorem Th42: :: GR_CY_1:42

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 )

proof end;

theorem Th43: :: GR_CY_1:43

for G being finite Group holds
( G is cyclic iff ex a being Element of G st ord a = card G )

proof end;

theorem :: GR_CY_1:44

for G being finite Group
for H being strict Subgroup of G st G is cyclic holds
H is cyclic

proof end;

theorem :: GR_CY_1:45

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

proof end;

theorem Th46: :: GR_CY_1:46

for n being Nat st n > 0 holds
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

proof end;

registration

cluster non empty Group-like associative cyclic -> commutative multMagma ;
coherence
for b₁ being Group st b₁ is cyclic holds
b₁ is commutative

proof end;

end;

theorem :: GR_CY_1:47

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

theorem Th48: :: GR_CY_1:48

INT.Group is cyclic

proof end;

registration

cluster INT.Group -> strict cyclic ;
coherence
INT.Group is cyclic by Th48;

end;

theorem Th49: :: GR_CY_1:49

for n being Nat st n > 0 holds
INT.Group n is cyclic

proof end;

registration

let n be natural non zero number ;
cluster INT.Group n -> strict cyclic ;
coherence
INT.Group n is cyclic by Th49;

end;

theorem :: GR_CY_1:50

INT.Group is commutative ;