reconsider x1 = 1, x2 = 0 as set ;
let G be finite Group; for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p
let p be prime Nat; ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
set n = card G;
set LO = the_left_operation_of G;
consider m, r being Nat such that
A1:
card G = (p |^ r) * m
and
A2:
not p divides m
by Lm2;
reconsider k1 = p9 |^ r as Element of NAT by ORDINAL1:def 12;
set SF = the_subsets_of_card (k1, the carrier of G);
card (the_subsets_of_card (k1, the carrier of G)) = card (Choose ( the carrier of G,k1,x1,x2))
by Th2;
then A3:
card (the_subsets_of_card (k1, the carrier of G)) = (card G) choose k1
by CARD_FIN:16;
then
(card (the_subsets_of_card (k1, the carrier of G))) mod p <> 0
by A1, A2, Lm5;
then reconsider E = the_subsets_of_card (k1, the carrier of G) as non empty finite set by NAT_D:26;
set LO9 = the_extension_of_left_operation_of (k1,(the_left_operation_of G));
reconsider T = the_extension_of_left_operation_of (k1,(the_left_operation_of G)) as LeftOperation of G,E ;
ex X being Element of E st (card (the_orbit_of (X,T))) mod p <> 0
proof
consider f being
FinSequence such that A4:
rng f = the_orbits_of T
and A5:
f is
one-to-one
by FINSEQ_4:58;
reconsider f =
f as
FinSequence of
the_orbits_of T by A4, FINSEQ_1:def 4;
deffunc H1(
set )
-> set =
card (f . $1);
consider pf being
FinSequence such that A6:
(
len pf = len f & ( for
i being
Nat st
i in dom pf holds
pf . i = H1(
i) ) )
from FINSEQ_1:sch 2();
for
x being
object st
x in rng pf holds
x in NAT
then
rng pf c= NAT
;
then reconsider c =
pf as
FinSequence of
NAT by FINSEQ_1:def 4;
deffunc H2(
set )
-> set =
(c . $1) / p;
consider c9 being
FinSequence such that A10:
(
len c9 = len c & ( for
i being
Nat st
i in dom c9 holds
c9 . i = H2(
i) ) )
from FINSEQ_1:sch 2();
assume A11:
for
X being
Element of
E holds
(card (the_orbit_of (X,T))) mod p = 0
;
contradiction
for
x being
object st
x in rng c9 holds
x in NAT
proof
reconsider p99 =
p9 as
Real ;
let x be
object ;
( x in rng c9 implies x in NAT )
assume
x in rng c9
;
x in NAT
then consider i being
Nat such that A12:
i in dom c9
and A13:
c9 . i = x
by FINSEQ_2:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
i in dom f
by A6, A10, A12, FINSEQ_3:29;
then
f . i in the_orbits_of T
by A4, FUNCT_1:3;
then consider X being
Subset of
E such that A14:
f . i = X
and A15:
ex
x9 being
Element of
E st
X = the_orbit_of (
x9,
T)
;
dom pf = dom c9
by A10, FINSEQ_3:29;
then
c . i = card X
by A6, A12, A14;
then A16:
(c . i) mod p = 0
by A11, A15;
set q =
(c . i) div p9;
c . i =
(p9 * ((c . i) div p9)) + ((c . i) mod p9)
by NAT_D:2
.=
p9 * ((c . i) div p9)
by A16
;
then consider q being
Nat such that A17:
c . i = p * q
;
x =
(p99 * q) / p99
by A10, A12, A13, A17
.=
(p99 / p99) * q
by XCMPLX_1:74
.=
1
* q
by XCMPLX_1:60
;
hence
x in NAT
by ORDINAL1:def 12;
verum
end;
then
rng c9 c= NAT
;
then reconsider c9 =
c9 as
FinSequence of
NAT by FINSEQ_1:def 4;
A18:
dom c =
Seg (len c9)
by A10, FINSEQ_1:def 3
.=
dom c9
by FINSEQ_1:def 3
.=
dom (p9 * c9)
by VALUED_1:def 5
;
for
k being
Nat st
k in dom c holds
c . k = (p9 * c9) . k
then A20:
c = p9 * c9
by A18, FINSEQ_1:13;
for
i being
Element of
NAT st
i in dom pf holds
pf . i = H1(
i)
by A6;
then
card E = Sum c
by A4, A5, A6, WEDDWITT:6;
then (card E) mod p =
(p9 * (Sum c9)) mod p9
by A20, RVSUM_1:87
.=
0
by NAT_D:13
;
hence
contradiction
by A1, A2, A3, Lm5;
verum
end;
then consider X being Element of E such that
A21:
(card (the_orbit_of (X,T))) mod p <> 0
;
set HX = the_strict_stabilizer_of (X,T);
card (the_orbit_of (X,T)) = Index (the_strict_stabilizer_of (X,T))
by Th8;
then A22:
(index (the_strict_stabilizer_of (X,T))) mod p <> 0
by A21, GROUP_2:def 18;
take
the_strict_stabilizer_of (X,T)
; the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p
X in { X9 where X9 is Subset of the carrier of G : card X9 = k1 }
;
then A24:
ex X9 being Subset of the carrier of G st
( X9 = X & card X9 = k1 )
;
reconsider H = the_strict_stabilizer_of (X,T) as finite Group ;
A25:
the carrier of (the_strict_stabilizer_of (X,T)) = { g where g is Element of G : (T ^ g) .: {X} = {X} }
by Def10;
reconsider X = X as non empty Subset of G by A24;
set x = the Element of X;
reconsider x = the Element of X as Element of G ;
k1 divides card G
by A1, NAT_D:def 3;
then
k1 <= card G
by NAT_D:7;
then
card k1 <= card the carrier of G
;
then A26:
Segm (card k1) c= Segm (card the carrier of G)
by NAT_1:39;
now for z being object st z in the carrier of H holds
z in X * (x ")reconsider X1 =
X as
Element of
E ;
let z be
object ;
( z in the carrier of H implies z in X * (x ") )assume
z in the
carrier of
H
;
z in X * (x ")then consider g being
Element of
G such that A27:
z = g
and A28:
(T ^ g) .: {X} = {X}
by A25;
dom (T ^ g) = E
by FUNCT_2:def 1;
then
Im (
(T ^ g),
X)
= {((T ^ g) . X)}
by FUNCT_1:59;
then A29:
(T ^ g) . X = X
by A28, ZFMISC_1:3;
set h =
g * x;
T . g = the_extension_of_left_translation_of (
k1,
g,
(the_left_operation_of G))
by A26, Def5;
then A30:
(T ^ g) . X1 = ((the_left_operation_of G) ^ g) .: X1
by A26, Def4;
reconsider LO =
the_left_operation_of G as
LeftOperation of
G, the
carrier of
G ;
A31:
LO ^ g = the_left_translation_of g
by Def2;
ex
x9 being
set st
(
x9 in dom (LO ^ g) &
x9 in X &
g * x = (LO ^ g) . x9 )
then A32:
g * x in (LO ^ g) .: X
by FUNCT_1:def 6;
(g * x) * (x ") =
g * (x * (x "))
by GROUP_1:def 3
.=
g * (1_ G)
by GROUP_1:def 5
.=
z
by A27, GROUP_1:def 4
;
hence
z in X * (x ")
by A29, A30, A32, GROUP_2:28;
verum end;
then
the carrier of H c= X * (x ")
;
then
card the carrier of H <= card (X * (x "))
by NAT_1:43;
then A33:
card H <= p |^ r
by A24, Lm7;
(p |^ r) * m = (card (the_strict_stabilizer_of (X,T))) * (index (the_strict_stabilizer_of (X,T)))
by A1, GROUP_2:147;
then
p |^ r divides card H
by A2, A23, Lm6;
then A34:
p |^ r <= card H
by NAT_D:7;
then
card H = p |^ r
by A33, XXREAL_0:1;
then A35:
H is p -group
;
index (the_strict_stabilizer_of (X,T)) =
((index (the_strict_stabilizer_of (X,T))) * (card (the_strict_stabilizer_of (X,T)))) * (1 / (card (the_strict_stabilizer_of (X,T))))
by XCMPLX_1:107
.=
((p |^ r) * m) * (1 / (card (the_strict_stabilizer_of (X,T))))
by A1, GROUP_2:147
.=
((p9 |^ r) * m) * (1 / (p9 |^ r))
by A34, A33, XXREAL_0:1
.=
m * ((p9 |^ r) * (1 / (p9 |^ r)))
.=
m * ((p9 |^ r) / (p9 |^ r))
by XCMPLX_1:99
.=
m
by XCMPLX_1:88
;
hence
the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p
by A2, A35; verum