:: GR_CY_2 semantic presentation

theorem :: GR_CY_2:1

canceled;

theorem :: GR_CY_2:2

canceled;

theorem :: GR_CY_2:3

canceled;

theorem :: GR_CY_2:4

canceled;

theorem :: GR_CY_2:5

canceled;

theorem :: GR_CY_2:6

for G being Group
for a, b being Element of G
for k being Nat st ord a > 1 & a = b |^ k holds
k <> 0

proof end;

Lm1: for G being Group st G is finite holds
ord G > 0
by GROUP_1:90;

theorem :: GR_CY_2:7

canceled;

theorem Th8: :: GR_CY_2:8

for G being Group
for a being Element of G holds a in gr {a}

proof end;

theorem Th9: :: GR_CY_2:9

for G being Group
for G1 being Subgroup of G
for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}

proof end;

theorem Th10: :: GR_CY_2:10

for G being Group
for a being Element of G holds gr {a} is cyclic Group

proof end;

theorem Th11: :: GR_CY_2:11

for G being strict Group
for b being Element of G holds
( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

proof end;

theorem Th12: :: GR_CY_2:12

for G being strict Group
for b being Element of G st G is finite holds
( ( for a being Element of G ex p being Nat st a = b |^ p ) iff G = gr {b} )

proof end;

theorem Th13: :: GR_CY_2:13

for G being strict Group
for a being Element of G st G is finite & G = gr {a} holds
for G1 being strict Subgroup of G ex p being Nat st G1 = gr {(a |^ p)}

proof end;

theorem Th14: :: GR_CY_2:14

for G being Group
for a being Element of G
for n, p, s being Nat st G is finite & G = gr {a} & ord G = n & n = p * s holds
ord (a |^ p) = s

proof end;

theorem Th15: :: GR_CY_2:15

for G being Group
for a being Element of G
for s, k being Nat st s divides k holds
a |^ k in gr {(a |^ s)}

proof end;

theorem Th16: :: GR_CY_2:16

for G being Group
for a being Element of G
for s, k being Nat st G is finite & ord (gr {(a |^ s)}) = ord (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}

proof end;

theorem Th17: :: GR_CY_2:17

for G being Group
for G1 being Subgroup of G
for a being Element of G
for n, p, k being Nat st G is finite & ord G = n & G = gr {a} & ord G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p

proof end;

theorem :: GR_CY_2:18

for n, k being Nat
for G being strict Group
for a being Element of G st G is finite & G = gr {a} & ord G = n holds
( G = gr {(a |^ k)} iff k hcf n = 1 )

proof end;

theorem Th19: :: GR_CY_2:19

for Gc being cyclic Group
for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} & g in H holds
HGrStr(# the carrier of Gc,the mult of Gc #) = HGrStr(# the carrier of H,the mult of H #)

proof end;

theorem Th20: :: GR_CY_2:20

for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )

proof end;

definition

let n be Nat;
assume A1: n > 0 ;
let h be Element of (INT.Group n);
func @ h -> Nat equals :Def1: :: GR_CY_2:def 1
h;
coherence

proof end;

end;

:: deftheorem Def1 defines @ GR_CY_2:def 1 :

theorem Th21: :: GR_CY_2:21

for n being Nat
for Gc being strict cyclic Group st Gc is finite & ord Gc = n holds
INT.Group n,Gc are_isomorphic

proof end;

theorem :: GR_CY_2:22

for Gc being strict cyclic Group st not Gc is finite holds
INT.Group ,Gc are_isomorphic

proof end;

theorem Th23: :: GR_CY_2:23

for Gc, Hc being strict cyclic Group st Hc is finite & Gc is finite & ord Hc = ord Gc holds
Hc,Gc are_isomorphic

proof end;

theorem Th24: :: GR_CY_2:24

for p being Nat
for F, G being strict Group st F is finite & G is finite & ord F = p & ord G = p & p is prime holds
F,G are_isomorphic

proof end;

theorem :: GR_CY_2:25

for F, G being strict Group st F is finite & G is finite & ord F = 2 & ord G = 2 holds
F,G are_isomorphic by Th24, INT_2:44;

theorem :: GR_CY_2:26

for G being strict Group st G is finite & ord G = 2 holds
for H being strict Subgroup of G holds
( H = (1). G or H = G ) by GR_CY_1:32, INT_2:44;

theorem :: GR_CY_2:27

for G being strict Group st G is finite & ord G = 2 holds
G is cyclic Group by GR_CY_1:45, INT_2:44;

theorem :: GR_CY_2:28

for n being Nat
for G being strict Group st G is finite & G is cyclic Group & ord G = n holds
for p being Nat st p divides n holds
ex G1 being strict Subgroup of G st
( ord G1 = p & ( for G2 being strict Subgroup of G st ord G2 = p holds
G2 = G1 ) )

proof end;

theorem :: GR_CY_2:29

for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is_epimorphism

proof end;

theorem Th30: :: GR_CY_2:30

for n being Nat
for Gc being strict cyclic Group st Gc is finite & ord Gc = n & ex k being Nat st n = 2 * k holds
ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )

proof end;

registration

let G be Group;
cluster center G -> normal ;
coherence by GROUP_5:90;

end;

theorem :: GR_CY_2:31

for n being Nat
for Gc being strict cyclic Group st Gc is finite & ord Gc = n & ex k being Nat st n = 2 * k holds
ex H being Subgroup of Gc st
( ord H = 2 & H is cyclic Group )

proof end;

theorem Th32: :: GR_CY_2:32

for F being Group
for G being strict Group
for g being Homomorphism of G,F st G is cyclic Group holds
Image g is cyclic Group

proof end;

theorem :: GR_CY_2:33

for G, F being strict Group st G,F are_isomorphic & ( G is cyclic Group or F is cyclic Group ) holds
( G is cyclic Group & F is cyclic Group )

proof end;