:: 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

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

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

theorem :: GROUP_8:4

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

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

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

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

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

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

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 )

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

( ( 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 ) )

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)

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;

ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = (H * a) * K )

for b_{1}, b_{2} being Subset-Family of G st ( for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds

( A in b_{2} iff ex a being Element of G st A = (H * a) * K ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of G holds

( A in it iff ex a being Element of G st A = (H * a) * K );

ex b

for A being Subset of G holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem defines Double_Cosets GROUP_8:def 1 :

for G being strict Group

for H, K being strict Subgroup of G

for b_{4} being Subset-Family of G holds

( b_{4} = Double_Cosets (H,K) iff for A being Subset of G holds

( A in b_{4} iff ex a being Element of G st A = (H * a) * K ) );

for G being strict Group

for H, K being strict Subgroup of G

for b

( b

( A in b

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

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

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

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 :: 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) )

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

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

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;