:: GROUP_8 semantic presentation

theorem Th1: :: GROUP_8:1

for b₁ being strict Group
for b₂ being Nat st b₂ is prime & ord b₁ = b₂ & b₁ is finite holds
ex b₃ being Element of b₁ st ord b₃ = b₂

proof end;

theorem Th2: :: GROUP_8:2

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
b₃ * b₄ = b₅ * b₆

proof end;

theorem Th3: :: GROUP_8:3

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₂
for b₄ being Element of b₁ st b₃ = b₄ holds
for b₅ being Nat holds b₃ |^ b₅ = b₄ |^ b₅

proof end;

theorem Th4: :: GROUP_8:4

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₂
for b₄ being Element of b₁ st b₃ = b₄ holds
for b₅ being Integer holds b₃ |^ b₅ = b₄ |^ b₅

proof end;

theorem Th5: :: GROUP_8:5

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₂
for b₄ being Element of b₁ st b₃ = b₄ & b₁ is finite holds
ord b₃ = ord b₄

proof end;

theorem Th6: :: GROUP_8:6

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
b₂ * b₃ c= the carrier of b₂

proof end;

theorem Th7: :: GROUP_8:7

for b₁ being strict Group
for b₂ being Element of b₁ st b₂ <> 1. b₁ holds
gr {b₂} <> (1). b₁

proof end;

theorem Th8: :: GROUP_8:8

for b₁ being strict Group
for b₂ being Integer holds (1. b₁) |^ b₂ = 1. b₁

proof end;

theorem Th9: :: GROUP_8:9

for b₁ being strict Group
for b₂ being Element of b₁
for b₃ being Integer holds b₂ |^ (b₃ * (ord b₂)) = 1. b₁

proof end;

theorem Th10: :: GROUP_8:10

for b₁ being strict Group
for b₂ being Element of b₁ st b₂ is_not_of_order_0 holds
for b₃ being Integer holds b₂ |^ b₃ = b₂ |^ (b₃ mod (ord b₂))

proof end;

theorem Th11: :: GROUP_8:11

for b₁ being strict Group
for b₂ being Element of b₁ st b₂ is_not_of_order_0 holds
gr {b₂} is finite

proof end;

theorem Th12: :: GROUP_8:12

for b₁ being strict Group
for b₂ being Element of b₁ st b₂ is_of_order_0 holds
b₂ " is_of_order_0

proof end;

theorem Th13: :: GROUP_8:13

for b₁ being strict Group
for b₂ being Element of b₁ holds
( b₂ is_of_order_0 iff for b₃ being Integer st b₂ |^ b₃ = 1. b₁ holds
b₃ = 0 )

proof end;

theorem Th14: :: GROUP_8:14

for b₁ being strict Group st ex b₂ being Element of b₁ st b₂ <> 1. b₁ holds
( ( for b₂ being strict Subgroup of b₁ holds
( b₂ = b₁ or b₂ = (1). b₁ ) ) iff ( b₁ is cyclic Group & b₁ is finite & ex b₂ being Nat st
( ord b₁ = b₂ & b₂ is prime ) ) )

proof end;

theorem Th15: :: GROUP_8:15

for b₁ being strict Group
for b₂, b₃, b₄ being Element of b₁
for b₅ being Subset of b₁ holds
( b₄ in (b₂ * b₅) * b₃ iff ex b₆ being Element of b₁ st
( b₄ = (b₂ * b₆) * b₃ & b₆ in b₅ ) )

proof end;

theorem Th16: :: GROUP_8:16

for b₁ being strict Group
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁ holds Card b₂ = Card (((b₃ " ) * b₂) * b₃)

proof end;

definition

let c₁ be strict Group;
let c₂, c₃ be strict Subgroup of c₁;
func Double_Cosets c₂,c₃ -> Subset-Family of a₁ means :: GROUP_8:def 1
for b₁ being Subset of a₁ holds
( b₁ in a₄ iff ex b₂ being Element of a₁ st b₁ = (a₂ * b₂) * a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Double_Cosets GROUP_8:def 1 :

theorem Th17: :: GROUP_8:17

for b₁ being strict Group
for b₂, b₃ being Element of b₁
for b₄, b₅ being strict Subgroup of b₁ holds
( b₂ in (b₄ * b₃) * b₅ iff ex b₆, b₇ being Element of b₁ st
( b₂ = (b₆ * b₃) * b₇ & b₆ in b₄ & b₇ in b₅ ) )

proof end;

theorem Th18: :: GROUP_8:18

for b₁ being strict Group
for b₂, b₃ being Element of b₁
for b₄, b₅ being strict Subgroup of b₁ holds
( (b₄ * b₂) * b₅ = (b₄ * b₃) * b₅ or for b₆ being Element of b₁ holds
( not b₆ in (b₄ * b₂) * b₅ or not b₆ in (b₄ * b₃) * b₅ ) )

proof end;

registration

let c₁ be strict Group;
let c₂ be strict Subgroup of c₁;
cluster Left_Cosets a₂ -> non empty ;
coherence by GROUP_2:165;

end;

notation

let c₁ be strict Group;
let c₂ be Subgroup of c₁;
synonym index c₁,c₂ for index c₂;

end;

theorem Th19: :: GROUP_8:19

for b₁ being strict Group
for b₂, b₃ being strict Subgroup of b₁
for b₄ being strict Subgroup of b₂ st b₁ = b₂ "\/" b₃ & b₄ = b₂ /\ b₃ & b₁ is finite holds
index b₁,b₃ >= index b₂,b₄

proof end;

theorem Th20: :: GROUP_8:20

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ st b₁ is finite holds
index b₁,b₂ > 0

proof end;

theorem Th21: :: GROUP_8:21

for b₁ being strict Group st b₁ is finite holds
for b₂ being strict Subgroup of b₁
for b₃, b₄ being strict Subgroup of b₂ st b₂ = b₃ "\/" b₄ holds
for b₅ being strict Subgroup of b₃ st b₅ = b₃ /\ b₄ holds
for b₆ being strict Subgroup of b₄ st b₆ = b₃ /\ b₄ holds
for b₇ being strict Subgroup of b₂ st b₇ = b₃ /\ b₄ & Left_Cosets b₄ is finite & Left_Cosets b₃ is finite & index b₂,b₃, index b₂,b₄ are_relative_prime holds
( index b₂,b₄ = index b₃,b₅ & index b₂,b₃ = index b₄,b₆ )

proof end;

theorem Th22: :: GROUP_8:22

for b₁ being strict Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
for b₄ being Integer holds b₃ |^ b₄ in b₂

proof end;

theorem Th23: :: GROUP_8:23

for b₁ being strict Group st b₁ <> (1). b₁ holds
ex b₂ being Element of b₁ st b₂ <> 1. b₁

proof end;

theorem Th24: :: GROUP_8:24

for b₁ being strict Group
for b₂ being Element of b₁ st b₁ = gr {b₂} & b₁ <> (1). b₁ holds
for b₃ being strict Subgroup of b₁ st b₃ <> (1). b₁ holds
ex b₄ being Nat st
( 0 < b₄ & b₂ |^ b₄ in b₃ )

proof end;

theorem Th25: :: GROUP_8:25

for b₁ being strict cyclic Group st b₁ <> (1). b₁ holds
for b₂ being strict Subgroup of b₁ st b₂ <> (1). b₁ holds
b₂ is cyclic Group

proof end;