:: GR_CY_2 semantic presentation

theorem Th1: :: GR_CY_2:1

canceled;

theorem Th2: :: GR_CY_2:2

canceled;

theorem Th3: :: GR_CY_2:3

canceled;

theorem Th4: :: GR_CY_2:4

canceled;

theorem Th5: :: GR_CY_2:5

canceled;

theorem Th6: :: GR_CY_2:6

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Nat st ord b₂ > 1 & b₂ = b₃ |^ b₄ holds
b₄ <> 0

proof end;

Lemma1: for b₁ being Group st b₁ is finite holds
ord b₁ > 0
by GROUP_1:90;

theorem Th7: :: GR_CY_2:7

canceled;

theorem Th8: :: GR_CY_2:8

for b₁ being Group
for b₂ being Element of b₁ holds b₂ in gr {b₂}

proof end;

theorem Th9: :: GR_CY_2:9

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
gr {b₃} = gr {b₄}

proof end;

theorem Th10: :: GR_CY_2:10

for b₁ being Group
for b₂ being Element of b₁ holds gr {b₂} is cyclic Group

proof end;

theorem Th11: :: GR_CY_2:11

for b₁ being strict Group
for b₂ being Element of b₁ holds
( ( for b₃ being Element of b₁ ex b₄ being Integer st b₃ = b₂ |^ b₄ ) iff b₁ = gr {b₂} )

proof end;

theorem Th12: :: GR_CY_2:12

for b₁ being strict Group
for b₂ being Element of b₁ st b₁ is finite holds
( ( for b₃ being Element of b₁ ex b₄ being Nat st b₃ = b₂ |^ b₄ ) iff b₁ = gr {b₂} )

proof end;

theorem Th13: :: GR_CY_2:13

for b₁ being strict Group
for b₂ being Element of b₁ st b₁ is finite & b₁ = gr {b₂} holds
for b₃ being strict Subgroup of b₁ ex b₄ being Nat st b₃ = gr {(b₂ |^ b₄)}

proof end;

theorem Th14: :: GR_CY_2:14

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄, b₅ being Nat st b₁ is finite & b₁ = gr {b₂} & ord b₁ = b₃ & b₃ = b₄ * b₅ holds
ord (b₂ |^ b₄) = b₅

proof end;

theorem Th15: :: GR_CY_2:15

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Nat st b₃ divides b₄ holds
b₂ |^ b₄ in gr {(b₂ |^ b₃)}

proof end;

theorem Th16: :: GR_CY_2:16

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Nat st b₁ is finite & ord (gr {(b₂ |^ b₃)}) = ord (gr {(b₂ |^ b₄)}) & b₂ |^ b₄ in gr {(b₂ |^ b₃)} holds
gr {(b₂ |^ b₃)} = gr {(b₂ |^ b₄)}

proof end;

theorem Th17: :: GR_CY_2:17

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being Element of b₁
for b₄, b₅, b₆ being Nat st b₁ is finite & ord b₁ = b₄ & b₁ = gr {b₃} & ord b₂ = b₅ & b₂ = gr {(b₃ |^ b₆)} holds
b₄ divides b₆ * b₅

proof end;

theorem Th18: :: GR_CY_2:18

for b₁, b₂ being Nat
for b₃ being strict Group
for b₄ being Element of b₃ st b₃ is finite & b₃ = gr {b₄} & ord b₃ = b₁ holds
( b₃ = gr {(b₄ |^ b₂)} iff b₂ hcf b₁ = 1 )

proof end;

theorem Th19: :: GR_CY_2:19

for b₁ being cyclic Group
for b₂ being Subgroup of b₁
for b₃ being Element of b₁ st b₁ = gr {b₃} & b₃ in b₂ holds
HGrStr(# the carrier of b₁,the mult of b₁ #) = HGrStr(# the carrier of b₂,the mult of b₂ #)

proof end;

theorem Th20: :: GR_CY_2:20

for b₁ being cyclic Group
for b₂ being Element of b₁ st b₁ = gr {b₂} holds
( b₁ is finite iff ex b₃, b₄ being Integer st
( b₃ <> b₄ & b₂ |^ b₃ = b₂ |^ b₄ ) )

proof end;

definition

let c₁ be Nat;
assume E14: c₁ > 0 ;
let c₂ be Element of (INT.Group c₁);
func @ c₂ -> Nat equals :Def1: :: GR_CY_2:def 1
a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines @ GR_CY_2:def 1 :

theorem Th21: :: GR_CY_2:21

for b₁ being Nat
for b₂ being strict cyclic Group st b₂ is finite & ord b₂ = b₁ holds
INT.Group b₁,b₂ are_isomorphic

proof end;

theorem Th22: :: GR_CY_2:22

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

proof end;

theorem Th23: :: GR_CY_2:23

for b₁, b₂ being strict cyclic Group st b₂ is finite & b₁ is finite & ord b₂ = ord b₁ holds
b₂,b₁ are_isomorphic

proof end;

theorem Th24: :: GR_CY_2:24

for b₁ being Nat
for b₂, b₃ being strict Group st b₂ is finite & b₃ is finite & ord b₂ = b₁ & ord b₃ = b₁ & b₁ is prime holds
b₂,b₃ are_isomorphic

proof end;

theorem Th25: :: GR_CY_2:25

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

theorem Th26: :: GR_CY_2:26

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

theorem Th27: :: GR_CY_2:27

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

theorem Th28: :: GR_CY_2:28

for b₁ being Nat
for b₂ being strict Group st b₂ is finite & b₂ is cyclic Group & ord b₂ = b₁ holds
for b₃ being Nat st b₃ divides b₁ holds
ex b₄ being strict Subgroup of b₂ st
( ord b₄ = b₃ & ( for b₅ being strict Subgroup of b₂ st ord b₅ = b₃ holds
b₅ = b₄ ) )

proof end;

theorem Th29: :: GR_CY_2:29

for b₁ being cyclic Group
for b₂ being Element of b₁ st b₁ = gr {b₂} holds
for b₃ being Group
for b₄ being Homomorphism of b₃,b₁ st b₂ in Image b₄ holds
b₄ is_epimorphism

proof end;

theorem Th30: :: GR_CY_2:30

for b₁ being Nat
for b₂ being strict cyclic Group st b₂ is finite & ord b₂ = b₁ & ex b₃ being Nat st b₁ = 2 * b₃ holds
ex b₃ being Element of b₂ st
( ord b₃ = 2 & ( for b₄ being Element of b₂ st ord b₄ = 2 holds
b₃ = b₄ ) )

proof end;

registration

let c₁ be Group;
cluster center a₁ -> normal ;
coherence by GROUP_5:90;

end;

theorem Th31: :: GR_CY_2:31

for b₁ being Nat
for b₂ being strict cyclic Group st b₂ is finite & ord b₂ = b₁ & ex b₃ being Nat st b₁ = 2 * b₃ holds
ex b₃ being Subgroup of b₂ st
( ord b₃ = 2 & b₃ is cyclic Group )

proof end;

theorem Th32: :: GR_CY_2:32

for b₁ being Group
for b₂ being strict Group
for b₃ being Homomorphism of b₂,b₁ st b₂ is cyclic Group holds
Image b₃ is cyclic Group

proof end;

theorem Th33: :: GR_CY_2:33

for b₁, b₂ being strict Group st b₁,b₂ are_isomorphic & ( b₁ is cyclic Group or b₂ is cyclic Group ) holds
( b₁ is cyclic Group & b₂ is cyclic Group )

proof end;