:: Properties of Groups
:: by Gijs Geleijnse and Grzegorz Bancerek
::
:: Received May 31, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem :: GROUP_8:1
for p being Element of NAT
for G being finite strict Group st p is prime & card G = p holds
ex a being Element of G st ord a = p
proofend;

theorem :: GROUP_8:2
for G being Group
for H being 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
proofend;

theorem :: GROUP_8:3
for G being Group
for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for n being Element of NAT holds a |^ n = b |^ n by GROUP_4:1;

theorem :: GROUP_8:4
for G being Group
for H being 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 by GROUP_4:2;

theorem :: GROUP_8:5
for G being Group
for H being 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
proofend;

theorem :: GROUP_8:6
for G being Group
for H being Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H
proofend;

theorem Th7: :: GROUP_8:7
for G being Group
for a being Element of G st a <> 1_ G holds
gr {a} <> (1). G
proofend;

theorem :: GROUP_8:8
for G being Group
for m being Integer holds (1_ G) |^ m = 1_ G by GROUP_1:31;

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
proofend;

theorem Th10: :: GROUP_8:10
for G being strict Group
for a being Element of G st not a is being_of_order_0 holds
for m being Integer holds a |^ m = a |^ (m mod (ord a))
proofend;

theorem Th11: :: GROUP_8:11
for G being strict Group
for b being Element of G st not b is being_of_order_0 holds
gr {b} is finite
proofend;

theorem Th12: :: GROUP_8:12
for G being strict Group
for b being Element of G st b is being_of_order_0 holds
b " is being_of_order_0
proofend;

theorem Th13: :: GROUP_8:13
for G being strict Group
for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
proofend;

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 &amp; G is finite &amp; ex p being Element of NAT st
( card G = p &amp; p is prime ) ) )
proofend;

theorem Th15: :: GROUP_8:15
for G being 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 &amp; a in A ) )
proofend;

theorem :: GROUP_8:16
for G being Group
for A being non empty Subset of G
for x being Element of G holds card A = card (((x ") * A) * x)
proofend;

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
 ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = (H * a) * K )
proofend;
uniqueness
 for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = (H * a) * K ) ) &amp; ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = (H * a) * K ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Double_Cosets GROUP_8:def_1_:_
 for G being strict Group
for H, K being strict Subgroup of G
for b4 being Subset-Family of G holds
( b4 = Double_Cosets (H,K) iff for A being Subset of G holds
( A in b4 iff ex a being Element of G st A = (H * a) * K ) );

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 &amp; g in H &amp; h in K ) )
proofend;

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 ) )
proofend;

registration
let G be Group;
let A be Subgroup of G;
cluster Left_Cosets A ->  non empty ;
coherence
 not Left_Cosets A is empty by GROUP_2:135;
end;

notation
let G be Group;
let H be Subgroup of G;
synonym  index (G,H) for  index H;
end;

theorem Th19: :: GROUP_8:19
for G being Group
for A, B being Subgroup of G
for D being Subgroup of A st D = A /\ B &amp; G is finite holds
index (G,B) >= index (A,D)
proofend;

theorem Th20: :: GROUP_8:20
for G being finite Group
for H being Subgroup of G holds index (G,H) > 0
proofend;

theorem :: GROUP_8:21
for G being Group st G is finite holds
for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B &amp; index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) &amp; index (C,A) = index (B,E) )
proofend;

theorem Th22: :: GROUP_8:22
for G being Group
for H being Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
proofend;

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
proofend;

theorem Th24: :: GROUP_8:24
for G being strict Group
for a being Element of G st G = gr {a} holds
for H being strict Subgroup of G st H <> (1). G holds
ex k being Element of NAT st
( 0 < k &amp; a |^ k in H )
proofend;

theorem :: GROUP_8:25
for G being strict cyclic Group
for H being strict Subgroup of G holds H is cyclic Group
proofend;