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


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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

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))
proof end;

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
proof end;

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
proof end;

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

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 & a in A ) )
proof end;

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)
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
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 )
proof end;
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 ) ) & ( 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
proof end;
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 x, z 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 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 B, A being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
proof end;

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

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 & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
proof end;

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
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} 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
for H being strict Subgroup of G holds H is cyclic Group
proof end;