:: 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 b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = (H * a) * K )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of G st ( for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds
( A in b₂ iff ex a being Element of G st A = (H * a) * K ) ) holds
b₁ = b₂

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 b₄ being Subset-Family of G holds
( b₄ = Double_Cosets (H,K) iff for A being Subset of G holds
( A in b₄ 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;