:: The Sylow Theorems
:: by Marco Riccardi
::
:: Received August 13, 2007
:: Copyright (c) 2007 Association of Mizar Users

begin

notation

let S be non empty 1-sorted ;
let E be set ;
let A be Action of the carrier of S,E;
let s be Element of ;
synonym A ^ s for S . E;

end;

definition

let S be non empty 1-sorted ;
let E be set ;
let A be Action of the carrier of S,E;
let s be Element of ;
:: original: ^
redefine func A ^ s -> Function of E,E;
correctness
coherence
^ is Function of E,E;

proof end;

end;

definition

let S be non empty unital multMagma ;
let E be set ;
let A be Action of the carrier of S,E;
attr A is being_left_operation means :Def1: :: GROUP_10:def 1
( A ^ (1_ S) = id E & ( for s1, s2 being Element of holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) );

end;

:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :

for S being non empty unital multMagma
for E being set
for A being Action of the carrier of S,E holds
( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

registration

let S be non empty unital multMagma ;
let E be set ;
cluster being_left_operation Element of bool [:the carrier of S,(Funcs E,E):];
correctness
existence
ex b₁ being Action of the carrier of S,E st b₁ is being_left_operation ;

proof end;

end;

definition

let S be non empty unital multMagma ;
let E be set ;
mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;

end;

scheme :: GROUP_10:sch 1
ExLeftOperation{ F₁() -> set , F₂() -> non empty Group-like multMagma , F₃( Element of ) -> Function of F₁(),F₁() } :

ex T being LeftOperation of F₂(),F₁() st
for s being Element of holds T . s = F₃(s)

provided

A1: F₃((1_ F₂())) = id F₁() and
A2: for s1, s2 being Element of holds F₃((s1 * s2)) = F₃(s1) * F₃(s2)

proof end;

theorem Th1: :: GROUP_10:1

for E being non empty set
for S being non empty Group-like multMagma
for s being Element of
for LO being LeftOperation of S,E holds LO ^ s is one-to-one

proof end;

notation

let S be non empty multMagma ;
let s be Element of ;
synonym the_left_translation_of s for s * ;

end;

definition

let S be non empty Group-like associative multMagma ;
func the_left_operation_of S -> LeftOperation of S,the carrier of S means :Def2: :: GROUP_10:def 2
for s being Element of holds it . s = the_left_translation_of s;
existence
ex b₁ being LeftOperation of S,the carrier of S st
for s being Element of holds b₁ . s = the_left_translation_of s

proof end;

uniqueness
for b₁, b₂ being LeftOperation of S,the carrier of S st ( for s being Element of holds b₁ . s = the_left_translation_of s ) & ( for s being Element of holds b₂ . s = the_left_translation_of s ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines the_left_operation_of GROUP_10:def 2 :

for S being non empty Group-like associative multMagma
for b₂ being LeftOperation of S,the carrier of S holds
( b₂ = the_left_operation_of S iff for s being Element of holds b₂ . s = the_left_translation_of s );

definition

let E, n be set ;
func the_subsets_of_card n,E -> Subset-Family of equals :: GROUP_10:def 3
{ X where X is Subset of : card X = n } ;
correctness
coherence
{ X where X is Subset of : card X = n } is Subset-Family of ;

proof end;

end;

:: deftheorem defines the_subsets_of_card GROUP_10:def 3 :

for E, n being set holds the_subsets_of_card n,E = { X where X is Subset of : card X = n } ;

registration

let E be finite set ;
let n be set ;
cluster the_subsets_of_card n,E -> finite ;
correctness
coherence
the_subsets_of_card n,E is finite ;
;

end;

theorem Th2: :: GROUP_10:2

for n being natural number
for E being non empty set st card n c= card E holds
not the_subsets_of_card n,E is empty

proof end;

theorem Th3: :: GROUP_10:3

for E being non empty finite set
for k being Element of NAT
for x1, x2 being set st x1 <> x2 holds
card (Choose E,k,x1,x2) = card (the_subsets_of_card k,E)

proof end;

definition

let E be non empty set ;
let n be natural number ;
let S be non empty Group-like multMagma ;
let s be Element of ;
let LO be LeftOperation of S,E;
assume A1: card n c= card E ;
func the_extension_of_left_translation_of n,s,LO -> Function of the_subsets_of_card n,E, the_subsets_of_card n,E means :Def4: :: GROUP_10:def 4
for X being Element of the_subsets_of_card n,E holds it . X = (LO ^ s) .: X;
existence
ex b₁ being Function of the_subsets_of_card n,E, the_subsets_of_card n,E st
for X being Element of the_subsets_of_card n,E holds b₁ . X = (LO ^ s) .: X

proof end;

uniqueness
for b₁, b₂ being Function of the_subsets_of_card n,E, the_subsets_of_card n,E st ( for X being Element of the_subsets_of_card n,E holds b₁ . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card n,E holds b₂ . X = (LO ^ s) .: X ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines the_extension_of_left_translation_of GROUP_10:def 4 :

for E being non empty set
for n being natural number
for S being non empty Group-like multMagma
for s being Element of
for LO being LeftOperation of S,E st card n c= card E holds
for b₆ being Function of the_subsets_of_card n,E, the_subsets_of_card n,E holds
( b₆ = the_extension_of_left_translation_of n,s,LO iff for X being Element of the_subsets_of_card n,E holds b₆ . X = (LO ^ s) .: X );

definition

let E be non empty set ;
let n be natural number ;
let S be non empty Group-like multMagma ;
let LO be LeftOperation of S,E;
assume A1: card n c= card E ;
func the_extension_of_left_operation_of n,LO -> LeftOperation of S,(the_subsets_of_card n,E) means :Def5: :: GROUP_10:def 5
for s being Element of holds it . s = the_extension_of_left_translation_of n,s,LO;
existence
ex b₁ being LeftOperation of S,(the_subsets_of_card n,E) st
for s being Element of holds b₁ . s = the_extension_of_left_translation_of n,s,LO

proof end;

uniqueness
for b₁, b₂ being LeftOperation of S,(the_subsets_of_card n,E) st ( for s being Element of holds b₁ . s = the_extension_of_left_translation_of n,s,LO ) & ( for s being Element of holds b₂ . s = the_extension_of_left_translation_of n,s,LO ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines the_extension_of_left_operation_of GROUP_10:def 5 :

for E being non empty set
for n being natural number
for S being non empty Group-like multMagma
for LO being LeftOperation of S,E st card n c= card E holds
for b₅ being LeftOperation of S,(the_subsets_of_card n,E) holds
( b₅ = the_extension_of_left_operation_of n,LO iff for s being Element of holds b₅ . s = the_extension_of_left_translation_of n,s,LO );

definition

let S be non empty multMagma ;
let s be Element of ;
let Z be non empty set ;
func the_left_translation_of s,Z -> Function of [:the carrier of S,Z:],[:the carrier of S,Z:] means :Def6: :: GROUP_10:def 6
for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of ex z being Element of Z st
( z2 = it . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] );
existence
ex b₁ being Function of [:the carrier of S,Z:],[:the carrier of S,Z:] st
for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of ex z being Element of Z st
( z2 = b₁ . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )

proof end;

uniqueness
for b₁, b₂ being Function of [:the carrier of S,Z:],[:the carrier of S,Z:] st ( for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of ex z being Element of Z st
( z2 = b₁ . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) & ( for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of ex z being Element of Z st
( z2 = b₂ . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines the_left_translation_of GROUP_10:def 6 :

for S being non empty multMagma
for s being Element of
for Z being non empty set
for b₄ being Function of [:the carrier of S,Z:],[:the carrier of S,Z:] holds
( b₄ = the_left_translation_of s,Z iff for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of ex z being Element of Z st
( z2 = b₄ . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) );

definition

let S be non empty Group-like associative multMagma ;
let Z be non empty set ;
func the_left_operation_of S,Z -> LeftOperation of S,[:the carrier of S,Z:] means :Def7: :: GROUP_10:def 7
for s being Element of holds it . s = the_left_translation_of s,Z;
existence
ex b₁ being LeftOperation of S,[:the carrier of S,Z:] st
for s being Element of holds b₁ . s = the_left_translation_of s,Z

proof end;

uniqueness
for b₁, b₂ being LeftOperation of S,[:the carrier of S,Z:] st ( for s being Element of holds b₁ . s = the_left_translation_of s,Z ) & ( for s being Element of holds b₂ . s = the_left_translation_of s,Z ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines the_left_operation_of GROUP_10:def 7 :

for S being non empty Group-like associative multMagma
for Z being non empty set
for b₃ being LeftOperation of S,[:the carrier of S,Z:] holds
( b₃ = the_left_operation_of S,Z iff for s being Element of holds b₃ . s = the_left_translation_of s,Z );

definition

let G be Group;
let H, P be Subgroup of G;
let h be Element of ;
func the_left_translation_of h,P -> Function of Left_Cosets P, Left_Cosets P means :Def8: :: GROUP_10:def 8
for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = it . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h );
existence
ex b₁ being Function of Left_Cosets P, Left_Cosets P st
for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = b₁ . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )

proof end;

uniqueness
for b₁, b₂ being Function of Left_Cosets P, Left_Cosets P st ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = b₁ . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) & ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = b₂ . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines the_left_translation_of GROUP_10:def 8 :

for G being Group
for H, P being Subgroup of G
for h being Element of
for b₅ being Function of Left_Cosets P, Left_Cosets P holds
( b₅ = the_left_translation_of h,P iff for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = b₅ . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) );

definition

let G be Group;
let H, P be Subgroup of G;
func the_left_operation_of H,P -> LeftOperation of H,(Left_Cosets P) means :Def9: :: GROUP_10:def 9
for h being Element of holds it . h = the_left_translation_of h,P;
existence
ex b₁ being LeftOperation of H,(Left_Cosets P) st
for h being Element of holds b₁ . h = the_left_translation_of h,P

proof end;

uniqueness
for b₁, b₂ being LeftOperation of H,(Left_Cosets P) st ( for h being Element of holds b₁ . h = the_left_translation_of h,P ) & ( for h being Element of holds b₂ . h = the_left_translation_of h,P ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines the_left_operation_of GROUP_10:def 9 :

for G being Group
for H, P being Subgroup of G
for b₄ being LeftOperation of H,(Left_Cosets P) holds
( b₄ = the_left_operation_of H,P iff for h being Element of holds b₄ . h = the_left_translation_of h,P );

begin

definition

let G be Group;
let E be non empty set ;
let T be LeftOperation of G,E;
let A be Subset of ;
func the_strict_stabilizer_of A,T -> strict Subgroup of G means :Def10: :: GROUP_10:def 10
the carrier of it = { g where g is Element of : (T ^ g) .: A = A } ;
existence
ex b₁ being strict Subgroup of G st the carrier of b₁ = { g where g is Element of : (T ^ g) .: A = A }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = { g where g is Element of : (T ^ g) .: A = A } & the carrier of b₂ = { g where g is Element of : (T ^ g) .: A = A } holds
b₁ = b₂ by GROUP_2:68;

end;

:: deftheorem Def10 defines the_strict_stabilizer_of GROUP_10:def 10 :

for G being Group
for E being non empty set
for T being LeftOperation of G,E
for A being Subset of
for b₅ being strict Subgroup of G holds
( b₅ = the_strict_stabilizer_of A,T iff the carrier of b₅ = { g where g is Element of : (T ^ g) .: A = A } );

definition

let G be Group;
let E be non empty set ;
let T be LeftOperation of G,E;
let x be Element of E;
func the_strict_stabilizer_of x,T -> strict Subgroup of G equals :: GROUP_10:def 11
the_strict_stabilizer_of {x},T;
correctness
coherence
the_strict_stabilizer_of {x},T is strict Subgroup of G;
;

end;

:: deftheorem defines the_strict_stabilizer_of GROUP_10:def 11 :

for G being Group
for E being non empty set
for T being LeftOperation of G,E
for x being Element of E holds the_strict_stabilizer_of x,T = the_strict_stabilizer_of {x},T;

definition

let S be non empty unital multMagma ;
let E be set ;
let T be LeftOperation of S,E;
let x be Element of E;
pred x is_fixed_under T means :Def12: :: GROUP_10:def 12
for s being Element of holds x = (T ^ s) . x;

end;

:: deftheorem Def12 defines is_fixed_under GROUP_10:def 12 :

for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E
for x being Element of E holds
( x is_fixed_under T iff for s being Element of holds x = (T ^ s) . x );

definition

let S be non empty unital multMagma ;
let E be set ;
let T be LeftOperation of S,E;
func the_fixed_points_of T -> Subset of equals :Def13: :: GROUP_10:def 13
{ x where x is Element of E : x is_fixed_under T } if not E is empty
otherwise {} E;
correctness
coherence
( ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of ) & ( E is empty implies {} E is Subset of ) );
consistency
for b₁ being Subset of holds verum;

proof end;

end;

:: deftheorem Def13 defines the_fixed_points_of GROUP_10:def 13 :

for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E holds
( ( not E is empty implies the_fixed_points_of T = { x where x is Element of E : x is_fixed_under T } ) & ( E is empty implies the_fixed_points_of T = {} E ) );

definition

let S be non empty unital multMagma ;
let E be set ;
let T be LeftOperation of S,E;
let x, y be Element of E;
pred x,y are_conjugated_under T means :Def14: :: GROUP_10:def 14
ex s being Element of st y = (T ^ s) . x;

end;

:: deftheorem Def14 defines are_conjugated_under GROUP_10:def 14 :

for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E
for x, y being Element of E holds
( x,y are_conjugated_under T iff ex s being Element of st y = (T ^ s) . x );

theorem Th4: :: GROUP_10:4

for S being non empty unital multMagma
for E being non empty set
for x being Element of E
for T being LeftOperation of S,E holds x,x are_conjugated_under T

proof end;

theorem Th5: :: GROUP_10:5

for G being Group
for E being non empty set
for x, y being Element of E
for T being LeftOperation of G,E st x,y are_conjugated_under T holds
y,x are_conjugated_under T

proof end;

theorem Th6: :: GROUP_10:6

for S being non empty unital multMagma
for E being non empty set
for x, y, z being Element of E
for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds
x,z are_conjugated_under T

proof end;

definition

let S be non empty unital multMagma ;
let E be non empty set ;
let T be LeftOperation of S,E;
let x be Element of E;
func the_orbit_of x,T -> Subset of equals :: GROUP_10:def 15
{ y where y is Element of E : x,y are_conjugated_under T } ;
correctness
coherence
{ y where y is Element of E : x,y are_conjugated_under T } is Subset of ;

proof end;

end;

:: deftheorem defines the_orbit_of GROUP_10:def 15 :

for S being non empty unital multMagma
for E being non empty set
for T being LeftOperation of S,E
for x being Element of E holds the_orbit_of x,T = { y where y is Element of E : x,y are_conjugated_under T } ;

theorem Th7: :: GROUP_10:7

for S being non empty unital multMagma
for E being non empty set
for x being Element of E
for T being LeftOperation of S,E holds not the_orbit_of x,T is empty

proof end;

theorem Th8: :: GROUP_10:8

for G being Group
for E being non empty set
for x, y being Element of E
for T being LeftOperation of G,E holds
( the_orbit_of x,T misses the_orbit_of y,T or the_orbit_of x,T = the_orbit_of y,T )

proof end;

theorem Th9: :: GROUP_10:9

for S being non empty unital multMagma
for E being non empty finite set
for x being Element of E
for T being LeftOperation of S,E st x is_fixed_under T holds
the_orbit_of x,T = {x}

proof end;

theorem Th10: :: GROUP_10:10

for G being Group
for E being non empty set
for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)

proof end;

definition

let G be Group;
let E be non empty set ;
let T be LeftOperation of G,E;
func the_orbits_of T -> a_partition of E equals :: GROUP_10:def 16
{ X where X is Subset of : ex x being Element of E st X = the_orbit_of x,T } ;
correctness
coherence
{ X where X is Subset of : ex x being Element of E st X = the_orbit_of x,T } is a_partition of E;

proof end;

end;

:: deftheorem defines the_orbits_of GROUP_10:def 16 :

for G being Group
for E being non empty set
for T being LeftOperation of G,E holds the_orbits_of T = { X where X is Subset of : ex x being Element of E st X = the_orbit_of x,T } ;

begin

definition

let p be natural prime number ;
let G be Group;
pred G is_p-group_of_prime p means :Def17: :: GROUP_10:def 17
ex r being natural number st card G = p |^ r;

end;

:: deftheorem Def17 defines is_p-group_of_prime GROUP_10:def 17 :

for p being natural prime number
for G being Group holds
( G is_p-group_of_prime p iff ex r being natural number st card G = p |^ r );

definition

let p be natural prime number ;
let G be Group;
let P be Subgroup of G;
pred P is_p-group_of_prime p means :Def18: :: GROUP_10:def 18
ex H being finite Group st
( P = H & H is_p-group_of_prime p );

end;

:: deftheorem Def18 defines is_p-group_of_prime GROUP_10:def 18 :

for p being natural prime number
for G being Group
for P being Subgroup of G holds
( P is_p-group_of_prime p iff ex H being finite Group st
( P = H & H is_p-group_of_prime p ) );

theorem Th11: :: GROUP_10:11

for E being non empty finite set
for G being finite Group
for p being natural prime number
for T being LeftOperation of G,E st G is_p-group_of_prime p holds
(card (the_fixed_points_of T)) mod p = (card E) mod p

proof end;

begin

definition

let p be natural prime number ;
let G be Group;
let P be Subgroup of G;
pred P is_Sylow_p-subgroup_of_prime p means :Def19: :: GROUP_10:def 19
( P is_p-group_of_prime p & not p divides index P );

end;

:: deftheorem Def19 defines is_Sylow_p-subgroup_of_prime GROUP_10:def 19 :

for p being natural prime number
for G being Group
for P being Subgroup of G holds
( P is_Sylow_p-subgroup_of_prime p iff ( P is_p-group_of_prime p & not p divides index P ) );

Lm1: for n being natural number
for p being natural prime number st n <> 0 holds
ex m, r being natural number st
( n = (p |^ r) * m & not p divides m )

proof end;

Lm2: for n being natural number st n > 0 holds
card (INT.Group n) = n

proof end;

Lm3: for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y

proof end;

Lm4: for G being finite Group
for E, T being non empty set
for LO being LeftOperation of G,E
for n being natural number st LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }

proof end;

Lm5: for n, m, r being natural number
for p being natural prime number st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0

proof end;

Lm6: for r, n, m1, m2 being natural number
for p being natural prime number st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ r divides m1

proof end;

Lm7: for G being Group
for A being non empty Subset of
for x being Element of holds card A = card (A * x)

proof end;

theorem Th12: :: GROUP_10:12

for G being finite Group
for p being natural prime number ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p

proof end;

Lm8: for n, r being natural number
for p being natural prime number st n divides p |^ r & n > 1 holds
p divides n

proof end;

theorem :: GROUP_10:13

for G being finite Group
for p being natural prime number st p divides card G holds
ex g being Element of st ord g = p

proof end;

theorem Th14: :: GROUP_10:14

for G being finite Group
for p being natural prime number holds
( ( for H being Subgroup of G st H is_p-group_of_prime p holds
ex P being Subgroup of G st
( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) & ( for P1, P2 being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p holds
P1,P2 are_conjugated ) )

proof end;

definition

let G be Group;
let p be natural prime number ;
func the_sylow_p-subgroups_of_prime p,G -> Subset of equals :: GROUP_10:def 20
{ H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;
correctness
coherence
{ H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } is Subset of ;

proof end;

end;

:: deftheorem defines the_sylow_p-subgroups_of_prime GROUP_10:def 20 :

for G being Group
for p being natural prime number holds the_sylow_p-subgroups_of_prime p,G = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

registration

let G be finite Group;
let p be natural prime number ;
cluster the_sylow_p-subgroups_of_prime p,G -> non empty finite ;
correctness
coherence
( not the_sylow_p-subgroups_of_prime p,G is empty & the_sylow_p-subgroups_of_prime p,G is finite );

proof end;

end;

definition

let G be finite Group;
let p be natural prime number ;
let H be Subgroup of G;
let h be Element of ;
func the_left_translation_of h,p -> Function of the_sylow_p-subgroups_of_prime p,G, the_sylow_p-subgroups_of_prime p,G means :Def21: :: GROUP_10:def 21
for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of st
( P2 = it . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g );
existence
ex b₁ being Function of the_sylow_p-subgroups_of_prime p,G, the_sylow_p-subgroups_of_prime p,G st
for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of st
( P2 = b₁ . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )

proof end;

uniqueness
for b₁, b₂ being Function of the_sylow_p-subgroups_of_prime p,G, the_sylow_p-subgroups_of_prime p,G st ( for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of st
( P2 = b₁ . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of st
( P2 = b₂ . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines the_left_translation_of GROUP_10:def 21 :

for G being finite Group
for p being natural prime number
for H being Subgroup of G
for h being Element of
for b₅ being Function of the_sylow_p-subgroups_of_prime p,G, the_sylow_p-subgroups_of_prime p,G holds
( b₅ = the_left_translation_of h,p iff for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of st
( P2 = b₅ . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) );

definition

let G be finite Group;
let p be natural prime number ;
let H be Subgroup of G;
func the_left_operation_of H,p -> LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) means :Def22: :: GROUP_10:def 22
for h being Element of holds it . h = the_left_translation_of h,p;
existence
ex b₁ being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of holds b₁ . h = the_left_translation_of h,p

proof end;

uniqueness
for b₁, b₂ being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st ( for h being Element of holds b₁ . h = the_left_translation_of h,p ) & ( for h being Element of holds b₂ . h = the_left_translation_of h,p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines the_left_operation_of GROUP_10:def 22 :

for G being finite Group
for p being natural prime number
for H being Subgroup of G
for b₄ being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) holds
( b₄ = the_left_operation_of H,p iff for h being Element of holds b₄ . h = the_left_translation_of h,p );

Lm9: for G, H being finite Group
for p being natural prime number
for I being Subgroup of G
for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p

proof end;

theorem :: GROUP_10:15

for G being finite Group
for p being natural prime number holds
( (card (the_sylow_p-subgroups_of_prime p,G)) mod p = 1 & card (the_sylow_p-subgroups_of_prime p,G) divides card G )

proof end;

begin

theorem :: GROUP_10:16

for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y by Lm3;

theorem :: GROUP_10:17

for n, m, r being natural number
for p being natural prime number st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0 by Lm5;

theorem :: GROUP_10:18

for n being non zero natural number holds card (INT.Group n) = n by Lm2;

theorem :: GROUP_10:19

for G being Group
for A being non empty Subset of
for g being Element of holds card A = card (A * g) by Lm7;