let G be 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 )
let p be natural prime number ; ( (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 Th12;
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, Def19;
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 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
set ;
( ( 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, Th14;
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:57
.=
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 Def21;
then
Q9 = ((the_left_operation_of ((Omega). G),p) ^ g9) . P9
by A9, A10, Def22;
then
P9,
Q99 are_conjugated_under the_left_operation_of ((Omega). G),
p
by Def14;
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 set holds
( x in the_fixed_points_of T iff x = P9 )
proof
let x be
set ;
( 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 Def21;
A16:
g in H1
by A12, A14, STRUCT_0:def 5;
then
carr H1 c= ((g " ) * H1) * g
by TARSKI:def 3;
then A20:
carr H1 c= carr (H1 |^ g)
by GROUP_3:71;
A21:
card (carr H1) =
card H1
.=
card (H1 |^ g)
by GROUP_3:79
.=
card (carr (H1 |^ g))
;
(T ^ h) . P9 = P2
by A11, Def22;
hence
P9 = (T ^ h) . P9
by A12, A13, A15, A20, A21, CARD_FIN:1, GROUP_2:68;
verum
end;
then A22:
P9 is_fixed_under T
by Def12;
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 =
Normalizator Q9;
now let y be
set ;
( y in the carrier of P implies y in the carrier of (Normalizator Q9) )assume A29:
y in the
carrier of
P
;
y in the carrier of (Normalizator 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 Def21;
(
Q9 = (T ^ h9) . Q9 &
T . h9 = the_left_translation_of h9,
p )
by A24, A25, A27, Def12, Def22;
then
Q9 |^ (h " ) = Q9
by A30, GROUP_2:57;
then
(
(h " ) * h = 1_ G &
Q9 |^ ((h " ) * h) = Q9 |^ h )
by GROUP_1:def 6, GROUP_3:72;
hence
Q9 |^ h = Q9
by GROUP_3:73;
verum
end; then
y in Normalizator Q9
by GROUP_3:160;
hence
y in the
carrier of
(Normalizator Q9)
by STRUCT_0:def 5;
verum end; then A31:
the
carrier of
P c= the
carrier of
(Normalizator Q9)
by TARSKI:def 3;
then A38:
the
carrier of
Q9 c= the
carrier of
(Normalizator Q9)
by TARSKI:def 3;
reconsider N =
Normalizator Q9 as
finite Group ;
reconsider Q99 =
Q9 as
strict Subgroup of
N by A38, GROUP_2:66;
A39:
Q99 is_Sylow_p-subgroup_of_prime p
by A28, Lm9;
reconsider P99 =
P9 as
strict Subgroup of
N by A31, GROUP_2:66;
P99 is_Sylow_p-subgroup_of_prime p
by A2, Lm9;
then
P99,
Q99 are_conjugated
by A39, Th14;
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:103, ZFMISC_1:119
.=
the
multF of
N || the
carrier of
(Q99 |^ n)
by GROUP_2:def 5
;
n in Normalizator Q9
by STRUCT_0:def 5;
then consider n9 being
Element of
G such that A42:
n = n9
and A43:
Q9 |^ n9 = Q9
by GROUP_3:160;
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, Th11
.=
1 mod p
by A51, CARD_1:50
;
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 Th10;
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:177;
ex B being finite set st
( B = Left_Cosets K & index K = card B )
by GROUP_2:176;
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