let G be finite Group; for p being prime Nat 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 )
let p be prime Nat; ( (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 & card (the_sylow_p-subgroups_of_prime (p,G)) divides card G )
set E = the_sylow_p-subgroups_of_prime (p,G);
A1:
p > 1
by NAT_4:12;
consider P being strict Subgroup of G such that
A2:
P is_Sylow_p-subgroup_of_prime p
by Th10;
set P9 = (Omega). P;
reconsider P9 = (Omega). P as strict Subgroup of G ;
reconsider H9 = P9 as Element of Subgroups G by GROUP_3:def 1;
reconsider P9 = P9 as finite strict Subgroup of G ;
H9 = P9
;
then
P9 in the_sylow_p-subgroups_of_prime (p,G)
by A2;
then reconsider P9 = P9 as Element of the_sylow_p-subgroups_of_prime (p,G) ;
set T = the_left_operation_of (P,p);
A3:
P is p -group
by A2;
set G9 = (Omega). G;
set T9 = the_left_operation_of (((Omega). G),p);
set K = the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p)));
A4:
now for y being object holds
( ( y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) implies y in the_sylow_p-subgroups_of_prime (p,G) ) & ( y in the_sylow_p-subgroups_of_prime (p,G) implies y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) ) )reconsider P1 =
P9 as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
reconsider P99 =
P9 as
strict Subgroup of
G ;
let y be
object ;
( ( y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) implies y in the_sylow_p-subgroups_of_prime (p,G) ) & ( y in the_sylow_p-subgroups_of_prime (p,G) implies y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) ) )thus
(
y in the_orbit_of (
P9,
(the_left_operation_of (((Omega). G),p))) implies
y in the_sylow_p-subgroups_of_prime (
p,
G) )
;
( y in the_sylow_p-subgroups_of_prime (p,G) implies y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) )assume
y in the_sylow_p-subgroups_of_prime (
p,
G)
;
y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p)))then consider Q being
Element of
Subgroups G such that A5:
y = Q
and A6:
ex
P being
strict Subgroup of
G st
(
P = Q &
P is_Sylow_p-subgroup_of_prime p )
;
consider Q9 being
strict Subgroup of
G such that A7:
Q9 = Q
and A8:
Q9 is_Sylow_p-subgroup_of_prime p
by A6;
P99,
Q9 are_conjugated
by A2, A8, Th12;
then consider g being
Element of
G such that A9:
Q9 = P99 |^ g
by GROUP_3:def 11;
Q9 in the_sylow_p-subgroups_of_prime (
p,
G)
by A7, A8;
then reconsider Q99 =
Q9 as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
reconsider g9 =
g " as
Element of
((Omega). G) ;
A10:
g9 " =
(g ") "
by GROUP_2:48
.=
g
;
ex
P2 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ex
H1,
H2 being
strict Subgroup of
G ex
g999 being
Element of
G st
(
P2 = (the_left_translation_of (g9,p)) . P1 &
P1 = H1 &
P2 = H2 &
g9 " = g999 &
H2 = H1 |^ g999 )
by Def20;
then
Q9 = ((the_left_operation_of (((Omega). G),p)) ^ g9) . P9
by A9, A10, Def21;
then
P9,
Q99 are_conjugated_under the_left_operation_of (
((Omega). G),
p)
;
hence
y in the_orbit_of (
P9,
(the_left_operation_of (((Omega). G),p)))
by A5, A7;
verum end;
reconsider P = P as finite Subgroup of G ;
reconsider T = the_left_operation_of (P,p) as LeftOperation of P,(the_sylow_p-subgroups_of_prime (p,G)) ;
for x being object holds
( x in the_fixed_points_of T iff x = P9 )
proof
let x be
object ;
( x in the_fixed_points_of T iff x = P9 )
for
h being
Element of
P holds
P9 = (T ^ h) . P9
proof
reconsider P1 =
P9 as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
let h be
Element of
P;
P9 = (T ^ h) . P9
consider P2 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G),
H1,
H2 being
strict Subgroup of
G,
g being
Element of
G such that A11:
P2 = (the_left_translation_of (h,p)) . P1
and A12:
P1 = H1
and A13:
P2 = H2
and A14:
h " = g
and A15:
H2 = H1 |^ g
by Def20;
A16:
g in H1
by A12, A14;
then
carr H1 c= ((g ") * H1) * g
;
then A20:
carr H1 c= carr (H1 |^ g)
by GROUP_3:59;
A21:
card (carr H1) =
card H1
.=
card (H1 |^ g)
by GROUP_3:66
.=
card (carr (H1 |^ g))
;
(T ^ h) . P9 = P2
by A11, Def21;
hence
P9 = (T ^ h) . P9
by A12, A13, A15, A20, A21, CARD_2:102, GROUP_2:59;
verum
end;
then A22:
P9 is_fixed_under T
;
hereby ( x = P9 implies x in the_fixed_points_of T )
assume
x in the_fixed_points_of T
;
x = P9then
x in { x9 where x9 is Element of the_sylow_p-subgroups_of_prime (p,G) : x9 is_fixed_under T }
by Def13;
then consider Q being
Element of
the_sylow_p-subgroups_of_prime (
p,
G)
such that A23:
x = Q
and A24:
Q is_fixed_under T
;
Q in { H99 where H99 is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H99 & P is_Sylow_p-subgroup_of_prime p ) }
;
then consider H99 being
Element of
Subgroups G such that A25:
Q = H99
and A26:
ex
P being
strict Subgroup of
G st
(
P = H99 &
P is_Sylow_p-subgroup_of_prime p )
;
consider Q9 being
strict Subgroup of
G such that A27:
Q9 = H99
and A28:
Q9 is_Sylow_p-subgroup_of_prime p
by A26;
set N =
Normalizer Q9;
now for y being object st y in the carrier of P holds
y in the carrier of (Normalizer Q9)let y be
object ;
( y in the carrier of P implies y in the carrier of (Normalizer Q9) )assume A29:
y in the
carrier of
P
;
y in the carrier of (Normalizer Q9)
ex
h being
Element of
G st
(
y = h &
Q9 |^ h = Q9 )
proof
set h =
y;
the
carrier of
P c= the
carrier of
G
by GROUP_2:def 5;
then reconsider h =
y as
Element of
G by A29;
reconsider h9 =
h as
Element of
P by A29;
take
h
;
( y = h & Q9 |^ h = Q9 )
thus
y = h
;
Q9 |^ h = Q9
dom (T ^ h9) = the_sylow_p-subgroups_of_prime (
p,
G)
by FUNCT_2:def 1;
then
Q9 in dom (T ^ h9)
by A27, A28;
then reconsider Q1 =
Q9 as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
A30:
ex
Q2 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
Q2 = (the_left_translation_of (h9,p)) . Q1 &
Q1 = H1 &
Q2 = H2 &
h9 " = g &
H2 = H1 |^ g )
by Def20;
(
Q9 = (T ^ h9) . Q9 &
T . h9 = the_left_translation_of (
h9,
p) )
by A24, A25, A27, Def21;
then
Q9 |^ (h ") = Q9
by A30, GROUP_2:48;
then
(
(h ") * h = 1_ G &
Q9 |^ ((h ") * h) = Q9 |^ h )
by GROUP_1:def 5, GROUP_3:60;
hence
Q9 |^ h = Q9
by GROUP_3:61;
verum
end; then
y in Normalizer Q9
by GROUP_3:134;
hence
y in the
carrier of
(Normalizer Q9)
;
verum end; then A31:
the
carrier of
P c= the
carrier of
(Normalizer Q9)
;
then A38:
the
carrier of
Q9 c= the
carrier of
(Normalizer Q9)
;
reconsider N =
Normalizer Q9 as
finite Group ;
reconsider Q99 =
Q9 as
strict Subgroup of
N by A38, GROUP_2:57;
A39:
Q99 is_Sylow_p-subgroup_of_prime p
by A28, Lm9;
reconsider P99 =
P9 as
strict Subgroup of
N by A31, GROUP_2:57;
P99 is_Sylow_p-subgroup_of_prime p
by A2, Lm9;
then
P99,
Q99 are_conjugated
by A39, Th12;
then consider n being
Element of
N such that A40:
P99 = Q99 |^ n
by GROUP_3:def 11;
the
carrier of
(Q99 |^ n) c= the
carrier of
N
by GROUP_2:def 5;
then A41: the
multF of
G || the
carrier of
(Q99 |^ n) =
( the multF of G || the carrier of N) || the
carrier of
(Q99 |^ n)
by RELAT_1:74, ZFMISC_1:96
.=
the
multF of
N || the
carrier of
(Q99 |^ n)
by GROUP_2:def 5
;
n in Normalizer Q9
;
then consider n9 being
Element of
G such that A42:
n = n9
and A43:
Q9 |^ n9 = Q9
by GROUP_3:134;
then
the
carrier of
(Q9 |^ n9) = the
carrier of
(Q99 |^ n)
by TARSKI:2;
then the
multF of
(Q9 |^ n9) =
the
multF of
G || the
carrier of
(Q99 |^ n)
by GROUP_2:def 5
.=
the
multF of
(Q99 |^ n)
by A41, GROUP_2:def 5
;
hence
x = P9
by A23, A25, A27, A40, A43, A44, TARSKI:2;
verum
end;
assume
x = P9
;
x in the_fixed_points_of T
then
x in { x9 where x9 is Element of the_sylow_p-subgroups_of_prime (p,G) : x9 is_fixed_under T }
by A22;
hence
x in the_fixed_points_of T
by Def13;
verum
end;
then A51:
the_fixed_points_of T = {P9}
by TARSKI:def 1;
(card (the_sylow_p-subgroups_of_prime (p,G))) mod p =
(card (the_fixed_points_of T)) mod p
by A3, Th9
.=
1 mod p
by A51, CARD_1:30
;
hence
(card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1
by A1, NAT_D:14; card (the_sylow_p-subgroups_of_prime (p,G)) divides card G
A52:
card (the_orbit_of (P9,(the_left_operation_of (((Omega). G),p)))) = Index (the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p))))
by Th8;
reconsider K = the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p))) as Subgroup of (Omega). G ;
card G = (card ((Omega). G)) * 1
;
then A53:
card G = (card K) * (index K)
by GROUP_2:147;
ex B being finite set st
( B = Left_Cosets K & index K = card B )
by GROUP_2:146;
then
card (the_sylow_p-subgroups_of_prime (p,G)) = index K
by A52, A4, TARSKI:2;
hence
card (the_sylow_p-subgroups_of_prime (p,G)) divides card G
by A53, NAT_D:def 3; verum