:: GR_CY_1 semantic presentation

definition

let n be natural number ;
assume A1: n > 0 ;
func Segm n -> non empty Subset of NAT equals :Def1: :: GR_CY_1:def 1
{ p where p is Nat : p < n } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Segm GR_CY_1:def 1 :

Lm1: for x being set
for n being Nat st n > 0 & x in Segm n holds
x is Nat
;

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 Th10: :: GR_CY_1:10

for n, s being natural number st n > 0 holds
( s in Segm n iff s < n )

proof end;

theorem :: GR_CY_1:11

canceled;

theorem :: GR_CY_1:12

for n being natural number st n > 0 holds
0 in Segm n by Th10;

theorem Th13: :: GR_CY_1:13

Segm 1 = {0}

proof end;

definition

redefine func addint means :: GR_CY_1:def 2
for i1, i2 being Element of INT holds it . i1,i2 = addreal . i1,i2;
compatibility

proof end;

end;

:: deftheorem defines addint GR_CY_1:def 2 :

theorem Th14: :: GR_CY_1:14

for j1, j2 being Integer holds addint . j1,j2 = j1 + j2

proof end;

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;

definition

let F be FinSequence of INT ;
func Sum F -> Integer equals :: GR_CY_1:def 3
addint $$ F;
coherence ;

end;

:: deftheorem defines Sum GR_CY_1:def 3 :

theorem :: GR_CY_1:16

canceled;

theorem :: GR_CY_1:17

canceled;

theorem :: GR_CY_1:18

canceled;

theorem :: GR_CY_1:19

canceled;

theorem Th20: :: GR_CY_1:20

for i1 being Element of INT
for I being FinSequence of INT holds Sum (I ^ <*i1*>) = (Sum I) + (@ i1)

proof end;

theorem :: GR_CY_1:21

for i1 being Element of INT holds Sum <*i1*> = i1 by FINSOP_1:12;

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 Group
for a being Element of G st G is finite holds
a is_not_of_order_0

proof end;

theorem Th27: :: GR_CY_1:27

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

proof end;

theorem Th28: :: GR_CY_1:28

for G being Group
for a being Element of G st G is finite holds
ord a divides ord G

proof end;

theorem Th29: :: GR_CY_1:29

for G being Group
for a being Element of G st G is finite holds
a |^ (ord G) = 1. G

proof end;

theorem Th30: :: GR_CY_1:30

for n being Nat
for G being Group
for a being Element of G st G is finite holds
(a |^ n) " = a |^ ((ord G) - (n mod (ord G)))

proof end;

theorem Th31: :: GR_CY_1:31

for G being strict Group st ord 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 strict Group st G is finite & ord 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

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

proof end;

definition

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

end;

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines addint GR_CY_1:def 5 :

theorem Th34: :: GR_CY_1:34

for n being natural number st n > 0 holds
( HGrStr(# (Segm n),(addint n) #) is associative & HGrStr(# (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
HGrStr(# (Segm n),(addint n) #);
coherence by A1, Th34;

end;

:: deftheorem Def6 defines INT.Group GR_CY_1:def 6 :

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 Element of INT.Group ;
func @' h -> Integer equals :: GR_CY_1:def 7
h;
coherence by INT_1:def 2;

end;

:: deftheorem defines @' GR_CY_1:def 7 :

definition

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

end;

:: deftheorem defines @' GR_CY_1:def 8 :

theorem Th37: :: GR_CY_1:37

for h being Element of INT.Group holds h " = - (@' h)

proof end;

Lm4: for h, g being Element of INT.Group
for A, B being Integer st h = A & g = B holds
h * g = A + B
by Th14;

theorem Th38: :: GR_CY_1:38

for h being Element of INT.Group st h = 1 holds
for k being Nat holds h |^ k = k

proof end;

theorem Th39: :: GR_CY_1:39

for h being Element of INT.Group
for j1 being Integer st h = 1 holds
j1 = h |^ j1

proof end;

Lm5: ex a being Element of INT.Group st HGrStr(# the carrier of INT.Group ,the mult of INT.Group #) = gr {a}

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 HGrStr(# the carrier of IT,the mult of IT #) = gr {a};

end;