:: GROUP_8 semantic presentation

theorem :: GROUP_8:1

for G being strict Group
for p being Nat st p is prime & ord G = p & G is finite holds
ex a being Element of G st ord a = p

proof end;

theorem Th2: :: GROUP_8:2

for G being strict Group
for H being strict Subgroup of G
for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2

proof end;

theorem Th3: :: GROUP_8:3

for G being strict Group
for H being strict Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for n being Nat holds a |^ n = b |^ n

proof end;

theorem Th4: :: GROUP_8:4

for G being strict Group
for H being strict Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for i being Integer holds a |^ i = b |^ i

proof end;

theorem :: GROUP_8:5

for G being strict Group
for H being strict Subgroup of G
for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b

proof end;

theorem :: GROUP_8:6

for G being strict Group
for H being strict Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H

proof end;

theorem Th7: :: GROUP_8:7

for G being strict Group
for a being Element of G st a <> 1. G holds
gr {a} <> (1). G

proof end;

theorem Th8: :: GROUP_8:8

for G being strict Group
for m being Integer holds (1. G) |^ m = 1. G

proof end;

theorem Th9: :: GROUP_8:9

for G being strict Group
for a being Element of G
for m being Integer holds a |^ (m * (ord a)) = 1. G

proof end;

theorem Th10: :: GROUP_8:10

for G being strict Group
for a being Element of G st a is_not_of_order_0 holds
for m being Integer holds a |^ m = a |^ (m mod (ord a))

proof end;

theorem Th11: :: GROUP_8:11

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

proof end;

theorem Th12: :: GROUP_8:12

for G being strict Group
for b being Element of G st b is_of_order_0 holds
b " is_of_order_0

proof end;

theorem Th13: :: GROUP_8:13

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

proof end;

theorem :: GROUP_8:14

for G being strict Group st ex a being Element of G st a <> 1. G holds
( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) iff ( G is cyclic Group & G is finite & ex p being Nat st
( ord G = p & p is prime ) ) )

proof end;

theorem Th15: :: GROUP_8:15

for G being strict Group
for x, y, z being Element of G
for A being Subset of G holds
( z in (x * A) * y iff ex a being Element of G st
( z = (x * a) * y & a in A ) )

proof end;

theorem :: GROUP_8:16

for G being strict Group
for A being non empty Subset of G
for x being Element of G holds Card A = Card (((x " ) * A) * x)

proof end;

definition

let G be strict Group;
let H, K be strict Subgroup of G;
func Double_Cosets H,K -> Subset-Family of G means :: GROUP_8:def 1
for A being Subset of G holds
( A in it iff ex a being Element of G st A = (H * a) * K );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Double_Cosets GROUP_8:def 1 :

theorem Th17: :: GROUP_8:17

for G being strict Group
for z, x being Element of G
for H, K being strict Subgroup of G holds
( z in (H * x) * K iff ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) )

proof end;

theorem :: GROUP_8:18

for G being strict Group
for x, y being Element of G
for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )

proof end;

registration

let G be strict Group;
let A be strict Subgroup of G;
cluster Left_Cosets A -> non empty ;
coherence by GROUP_2:165;

end;

notation

let G be strict Group;
let H be Subgroup of G;
synonym index G,H for index H;

end;

theorem Th19: :: GROUP_8:19

for G being strict Group
for A, B being strict Subgroup of G
for D being strict Subgroup of A st G = A "\/" B & D = A /\ B & G is finite holds
index G,B >= index A,D

proof end;

theorem Th20: :: GROUP_8:20

for G being strict Group
for H being strict Subgroup of G st G is finite holds
index G,H > 0

proof end;

theorem :: GROUP_8:21

for G being strict Group st G is finite holds
for C being strict Subgroup of G
for A, B being strict Subgroup of C st C = A "\/" B holds
for D being strict Subgroup of A st D = A /\ B holds
for E being strict Subgroup of B st E = A /\ B holds
for F being strict Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )

proof end;

theorem Th22: :: GROUP_8:22

for G being strict Group
for H being strict Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H

proof end;

theorem Th23: :: GROUP_8:23

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

proof end;

theorem Th24: :: GROUP_8:24

for G being strict Group
for a being Element of G st G = gr {a} & G <> (1). G holds
for H being strict Subgroup of G st H <> (1). G holds
ex k being Nat st
( 0 < k & a |^ k in H )

proof end;

theorem :: GROUP_8:25

for G being strict cyclic Group st G <> (1). G holds
for H being strict Subgroup of G st H <> (1). G holds
H is cyclic Group

proof end;